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

Theorem divcld 10345
Description: Closure law for division. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
div1d.1
divcld.2
divcld.3
Assertion
Ref Expression
divcld

Proof of Theorem divcld
StepHypRef Expression
1 div1d.1 . 2
2 divcld.2 . 2
3 divcld.3 . 2
4 divcl 10238 . 2
51, 2, 3, 4syl3anc 1228 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  =/=wne 2652  (class class class)co 6296   cc 9511  0cc0 9513   cdiv 10231
This theorem is referenced by:  dmdcan2d  10375  hashf1  12506  abs1m  13168  abslem2  13172  sqreulem  13192  sqreu  13193  o1fsum  13627  divrcnv  13664  divcnv  13665  geolim  13679  geolim2  13680  geo2sum  13682  geo2lim  13684  fproddiv  13766  eftcl  13809  efaddlem  13828  tancl  13864  tanval2  13868  qredeq  14247  pcaddlem  14407  pjthlem1  21852  iblss  22211  itgeqa  22220  iblconst  22224  iblabsr  22236  iblmulc2  22237  itgsplit  22242  dvlem  22300  dvmulbr  22342  dvcobr  22349  dvrec  22358  dvcnvlem  22377  dveflem  22380  dvsincos  22382  dvlip  22394  c1liplem1  22397  lhop1lem  22414  lhop1  22415  lhop2  22416  lhop  22417  ftc1lem4  22440  vieta1lem2  22707  vieta1  22708  elqaalem3  22717  aareccl  22722  aalioulem1  22728  taylfvallem1  22752  tayl0  22757  taylply2  22763  taylply  22764  dvtaylp  22765  taylthlem2  22769  ulmdvlem1  22795  tanregt0  22926  eff1olem  22935  argregt0  22995  argrege0  22996  argimgt0  22997  logcnlem4  23026  advlogexp  23036  logtaylsum  23042  logtayl2  23043  root1eq1  23129  angcld  23137  angrteqvd  23138  cosangneg2d  23139  angrtmuld  23140  ang180lem1  23141  ang180lem2  23142  ang180lem3  23143  ang180lem4  23144  ang180lem5  23145  lawcoslem1  23147  lawcos  23148  isosctrlem2  23153  isosctrlem3  23154  angpieqvdlem  23159  angpieqvdlem2  23160  angpieqvd  23162  dcubic1lem  23174  dcubic2  23175  dcubic1  23176  dcubic  23177  mcubic  23178  cubic2  23179  dquartlem1  23182  dquartlem2  23183  dquart  23184  quart1cl  23185  quart1lem  23186  quart1  23187  quartlem3  23190  quartlem4  23191  quart  23192  tanatan  23250  atantayl  23268  atantayl2  23269  atantayl3  23270  log2cnv  23275  birthdaylem2  23282  efrlim  23299  dfef2  23300  cxploglim2  23308  fsumharmonic  23341  ftalem4  23349  ftalem5  23350  basellem8  23361  logexprlim  23500  bposlem9  23567  2sqlem3  23641  dchrmusum2  23679  dchrvmasum2lem  23681  dchrvmasumiflem1  23686  dchrvmasumiflem2  23687  dchrvmaeq0  23689  dchrisum0re  23698  dchrisum0lem1b  23700  dchrisum0lem1  23701  dchrisum0lem2a  23702  dchrisum0lem2  23703  dchrisum0lem3  23704  dchrisum0  23705  mudivsum  23715  vmalogdivsum2  23723  vmalogdivsum  23724  2vmadivsumlem  23725  selberg2  23736  selberg3lem1  23742  selberg3  23744  selberg4lem1  23745  selbergr  23753  selberg3r  23754  selberg4r  23755  selberg34r  23756  pntrlog2bndlem1  23762  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  colinearalg  24213  axcontlem8  24274  pjhthlem1  26309  eigvalcl  26880  riesz3i  26981  bcm1n  27600  divnumden2  27609  logbcl  28013  oddpwdc  28293  signsplypnf  28507  signsply0  28508  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem4  28574  lgamgulmlem5  28575  lgamgulmlem6  28576  lgamgulm2  28578  lgamcvg2  28597  gamcvg  28598  gamcvg2lem  28601  subfacval2  28631  divcnvlin  29118  iprodgam  29125  bpolycl  29814  bpolysum  29815  bpolydiflem  29816  bpoly4  29821  itg2addnclem  30066  iblmulc2nc  30080  ftc1cnnclem  30088  areacirclem1  30107  areacirclem4  30110  areacirc  30112  cntotbnd  30292  pellexlem2  30766  pellexlem6  30770  jm2.19  30935  jm2.27c  30949  proot1ex  31161  cvgdvgrat  31194  radcnvrat  31195  hashnzfzclim  31227  bcccl  31244  bccm1k  31247  binomcxplemrat  31255  binomcxplemfrat  31256  binomcxplemnotnn0  31261  mccllem  31605  clim1fr1  31607  0ellimcdiv  31655  coseq0  31664  dvrecg  31707  dvmptdiv  31714  fperdvper  31715  dvdivbd  31720  dvnmptdivc  31735  dvnxpaek  31739  dvnprodlem2  31744  iblsplit  31765  itgcoscmulx  31768  itgsincmulx  31773  stoweidlem11  31793  stoweidlem26  31808  stoweidlem42  31824  wallispilem4  31850  wallispilem5  31851  wallispi  31852  wallispi2lem1  31853  wallispi2lem2  31854  wallispi2  31855  stirlinglem1  31856  stirlinglem3  31858  stirlinglem4  31859  stirlinglem5  31860  stirlinglem6  31861  stirlinglem7  31862  stirlinglem13  31868  stirlinglem14  31869  stirlinglem15  31870  dirkeritg  31884  dirkercncflem1  31885  dirkercncflem2  31886  fourierdlem26  31915  fourierdlem39  31928  fourierdlem56  31945  fourierdlem62  31951  fourierdlem72  31961  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem80  31969  fourierdlem103  31992  fourierdlem104  31993  fouriersw  32014  elaa2lem  32016  etransclem15  32032  etransclem20  32037  etransclem21  32038  etransclem22  32039  etransclem23  32040  etransclem24  32041  etransclem25  32042  etransclem31  32048  etransclem32  32049  etransclem33  32050  etransclem34  32051  etransclem35  32052  etransclem47  32064  etransclem48  32065  sigardiv  32078  sharhght  32082  cotcl  33146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-po 4805  df-so 4806  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-div 10232
  Copyright terms: Public domain W3C validator