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

Theorem divcld 10255
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 10148 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  B  =/=  0 )  ->  ( A  /  B )  e.  CC )
51, 2, 3, 4syl3anc 1226 1  |-  ( ph  ->  ( A  /  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1836    =/= wne 2587  (class class class)co 6214   CCcc 9419   0cc0 9421    / cdiv 10141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497  ax-pre-mulgt0 9498
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rmo 2750  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-po 4727  df-so 4728  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-sub 9738  df-neg 9739  df-div 10142
This theorem is referenced by:  dmdcan2d  10285  hashf1  12429  abs1m  13189  abslem2  13193  sqreulem  13213  sqreu  13214  o1fsum  13648  divrcnv  13685  divcnv  13686  geolim  13700  geolim2  13701  geo2sum  13703  geo2lim  13705  fproddiv  13787  eftcl  13830  efaddlem  13849  tancl  13885  tanval2  13889  qredeq  14268  pcaddlem  14428  pjthlem1  21956  iblss  22315  itgeqa  22324  iblconst  22328  iblabsr  22340  iblmulc2  22341  itgsplit  22346  dvlem  22404  dvmulbr  22446  dvcobr  22453  dvrec  22462  dvcnvlem  22481  dveflem  22484  dvsincos  22486  dvlip  22498  c1liplem1  22501  lhop1lem  22518  lhop1  22519  lhop2  22520  lhop  22521  ftc1lem4  22544  vieta1lem2  22811  vieta1  22812  elqaalem3  22821  aareccl  22826  aalioulem1  22832  taylfvallem1  22856  tayl0  22861  taylply2  22867  taylply  22868  dvtaylp  22869  taylthlem2  22873  ulmdvlem1  22899  tanregt0  23030  eff1olem  23039  argregt0  23101  argrege0  23102  argimgt0  23103  logcnlem4  23132  advlogexp  23142  logtaylsum  23148  logtayl2  23149  root1eq1  23235  logbcl  23244  cxplogb  23263  logbf  23266  angcld  23274  angrteqvd  23275  cosangneg2d  23276  angrtmuld  23277  ang180lem1  23278  ang180lem2  23279  ang180lem3  23280  ang180lem4  23281  ang180lem5  23282  lawcoslem1  23284  lawcos  23285  isosctrlem2  23288  isosctrlem3  23289  angpieqvdlem  23294  angpieqvdlem2  23295  angpieqvd  23297  dcubic1lem  23309  dcubic2  23310  dcubic1  23311  dcubic  23312  mcubic  23313  cubic2  23314  dquartlem1  23317  dquartlem2  23318  dquart  23319  quart1cl  23320  quart1lem  23321  quart1  23322  quartlem3  23325  quartlem4  23326  quart  23327  tanatan  23385  atantayl  23403  atantayl2  23404  atantayl3  23405  log2cnv  23410  birthdaylem2  23418  efrlim  23435  dfef2  23436  cxploglim2  23444  fsumharmonic  23477  ftalem4  23485  ftalem5  23486  basellem8  23497  logexprlim  23636  bposlem9  23703  2sqlem3  23777  dchrmusum2  23815  dchrvmasum2lem  23817  dchrvmasumiflem1  23822  dchrvmasumiflem2  23823  dchrvmaeq0  23825  dchrisum0re  23834  dchrisum0lem1b  23836  dchrisum0lem1  23837  dchrisum0lem2a  23838  dchrisum0lem2  23839  dchrisum0lem3  23840  dchrisum0  23841  mudivsum  23851  vmalogdivsum2  23859  vmalogdivsum  23860  2vmadivsumlem  23861  selberg2  23872  selberg3lem1  23878  selberg3  23880  selberg4lem1  23881  selbergr  23889  selberg3r  23890  selberg4r  23891  selberg34r  23892  pntrlog2bndlem1  23898  pntrlog2bndlem2  23899  pntrlog2bndlem3  23900  pntrlog2bndlem4  23901  pntrlog2bndlem5  23902  colinearalg  24355  axcontlem8  24416  pjhthlem1  26447  eigvalcl  27017  riesz3i  27118  bcm1n  27783  divnumden2  27792  oddpwdc  28512  signsplypnf  28726  signsply0  28727  lgamgulmlem2  28797  lgamgulmlem3  28798  lgamgulmlem4  28799  lgamgulmlem5  28800  lgamgulmlem6  28801  lgamgulm2  28803  lgamcvg2  28822  gamcvg  28823  gamcvg2lem  28826  subfacval2  28856  divcnvlin  29320  iprodgam  29327  bpolycl  30003  bpolysum  30004  bpolydiflem  30005  bpoly4  30010  itg2addnclem  30268  iblmulc2nc  30282  ftc1cnnclem  30290  areacirclem1  30309  areacirclem4  30312  areacirc  30314  cntotbnd  30494  pellexlem2  30967  pellexlem6  30971  jm2.19  31137  jm2.27c  31151  proot1ex  31365  cvgdvgrat  31398  radcnvrat  31399  hashnzfzclim  31431  bcccl  31448  bccm1k  31451  binomcxplemrat  31459  binomcxplemfrat  31460  binomcxplemnotnn0  31465  mccllem  31806  clim1fr1  31808  0ellimcdiv  31856  coseq0  31865  dvrecg  31908  dvmptdiv  31915  fperdvper  31916  dvdivbd  31921  dvnmptdivc  31936  dvnxpaek  31940  dvnprodlem2  31945  iblsplit  31966  itgcoscmulx  31969  itgsincmulx  31974  stoweidlem11  31994  stoweidlem26  32009  stoweidlem42  32025  wallispilem4  32051  wallispilem5  32052  wallispi  32053  wallispi2lem1  32054  wallispi2lem2  32055  wallispi2  32056  stirlinglem1  32057  stirlinglem3  32059  stirlinglem4  32060  stirlinglem5  32061  stirlinglem6  32062  stirlinglem7  32063  stirlinglem13  32069  stirlinglem14  32070  stirlinglem15  32071  dirkeritg  32085  dirkercncflem1  32086  dirkercncflem2  32087  fourierdlem26  32116  fourierdlem39  32129  fourierdlem56  32146  fourierdlem62  32152  fourierdlem72  32162  fourierdlem74  32164  fourierdlem75  32165  fourierdlem76  32166  fourierdlem80  32170  fourierdlem103  32193  fourierdlem104  32194  fouriersw  32215  elaa2lem  32217  etransclem15  32233  etransclem20  32238  etransclem21  32239  etransclem22  32240  etransclem23  32241  etransclem24  32242  etransclem25  32243  etransclem31  32249  etransclem32  32250  etransclem33  32251  etransclem34  32252  etransclem35  32253  etransclem47  32265  etransclem48  32266  sigardiv  32279  sharhght  32283  fdivmptf  33397  cotcl  33517
  Copyright terms: Public domain W3C validator