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

Theorem divcld 10390
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 10283 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  B  =/=  0 )  ->  ( A  /  B )  e.  CC )
51, 2, 3, 4syl3anc 1264 1  |-  ( ph  ->  ( A  /  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872    =/= wne 2614  (class class class)co 6305   CCcc 9544   0cc0 9546    / cdiv 10276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-div 10277
This theorem is referenced by:  dmdcan2d  10420  hashf1  12624  abs1m  13398  abslem2  13402  sqreulem  13422  sqreu  13423  o1fsum  13872  divrcnv  13909  divcnv  13910  geolim  13925  geolim2  13926  geo2sum  13928  geo2lim  13930  fproddiv  14014  bpolycl  14104  bpolysum  14105  bpolydiflem  14106  bpoly4  14111  eftcl  14127  efaddlem  14146  tancl  14182  tanval2  14186  qredeq  14662  pcaddlem  14832  pjthlem1  22389  iblss  22760  itgeqa  22769  iblconst  22773  iblabsr  22785  iblmulc2  22786  itgsplit  22791  dvlem  22849  dvmulbr  22891  dvcobr  22898  dvrec  22907  dvcnvlem  22926  dveflem  22929  dvsincos  22931  dvlip  22943  c1liplem1  22946  lhop1lem  22963  lhop1  22964  lhop2  22965  lhop  22966  ftc1lem4  22989  vieta1lem2  23262  vieta1  23263  elqaalem3  23272  elqaalem3OLD  23275  aareccl  23280  aalioulem1  23286  taylfvallem1  23310  tayl0  23315  taylply2  23321  taylply  23322  dvtaylp  23323  taylthlem2  23327  ulmdvlem1  23353  tanregt0  23486  eff1olem  23495  argregt0  23557  argrege0  23558  argimgt0  23559  logcnlem4  23588  advlogexp  23598  logtaylsum  23604  logtayl2  23605  root1eq1  23693  logbcl  23702  cxplogb  23721  logbf  23724  angcld  23732  angrteqvd  23733  cosangneg2d  23734  angrtmuld  23735  ang180lem1  23736  ang180lem2  23737  ang180lem3  23738  ang180lem4  23739  ang180lem5  23740  lawcoslem1  23742  lawcos  23743  isosctrlem2  23746  isosctrlem3  23747  angpieqvdlem  23752  angpieqvdlem2  23753  angpieqvd  23755  dcubic1lem  23767  dcubic2  23768  dcubic1  23769  dcubic  23770  mcubic  23771  cubic2  23772  dquartlem1  23775  dquartlem2  23776  dquart  23777  quart1cl  23778  quart1lem  23779  quart1  23780  quartlem3  23783  quartlem4  23784  quart  23785  tanatan  23843  atantayl  23861  atantayl2  23862  atantayl3  23863  log2cnv  23868  birthdaylem2  23876  efrlim  23893  dfef2  23894  cxploglim2  23902  fsumharmonic  23935  lgamgulmlem2  23953  lgamgulmlem3  23954  lgamgulmlem4  23955  lgamgulmlem5  23956  lgamgulmlem6  23957  lgamgulm2  23959  lgamcvg2  23978  gamcvg  23979  gamcvg2lem  23982  ftalem4  23998  ftalem5  23999  ftalem4OLD  24000  ftalem5OLD  24001  basellem8  24012  logexprlim  24151  bposlem9  24218  2sqlem3  24292  dchrmusum2  24330  dchrvmasum2lem  24332  dchrvmasumiflem1  24337  dchrvmasumiflem2  24338  dchrvmaeq0  24340  dchrisum0re  24349  dchrisum0lem1b  24351  dchrisum0lem1  24352  dchrisum0lem2a  24353  dchrisum0lem2  24354  dchrisum0lem3  24355  dchrisum0  24356  mudivsum  24366  vmalogdivsum2  24374  vmalogdivsum  24375  2vmadivsumlem  24376  selberg2  24387  selberg3lem1  24393  selberg3  24395  selberg4lem1  24396  selbergr  24404  selberg3r  24405  selberg4r  24406  selberg34r  24407  pntrlog2bndlem1  24413  pntrlog2bndlem2  24414  pntrlog2bndlem3  24415  pntrlog2bndlem4  24416  pntrlog2bndlem5  24417  colinearalg  24938  axcontlem8  24999  pjhthlem1  27042  eigvalcl  27612  riesz3i  27713  bcm1n  28377  divnumden2  28388  oddpwdc  29195  signsplypnf  29447  signsply0  29448  subfacval2  29918  divcnvlin  30374  bcprod  30381  iprodgam  30385  itg2addnclem  31957  iblmulc2nc  31971  ftc1cnnclem  31979  areacirclem1  31996  areacirclem4  31999  areacirc  32001  cntotbnd  32092  pellexlem2  35644  pellexlem6  35648  jm2.19  35818  jm2.27c  35832  proot1ex  36048  cvgdvgrat  36632  radcnvrat  36633  hashnzfzclim  36641  bcccl  36658  bccm1k  36661  binomcxplemrat  36669  binomcxplemfrat  36670  binomcxplemnotnn0  36675  xralrple2  37531  mccllem  37617  clim1fr1  37619  0ellimcdiv  37670  coseq0  37679  dvrecg  37722  dvmptdiv  37729  fperdvper  37730  dvdivbd  37735  dvnmptdivc  37753  dvnxpaek  37757  dvnprodlem2  37762  iblsplit  37783  itgcoscmulx  37786  itgsincmulx  37791  stoweidlem11  37811  stoweidlem26  37826  stoweidlem42  37843  wallispilem4  37870  wallispilem5  37871  wallispi  37872  wallispi2lem1  37873  wallispi2lem2  37874  wallispi2  37875  stirlinglem1  37876  stirlinglem3  37878  stirlinglem4  37879  stirlinglem5  37880  stirlinglem6  37881  stirlinglem7  37882  stirlinglem13  37888  stirlinglem14  37889  stirlinglem15  37890  dirkeritg  37904  dirkercncflem1  37905  dirkercncflem2  37906  fourierdlem26  37935  fourierdlem39  37949  fourierdlem56  37966  fourierdlem62  37972  fourierdlem72  37982  fourierdlem74  37984  fourierdlem75  37985  fourierdlem76  37986  fourierdlem80  37990  fourierdlem103  38013  fourierdlem104  38014  fouriersw  38035  elaa2lem  38037  elaa2lemOLD  38038  etransclem15  38054  etransclem20  38059  etransclem21  38060  etransclem22  38061  etransclem23  38062  etransclem24  38063  etransclem25  38064  etransclem31  38070  etransclem32  38071  etransclem33  38072  etransclem34  38073  etransclem35  38074  etransclem47  38086  etransclem48OLD  38087  etransclem48  38088  sigardiv  38341  sharhght  38345  fdivmptf  39974  cotcl  40094
  Copyright terms: Public domain W3C validator