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

Theorem divcld 10786
Description: Closure law for division. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
div1d.1 (𝜑𝐴 ∈ ℂ)
divcld.2 (𝜑𝐵 ∈ ℂ)
divcld.3 (𝜑𝐵 ≠ 0)
Assertion
Ref Expression
divcld (𝜑 → (𝐴 / 𝐵) ∈ ℂ)

Proof of Theorem divcld
StepHypRef Expression
1 div1d.1 . 2 (𝜑𝐴 ∈ ℂ)
2 divcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 divcld.3 . 2 (𝜑𝐵 ≠ 0)
4 divcl 10676 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ)
51, 2, 3, 4syl3anc 1324 1 (𝜑 → (𝐴 / 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  wne 2791  (class class class)co 6635  cc 9919  0cc0 9921   / cdiv 10669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-po 5025  df-so 5026  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670
This theorem is referenced by:  dmdcan2d  10816  mulsubdivbinom2  13029  hashf1  13224  abs1m  14056  abslem2  14060  sqreulem  14080  sqreu  14081  o1fsum  14526  divrcnv  14565  divcnv  14566  geolim  14582  geolim2  14583  geo2sum  14585  geo2lim  14587  fproddiv  14672  bpolycl  14764  bpolysum  14765  bpolydiflem  14766  bpoly4  14771  eftcl  14785  efaddlem  14804  tancl  14840  tanval2  14844  qredeq  15352  pcaddlem  15573  pjthlem1  23189  iblss  23552  itgeqa  23561  iblconst  23565  iblabsr  23577  iblmulc2  23578  itgsplit  23583  dvlem  23641  dvmulbr  23683  dvcobr  23690  dvrec  23699  dvrecg  23717  dvmptdiv  23718  dvcnvlem  23720  dveflem  23723  dvsincos  23725  dvlip  23737  c1liplem1  23740  lhop1lem  23757  lhop1  23758  lhop2  23759  lhop  23760  ftc1lem4  23783  vieta1lem2  24047  vieta1  24048  elqaalem3  24057  aareccl  24062  aalioulem1  24068  taylfvallem1  24092  tayl0  24097  taylply2  24103  taylply  24104  dvtaylp  24105  taylthlem2  24109  ulmdvlem1  24135  tanregt0  24266  eff1olem  24275  argregt0  24337  argrege0  24338  argimgt0  24339  logcnlem4  24372  advlogexp  24382  logtaylsum  24388  logtayl2  24389  root1eq1  24477  logbcl  24486  cxplogb  24505  logbf  24508  angcld  24516  angrteqvd  24517  cosangneg2d  24518  angrtmuld  24519  ang180lem1  24520  ang180lem2  24521  ang180lem3  24522  ang180lem4  24523  ang180lem5  24524  lawcoslem1  24526  lawcos  24527  isosctrlem2  24530  isosctrlem3  24531  angpieqvdlem  24536  angpieqvdlem2  24537  angpieqvd  24539  dcubic1lem  24551  dcubic2  24552  dcubic1  24553  dcubic  24554  mcubic  24555  cubic2  24556  dquartlem1  24559  dquartlem2  24560  dquart  24561  quart1cl  24562  quart1lem  24563  quart1  24564  quartlem3  24567  quartlem4  24568  quart  24569  tanatan  24627  atantayl  24645  atantayl2  24646  atantayl3  24647  log2cnv  24652  birthdaylem2  24660  efrlim  24677  dfef2  24678  cxploglim2  24686  fsumharmonic  24719  lgamgulmlem2  24737  lgamgulmlem3  24738  lgamgulmlem4  24739  lgamgulmlem5  24740  lgamgulmlem6  24741  lgamgulm2  24743  lgamcvg2  24762  gamcvg  24763  gamcvg2lem  24766  ftalem4  24783  ftalem5  24784  basellem8  24795  logexprlim  24931  bposlem9  24998  2lgslem3d  25105  2sqlem3  25126  dchrmusum2  25164  dchrvmasum2lem  25166  dchrvmasumiflem1  25171  dchrvmasumiflem2  25172  dchrvmaeq0  25174  dchrisum0re  25183  dchrisum0lem1b  25185  dchrisum0lem1  25186  dchrisum0lem2a  25187  dchrisum0lem2  25188  dchrisum0lem3  25189  dchrisum0  25190  mudivsum  25200  vmalogdivsum2  25208  vmalogdivsum  25209  2vmadivsumlem  25210  selberg2  25221  selberg3lem1  25227  selberg3  25229  selberg4lem1  25230  selbergr  25238  selberg3r  25239  selberg4r  25240  selberg34r  25241  pntrlog2bndlem1  25247  pntrlog2bndlem2  25248  pntrlog2bndlem3  25249  pntrlog2bndlem4  25250  pntrlog2bndlem5  25251  colinearalg  25771  axcontlem8  25832  pjhthlem1  28220  eigvalcl  28790  riesz3i  28891  bcm1n  29528  divnumden2  29538  oddpwdc  30390  signsplypnf  30601  signsply0  30602  itgexpif  30658  hgt750leme  30710  subfacval2  31143  divcnvlin  31593  bcprod  31599  iprodgam  31603  unbdqndv2lem1  32475  knoppndvlem2  32479  knoppndvlem7  32484  knoppndvlem9  32486  knoppndvlem10  32487  knoppndvlem16  32493  knoppndvlem17  32494  itg2addnclem  33432  iblmulc2nc  33446  ftc1cnnclem  33454  areacirclem1  33471  areacirclem4  33474  areacirc  33476  cntotbnd  33566  pellexlem2  37213  pellexlem6  37217  jm2.19  37379  jm2.27c  37393  proot1ex  37598  cvgdvgrat  38332  radcnvrat  38333  hashnzfzclim  38341  bcccl  38358  bccm1k  38361  binomcxplemrat  38369  binomcxplemfrat  38370  binomcxplemnotnn0  38375  xralrple2  39383  mccllem  39629  clim1fr1  39633  0ellimcdiv  39681  coseq0  39838  fperdvper  39896  dvdivbd  39901  dvnmptdivc  39916  dvnxpaek  39920  dvnprodlem2  39925  iblsplit  39945  itgcoscmulx  39948  itgsincmulx  39953  stoweidlem11  39991  stoweidlem26  40006  stoweidlem42  40022  wallispilem4  40048  wallispilem5  40049  wallispi  40050  wallispi2lem1  40051  wallispi2lem2  40052  wallispi2  40053  stirlinglem1  40054  stirlinglem3  40056  stirlinglem4  40057  stirlinglem5  40058  stirlinglem6  40059  stirlinglem7  40060  stirlinglem13  40066  stirlinglem14  40067  stirlinglem15  40068  dirkeritg  40082  dirkercncflem1  40083  dirkercncflem2  40084  fourierdlem26  40113  fourierdlem39  40126  fourierdlem56  40142  fourierdlem62  40148  fourierdlem72  40158  fourierdlem74  40160  fourierdlem75  40161  fourierdlem76  40162  fourierdlem80  40166  fourierdlem103  40189  fourierdlem104  40190  fouriersw  40211  elaa2lem  40213  etransclem15  40229  etransclem20  40234  etransclem21  40235  etransclem22  40236  etransclem23  40237  etransclem24  40238  etransclem25  40239  etransclem31  40245  etransclem32  40246  etransclem33  40247  etransclem34  40248  etransclem35  40249  etransclem47  40261  etransclem48  40262  hoiqssbllem2  40600  sigardiv  40813  sharhght  40817  fmtnoprmfac2lem1  41243  fdivmptf  42100  cotcl  42258
  Copyright terms: Public domain W3C validator