MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  divcld Structured version   Unicode version

Theorem divcld 10099
Description: Closure law for division. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
div1d.1  |-  ( ph  ->  A  e.  CC )
divcld.2  |-  ( ph  ->  B  e.  CC )
divcld.3  |-  ( ph  ->  B  =/=  0 )
Assertion
Ref Expression
divcld  |-  ( ph  ->  ( A  /  B
)  e.  CC )

Proof of Theorem divcld
StepHypRef Expression
1 div1d.1 . 2  |-  ( ph  ->  A  e.  CC )
2 divcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 divcld.3 . 2  |-  ( ph  ->  B  =/=  0 )
4 divcl 9992 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  B  =/=  0 )  ->  ( A  /  B )  e.  CC )
51, 2, 3, 4syl3anc 1218 1  |-  ( ph  ->  ( A  /  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    =/= wne 2601  (class class class)co 6086   CCcc 9272   0cc0 9274    / cdiv 9985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-po 4636  df-so 4637  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986
This theorem is referenced by:  dmdcan2d  10129  hashf1  12202  abs1m  12815  abslem2  12819  sqreulem  12839  sqreu  12840  o1fsum  13268  divrcnv  13307  divcnv  13308  geolim  13322  geolim2  13323  geo2sum  13325  geo2lim  13327  eftcl  13351  efaddlem  13370  tancl  13405  tanval2  13409  qredeq  13784  pcaddlem  13942  pjthlem1  20899  iblss  21257  itgeqa  21266  iblconst  21270  iblabsr  21282  iblmulc2  21283  itgsplit  21288  dvlem  21346  dvmulbr  21388  dvcobr  21395  dvrec  21404  dvcnvlem  21423  dveflem  21426  dvsincos  21428  dvlip  21440  c1liplem1  21443  lhop1lem  21460  lhop1  21461  lhop2  21462  lhop  21463  ftc1lem4  21486  vieta1lem2  21752  vieta1  21753  elqaalem3  21762  aareccl  21767  aalioulem1  21773  taylfvallem1  21797  tayl0  21802  taylply2  21808  taylply  21809  dvtaylp  21810  taylthlem2  21814  ulmdvlem1  21840  tanregt0  21970  eff1olem  21979  argregt0  22034  argrege0  22035  argimgt0  22036  logcnlem4  22065  advlogexp  22075  logtaylsum  22081  logtayl2  22082  root1eq1  22168  angcld  22176  angrteqvd  22177  cosangneg2d  22178  angrtmuld  22179  ang180lem1  22180  ang180lem2  22181  ang180lem3  22182  ang180lem4  22183  ang180lem5  22184  lawcoslem1  22186  lawcos  22187  isosctrlem2  22192  isosctrlem3  22193  angpieqvdlem  22198  angpieqvdlem2  22199  angpieqvd  22201  dcubic1lem  22213  dcubic2  22214  dcubic1  22215  dcubic  22216  mcubic  22217  cubic2  22218  dquartlem1  22221  dquartlem2  22222  dquart  22223  quart1cl  22224  quart1lem  22225  quart1  22226  quartlem3  22229  quartlem4  22230  quart  22231  tanatan  22289  atantayl  22307  atantayl2  22308  atantayl3  22309  log2cnv  22314  birthdaylem2  22321  efrlim  22338  dfef2  22339  cxploglim2  22347  fsumharmonic  22380  ftalem4  22388  ftalem5  22389  basellem8  22400  logexprlim  22539  bposlem9  22606  2sqlem3  22680  dchrmusum2  22718  dchrvmasum2lem  22720  dchrvmasumiflem1  22725  dchrvmasumiflem2  22726  dchrvmaeq0  22728  dchrisum0re  22737  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2a  22741  dchrisum0lem2  22742  dchrisum0lem3  22743  dchrisum0  22744  mudivsum  22754  vmalogdivsum2  22762  vmalogdivsum  22763  2vmadivsumlem  22764  selberg2  22775  selberg3lem1  22781  selberg3  22783  selberg4lem1  22784  selbergr  22792  selberg3r  22793  selberg4r  22794  selberg34r  22795  pntrlog2bndlem1  22801  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  colinearalg  23107  axcontlem8  23168  pjhthlem1  24745  eigvalcl  25316  riesz3i  25417  bcm1n  26030  divnumden2  26038  logbcl  26408  oddpwdc  26689  signsplypnf  26903  signsply0  26904  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem4  26970  lgamgulmlem5  26971  lgamgulmlem6  26972  lgamgulm2  26974  lgamcvg2  26993  gamcvg  26994  gamcvg2lem  26997  subfacval2  27027  divcnvlin  27350  fproddiv  27423  iprodgam  27457  bpolycl  28146  bpolysum  28147  bpolydiflem  28148  bpoly4  28153  itg2addnclem  28396  iblmulc2nc  28410  ftc1cnnclem  28418  areacirclem1  28437  areacirclem4  28440  areacirc  28442  cntotbnd  28648  pellexlem2  29124  pellexlem6  29128  jm2.19  29295  jm2.27c  29309  proot1ex  29522  clim1fr1  29727  stoweidlem11  29759  stoweidlem26  29774  stoweidlem42  29790  wallispilem4  29816  wallispilem5  29817  wallispi  29818  wallispi2lem1  29819  wallispi2lem2  29820  wallispi2  29821  stirlinglem1  29822  stirlinglem3  29824  stirlinglem4  29825  stirlinglem5  29826  stirlinglem6  29827  stirlinglem7  29828  stirlinglem13  29834  stirlinglem14  29835  stirlinglem15  29836  sigardiv  29850  sharhght  29854  cotcl  30976
  Copyright terms: Public domain W3C validator