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

Theorem divcld 9722
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 9616 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  B  =/=  0 )  ->  ( A  /  B )  e.  CC )
51, 2, 3, 4syl3anc 1184 1  |-  ( ph  ->  ( A  /  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717    =/= wne 2550  (class class class)co 6020   CCcc 8921   0cc0 8923    / cdiv 9609
This theorem is referenced by:  dmdcan2d  9752  hashf1  11633  abs1m  12066  abslem2  12070  sqreulem  12090  sqreu  12091  o1fsum  12519  divrcnv  12559  divcnv  12560  geolim  12574  geolim2  12575  geo2sum  12577  geo2lim  12579  eftcl  12603  efaddlem  12622  tancl  12657  tanval2  12661  qredeq  13033  pcaddlem  13184  pjthlem1  19205  iblss  19563  itgeqa  19572  iblconst  19576  iblabsr  19588  iblmulc2  19589  itgsplit  19594  dvlem  19650  dvmulbr  19692  dvcobr  19699  dvrec  19708  dvcnvlem  19727  dveflem  19730  dvsincos  19732  dvlip  19744  c1liplem1  19747  lhop1lem  19764  lhop1  19765  lhop2  19766  lhop  19767  ftc1lem4  19790  vieta1lem2  20095  vieta1  20096  elqaalem3  20105  aareccl  20110  aalioulem1  20116  taylfvallem1  20140  tayl0  20145  taylply2  20151  taylply  20152  dvtaylp  20153  taylthlem2  20157  ulmdvlem1  20183  tanregt0  20308  eff1olem  20317  argregt0  20372  argrege0  20373  argimgt0  20374  logcnlem4  20403  advlogexp  20413  logtaylsum  20419  logtayl2  20420  root1eq1  20506  angcld  20514  angrteqvd  20515  cosangneg2d  20516  angrtmuld  20517  ang180lem1  20518  ang180lem2  20519  ang180lem3  20520  ang180lem4  20521  ang180lem5  20522  lawcoslem1  20524  lawcos  20525  isosctrlem2  20530  isosctrlem3  20531  angpieqvdlem  20536  angpieqvdlem2  20537  angpieqvd  20539  dcubic1lem  20550  dcubic2  20551  dcubic1  20552  dcubic  20553  mcubic  20554  cubic2  20555  dquartlem1  20558  dquartlem2  20559  dquart  20560  quart1cl  20561  quart1lem  20562  quart1  20563  quartlem3  20566  quartlem4  20567  quart  20568  tanatan  20626  atantayl  20644  atantayl2  20645  atantayl3  20646  log2cnv  20651  birthdaylem2  20658  efrlim  20675  dfef2  20676  cxploglim2  20684  fsumharmonic  20717  ftalem4  20725  ftalem5  20726  basellem8  20737  logexprlim  20876  bposlem9  20943  2sqlem3  21017  dchrmusum2  21055  dchrvmasum2lem  21057  dchrvmasumiflem1  21062  dchrvmasumiflem2  21063  dchrvmaeq0  21065  dchrisum0re  21074  dchrisum0lem1b  21076  dchrisum0lem1  21077  dchrisum0lem2a  21078  dchrisum0lem2  21079  dchrisum0lem3  21080  dchrisum0  21081  mudivsum  21091  vmalogdivsum2  21099  vmalogdivsum  21100  2vmadivsumlem  21101  selberg2  21112  selberg3lem1  21118  selberg3  21120  selberg4lem1  21121  selbergr  21129  selberg3r  21130  selberg4r  21131  selberg34r  21132  pntrlog2bndlem1  21138  pntrlog2bndlem2  21139  pntrlog2bndlem3  21140  pntrlog2bndlem4  21141  pntrlog2bndlem5  21142  pjhthlem1  22741  eigvalcl  23312  riesz3i  23413  bcm1n  23987  divnumden2  23999  logbcl  24193  lgamgulmlem2  24593  lgamgulmlem3  24594  lgamgulmlem4  24595  lgamgulmlem5  24596  lgamgulmlem6  24597  lgamgulm2  24599  lgamcvg2  24618  gamcvg  24619  gamcvg2lem  24622  subfacval2  24652  divcnvlin  24991  fproddiv  25064  colinearalg  25563  axcontlem8  25624  bpolycl  25812  bpolysum  25813  bpolydiflem  25814  bpoly4  25819  iblmulc2nc  25970  ftc1cnnclem  25978  areacirclem2  25982  areacirclem5  25986  areacirc  25988  cntotbnd  26196  pellexlem2  26584  pellexlem6  26588  jm2.19  26755  jm2.27c  26769  proot1ex  27189  clim1fr1  27395  stoweidlem11  27428  stoweidlem26  27443  stoweidlem42  27459  wallispilem4  27485  wallispilem5  27486  wallispi  27487  wallispi2lem1  27488  wallispi2lem2  27489  wallispi2  27490  stirlinglem1  27491  stirlinglem3  27493  stirlinglem4  27494  stirlinglem5  27495  stirlinglem6  27496  stirlinglem7  27497  stirlinglem13  27503  stirlinglem14  27504  stirlinglem15  27505  sigardiv  27519  sharhght  27523  cotcl  27841
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641  ax-resscn 8980  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-addrcl 8984  ax-mulcl 8985  ax-mulrcl 8986  ax-mulcom 8987  ax-addass 8988  ax-mulass 8989  ax-distr 8990  ax-i2m1 8991  ax-1ne0 8992  ax-1rid 8993  ax-rnegex 8994  ax-rrecex 8995  ax-cnre 8996  ax-pre-lttri 8997  ax-pre-lttrn 8998  ax-pre-ltadd 8999  ax-pre-mulgt0 9000
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-nel 2553  df-ral 2654  df-rex 2655  df-reu 2656  df-rmo 2657  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-opab 4208  df-mpt 4209  df-id 4439  df-po 4444  df-so 4445  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-ov 6023  df-oprab 6024  df-mpt2 6025  df-riota 6485  df-er 6841  df-en 7046  df-dom 7047  df-sdom 7048  df-pnf 9055  df-mnf 9056  df-xr 9057  df-ltxr 9058  df-le 9059  df-sub 9225  df-neg 9226  df-div 9610
  Copyright terms: Public domain W3C validator