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

Theorem divcld 10327
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 10220 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  B  =/=  0 )  ->  ( A  /  B )  e.  CC )
51, 2, 3, 4syl3anc 1229 1  |-  ( ph  ->  ( A  /  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804    =/= wne 2638  (class class class)co 6281   CCcc 9493   0cc0 9495    / cdiv 10213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-po 4790  df-so 4791  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-div 10214
This theorem is referenced by:  dmdcan2d  10357  hashf1  12488  abs1m  13150  abslem2  13154  sqreulem  13174  sqreu  13175  o1fsum  13609  divrcnv  13646  divcnv  13647  geolim  13661  geolim2  13662  geo2sum  13664  geo2lim  13666  fproddiv  13748  eftcl  13791  efaddlem  13810  tancl  13846  tanval2  13850  qredeq  14229  pcaddlem  14389  pjthlem1  21830  iblss  22189  itgeqa  22198  iblconst  22202  iblabsr  22214  iblmulc2  22215  itgsplit  22220  dvlem  22278  dvmulbr  22320  dvcobr  22327  dvrec  22336  dvcnvlem  22355  dveflem  22358  dvsincos  22360  dvlip  22372  c1liplem1  22375  lhop1lem  22392  lhop1  22393  lhop2  22394  lhop  22395  ftc1lem4  22418  vieta1lem2  22685  vieta1  22686  elqaalem3  22695  aareccl  22700  aalioulem1  22706  taylfvallem1  22730  tayl0  22735  taylply2  22741  taylply  22742  dvtaylp  22743  taylthlem2  22747  ulmdvlem1  22773  tanregt0  22904  eff1olem  22913  argregt0  22973  argrege0  22974  argimgt0  22975  logcnlem4  23004  advlogexp  23014  logtaylsum  23020  logtayl2  23021  root1eq1  23107  angcld  23115  angrteqvd  23116  cosangneg2d  23117  angrtmuld  23118  ang180lem1  23119  ang180lem2  23120  ang180lem3  23121  ang180lem4  23122  ang180lem5  23123  lawcoslem1  23125  lawcos  23126  isosctrlem2  23131  isosctrlem3  23132  angpieqvdlem  23137  angpieqvdlem2  23138  angpieqvd  23140  dcubic1lem  23152  dcubic2  23153  dcubic1  23154  dcubic  23155  mcubic  23156  cubic2  23157  dquartlem1  23160  dquartlem2  23161  dquart  23162  quart1cl  23163  quart1lem  23164  quart1  23165  quartlem3  23168  quartlem4  23169  quart  23170  tanatan  23228  atantayl  23246  atantayl2  23247  atantayl3  23248  log2cnv  23253  birthdaylem2  23260  efrlim  23277  dfef2  23278  cxploglim2  23286  fsumharmonic  23319  ftalem4  23327  ftalem5  23328  basellem8  23339  logexprlim  23478  bposlem9  23545  2sqlem3  23619  dchrmusum2  23657  dchrvmasum2lem  23659  dchrvmasumiflem1  23664  dchrvmasumiflem2  23665  dchrvmaeq0  23667  dchrisum0re  23676  dchrisum0lem1b  23678  dchrisum0lem1  23679  dchrisum0lem2a  23680  dchrisum0lem2  23681  dchrisum0lem3  23682  dchrisum0  23683  mudivsum  23693  vmalogdivsum2  23701  vmalogdivsum  23702  2vmadivsumlem  23703  selberg2  23714  selberg3lem1  23720  selberg3  23722  selberg4lem1  23723  selbergr  23731  selberg3r  23732  selberg4r  23733  selberg34r  23734  pntrlog2bndlem1  23740  pntrlog2bndlem2  23741  pntrlog2bndlem3  23742  pntrlog2bndlem4  23743  pntrlog2bndlem5  23744  colinearalg  24191  axcontlem8  24252  pjhthlem1  26287  eigvalcl  26858  riesz3i  26959  bcm1n  27578  divnumden2  27587  logbcl  27991  oddpwdc  28271  signsplypnf  28485  signsply0  28486  lgamgulmlem2  28550  lgamgulmlem3  28551  lgamgulmlem4  28552  lgamgulmlem5  28553  lgamgulmlem6  28554  lgamgulm2  28556  lgamcvg2  28575  gamcvg  28576  gamcvg2lem  28579  subfacval2  28609  divcnvlin  29096  iprodgam  29101  bpolycl  29790  bpolysum  29791  bpolydiflem  29792  bpoly4  29797  itg2addnclem  30042  iblmulc2nc  30056  ftc1cnnclem  30064  areacirclem1  30083  areacirclem4  30086  areacirc  30088  cntotbnd  30268  pellexlem2  30742  pellexlem6  30746  jm2.19  30911  jm2.27c  30925  proot1ex  31137  cvgdvgrat  31170  radcnvrat  31171  hashnzfzclim  31203  mccllem  31559  clim1fr1  31561  0ellimcdiv  31609  coseq0  31618  dvrecg  31661  dvmptdiv  31668  fperdvper  31669  dvdivbd  31674  dvnmptdivc  31689  dvnxpaek  31693  dvnprodlem2  31698  iblsplit  31719  itgcoscmulx  31722  itgsincmulx  31727  stoweidlem11  31747  stoweidlem26  31762  stoweidlem42  31778  wallispilem4  31804  wallispilem5  31805  wallispi  31806  wallispi2lem1  31807  wallispi2lem2  31808  wallispi2  31809  stirlinglem1  31810  stirlinglem3  31812  stirlinglem4  31813  stirlinglem5  31814  stirlinglem6  31815  stirlinglem7  31816  stirlinglem13  31822  stirlinglem14  31823  stirlinglem15  31824  dirkeritg  31838  dirkercncflem1  31839  dirkercncflem2  31840  fourierdlem26  31869  fourierdlem39  31882  fourierdlem56  31899  fourierdlem62  31905  fourierdlem72  31915  fourierdlem74  31917  fourierdlem75  31918  fourierdlem76  31919  fourierdlem80  31923  fourierdlem103  31946  fourierdlem104  31947  fouriersw  31968  elaa2lem  31970  etransclem15  31986  etransclem20  31991  etransclem21  31992  etransclem22  31993  etransclem23  31994  etransclem24  31995  etransclem25  31996  etransclem31  32002  etransclem32  32003  etransclem33  32004  etransclem34  32005  etransclem35  32006  etransclem47  32018  etransclem48  32019  sigardiv  32032  sharhght  32036  cotcl  33016
  Copyright terms: Public domain W3C validator