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

Theorem divcld 10372
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 10265 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  B  =/=  0 )  ->  ( A  /  B )  e.  CC )
51, 2, 3, 4syl3anc 1271 1  |-  ( ph  ->  ( A  /  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1891    =/= wne 2622  (class class class)co 6276   CCcc 9524   0cc0 9526    / cdiv 10258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-resscn 9583  ax-1cn 9584  ax-icn 9585  ax-addcl 9586  ax-addrcl 9587  ax-mulcl 9588  ax-mulrcl 9589  ax-mulcom 9590  ax-addass 9591  ax-mulass 9592  ax-distr 9593  ax-i2m1 9594  ax-1ne0 9595  ax-1rid 9596  ax-rnegex 9597  ax-rrecex 9598  ax-cnre 9599  ax-pre-lttri 9600  ax-pre-lttrn 9601  ax-pre-ltadd 9602  ax-pre-mulgt0 9603
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-po 4733  df-so 4734  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-riota 6238  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-er 7350  df-en 7557  df-dom 7558  df-sdom 7559  df-pnf 9664  df-mnf 9665  df-xr 9666  df-ltxr 9667  df-le 9668  df-sub 9849  df-neg 9850  df-div 10259
This theorem is referenced by:  dmdcan2d  10402  hashf1  12615  abs1m  13409  abslem2  13413  sqreulem  13433  sqreu  13434  o1fsum  13884  divrcnv  13921  divcnv  13922  geolim  13937  geolim2  13938  geo2sum  13940  geo2lim  13942  fproddiv  14026  bpolycl  14116  bpolysum  14117  bpolydiflem  14118  bpoly4  14123  eftcl  14139  efaddlem  14158  tancl  14194  tanval2  14198  qredeq  14674  pcaddlem  14844  pjthlem1  22402  iblss  22774  itgeqa  22783  iblconst  22787  iblabsr  22799  iblmulc2  22800  itgsplit  22805  dvlem  22863  dvmulbr  22905  dvcobr  22912  dvrec  22921  dvcnvlem  22940  dveflem  22943  dvsincos  22945  dvlip  22957  c1liplem1  22960  lhop1lem  22977  lhop1  22978  lhop2  22979  lhop  22980  ftc1lem4  23003  vieta1lem2  23276  vieta1  23277  elqaalem3  23286  elqaalem3OLD  23289  aareccl  23294  aalioulem1  23300  taylfvallem1  23324  tayl0  23329  taylply2  23335  taylply  23336  dvtaylp  23337  taylthlem2  23341  ulmdvlem1  23367  tanregt0  23500  eff1olem  23509  argregt0  23571  argrege0  23572  argimgt0  23573  logcnlem4  23602  advlogexp  23612  logtaylsum  23618  logtayl2  23619  root1eq1  23707  logbcl  23716  cxplogb  23735  logbf  23738  angcld  23746  angrteqvd  23747  cosangneg2d  23748  angrtmuld  23749  ang180lem1  23750  ang180lem2  23751  ang180lem3  23752  ang180lem4  23753  ang180lem5  23754  lawcoslem1  23756  lawcos  23757  isosctrlem2  23760  isosctrlem3  23761  angpieqvdlem  23766  angpieqvdlem2  23767  angpieqvd  23769  dcubic1lem  23781  dcubic2  23782  dcubic1  23783  dcubic  23784  mcubic  23785  cubic2  23786  dquartlem1  23789  dquartlem2  23790  dquart  23791  quart1cl  23792  quart1lem  23793  quart1  23794  quartlem3  23797  quartlem4  23798  quart  23799  tanatan  23857  atantayl  23875  atantayl2  23876  atantayl3  23877  log2cnv  23882  birthdaylem2  23890  efrlim  23907  dfef2  23908  cxploglim2  23916  fsumharmonic  23949  lgamgulmlem2  23967  lgamgulmlem3  23968  lgamgulmlem4  23969  lgamgulmlem5  23970  lgamgulmlem6  23971  lgamgulm2  23973  lgamcvg2  23992  gamcvg  23993  gamcvg2lem  23996  ftalem4  24012  ftalem5  24013  ftalem4OLD  24014  ftalem5OLD  24015  basellem8  24026  logexprlim  24165  bposlem9  24232  2sqlem3  24306  dchrmusum2  24344  dchrvmasum2lem  24346  dchrvmasumiflem1  24351  dchrvmasumiflem2  24352  dchrvmaeq0  24354  dchrisum0re  24363  dchrisum0lem1b  24365  dchrisum0lem1  24366  dchrisum0lem2a  24367  dchrisum0lem2  24368  dchrisum0lem3  24369  dchrisum0  24370  mudivsum  24380  vmalogdivsum2  24388  vmalogdivsum  24389  2vmadivsumlem  24390  selberg2  24401  selberg3lem1  24407  selberg3  24409  selberg4lem1  24410  selbergr  24418  selberg3r  24419  selberg4r  24420  selberg34r  24421  pntrlog2bndlem1  24427  pntrlog2bndlem2  24428  pntrlog2bndlem3  24429  pntrlog2bndlem4  24430  pntrlog2bndlem5  24431  colinearalg  24952  axcontlem8  25013  pjhthlem1  27056  eigvalcl  27626  riesz3i  27727  bcm1n  28379  divnumden2  28389  oddpwdc  29193  signsplypnf  29445  signsply0  29446  subfacval2  29916  divcnvlin  30373  bcprod  30380  iprodgam  30384  itg2addnclem  31995  iblmulc2nc  32009  ftc1cnnclem  32017  areacirclem1  32034  areacirclem4  32037  areacirc  32039  cntotbnd  32130  pellexlem2  35676  pellexlem6  35680  jm2.19  35850  jm2.27c  35864  proot1ex  36080  cvgdvgrat  36663  radcnvrat  36664  hashnzfzclim  36672  bcccl  36689  bccm1k  36692  binomcxplemrat  36700  binomcxplemfrat  36701  binomcxplemnotnn0  36706  xralrple2  37608  mccllem  37719  clim1fr1  37721  0ellimcdiv  37772  coseq0  37781  dvrecg  37824  dvmptdiv  37831  fperdvper  37832  dvdivbd  37837  dvnmptdivc  37855  dvnxpaek  37859  dvnprodlem2  37864  iblsplit  37885  itgcoscmulx  37888  itgsincmulx  37893  stoweidlem11  37928  stoweidlem26  37943  stoweidlem42  37960  wallispilem4  37987  wallispilem5  37988  wallispi  37989  wallispi2lem1  37990  wallispi2lem2  37991  wallispi2  37992  stirlinglem1  37993  stirlinglem3  37995  stirlinglem4  37996  stirlinglem5  37997  stirlinglem6  37998  stirlinglem7  37999  stirlinglem13  38005  stirlinglem14  38006  stirlinglem15  38007  dirkeritg  38021  dirkercncflem1  38022  dirkercncflem2  38023  fourierdlem26  38052  fourierdlem39  38066  fourierdlem56  38083  fourierdlem62  38089  fourierdlem72  38099  fourierdlem74  38101  fourierdlem75  38102  fourierdlem76  38103  fourierdlem80  38107  fourierdlem103  38130  fourierdlem104  38131  fouriersw  38152  elaa2lem  38154  elaa2lemOLD  38155  etransclem15  38171  etransclem20  38176  etransclem21  38177  etransclem22  38178  etransclem23  38179  etransclem24  38180  etransclem25  38181  etransclem31  38187  etransclem32  38188  etransclem33  38189  etransclem34  38190  etransclem35  38191  etransclem47  38203  etransclem48OLD  38204  etransclem48  38205  hoiqssbllem2  38508  sigardiv  38561  sharhght  38565  fdivmptf  40677  cotcl  40797
  Copyright terms: Public domain W3C validator