Theorem divcld 11961

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

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		divcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		divcld.3	. 2 ⊢ (𝜑 → 𝐵 ≠ 0)
4		divcl 11845	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ)
5	1, 2, 3, 4	syl3anc 1389	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2141   ≠ wne 2956  (class class class)co 7391  ℂcc 11065  0cc0 11067   / cdiv 11838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411  df-div 11839

This theorem is referenced by:  dmdcan2d  11991  mulsubdivbinom2  14269  hashf1  14464  abs1m  15354  abslem2  15358  sqreulem  15378  sqreu  15379  o1fsum  15832  divrcnv  15873  divcnv  15874  geolim  15891  geolim2  15892  geo2sum  15894  geo2lim  15896  fproddiv  15982  bpolycl  16073  bpolysum  16074  bpolydiflem  16075  bpoly4  16080  eftcl  16094  efaddlem  16114  tancl  16152  tanval2  16156  qredeq  16682  pcaddlem  16915  pjthlem1  25487  iblss  25855  itgeqa  25864  iblconst  25868  iblabsr  25880  iblmulc2  25881  itgsplit  25886  dvlem  25946  dvmulbr  25989  dvcobr  25996  dvrec  26005  dvrecg  26023  dvmptdiv  26024  dvcnvlem  26026  dveflem  26029  dvsincos  26031  dvlip  26043  c1liplem1  26046  lhop1lem  26063  lhop1  26064  lhop2  26065  lhop  26066  ftc1lem4  26089  vieta1lem2  26363  vieta1  26364  elqaalem3  26373  aareccl  26378  aalioulem1  26384  taylfvallem1  26408  tayl0  26413  taylply2  26419  taylply  26420  dvtaylp  26421  taylthlem2  26425  ulmdvlem1  26451  tanregt0  26592  eff1olem  26601  argregt0  26663  argrege0  26664  argimgt0  26665  logcnlem4  26698  advlogexp  26708  logtaylsum  26714  logtayl2  26715  root1eq1  26808  logbcl  26820  cxplogb  26839  logbf  26842  angcld  26858  angrteqvd  26859  cosangneg2d  26860  angrtmuld  26861  ang180lem1  26862  ang180lem2  26863  ang180lem3  26864  ang180lem4  26865  ang180lem5  26866  lawcoslem1  26868  lawcos  26869  isosctrlem2  26872  isosctrlem3  26873  angpieqvdlem  26881  angpieqvdlem2  26882  angpieqvd  26884  dcubic1lem  26896  dcubic2  26897  dcubic1  26898  dcubic  26899  mcubic  26900  cubic2  26901  dquartlem1  26904  dquartlem2  26905  dquart  26906  quart1cl  26907  quart1lem  26908  quart1  26909  quartlem3  26912  quartlem4  26913  quart  26914  tanatan  26972  atantayl  26990  atantayl2  26991  atantayl3  26992  log2cnv  26997  birthdaylem2  27005  efrlim  27022  dfef2  27023  cxploglim2  27031  fsumharmonic  27064  lgamgulmlem2  27082  lgamgulmlem3  27083  lgamgulmlem4  27084  lgamgulmlem5  27085  lgamgulmlem6  27086  lgamgulm2  27088  lgamcvg2  27107  gamcvg  27108  gamcvg2lem  27111  ftalem4  27128  ftalem5  27129  basellem8  27140  logexprlim  27277  bposlem9  27344  2lgslem3d  27451  2sqlem3  27472  dchrmusum2  27546  dchrvmasum2lem  27548  dchrvmasumiflem1  27553  dchrvmasumiflem2  27554  dchrvmaeq0  27556  dchrisum0re  27565  dchrisum0lem1b  27567  dchrisum0lem1  27568  dchrisum0lem2a  27569  dchrisum0lem2  27570  dchrisum0lem3  27571  dchrisum0  27572  mudivsum  27582  vmalogdivsum2  27590  vmalogdivsum  27591  2vmadivsumlem  27592  selberg2  27603  selberg3lem1  27609  selberg3  27611  selberg4lem1  27612  selbergr  27620  selberg3r  27621  selberg4r  27622  selberg34r  27623  pntrlog2bndlem1  27629  pntrlog2bndlem2  27630  pntrlog2bndlem3  27631  pntrlog2bndlem4  27632  pntrlog2bndlem5  27633  colinearalg  29068  axcontlem8  29129  nrt2irr  30632  pjhthlem1  31551  eigvalcl  32121  riesz3i  32222  quad3d  32912  bcm1n  32958  divnumden2  32979  zringfrac  33711  constrrtlc1  33990  constrrtcclem  33992  constrfin  34004  constrdircl  34023  constrreinvcl  34030  constrsqrtcl  34037  cos9thpiminplylem2  34041  cos9thpiminplylem3  34042  cos9thpiminply  34046  cos9thpinconstrlem1  34047  cos9thpinconstrlem2  34048  cos9thpinconstr  34049  oddpwdc  34612  signsplypnf  34805  signsply0  34806  itgexpif  34861  hgt750leme  34913  subfacval2  35498  divcnvlin  36044  bcprod  36049  iprodgam  36053  unbdqndv2lem1  36908  knoppndvlem2  36912  knoppndvlem7  36917  knoppndvlem9  36919  knoppndvlem10  36920  knoppndvlem16  36926  knoppndvlem17  36927  itg2addnclem  38131  iblmulc2nc  38145  ftc1cnnclem  38151  areacirclem1  38168  areacirclem4  38171  areacirc  38173  cntotbnd  38256  recbothd  42570  lcmineqlem12  42618  lcmineqlem18  42624  dvrelogpow2b  42646  aks4d1p1p2  42648  aks4d1p1p7  42652  aks6d1c2p2  42697  aks6d1c4  42702  2ap1caineq  42723  aks6d1c7lem1  42758  pellexlem2  43368  pellexlem6  43372  jm2.19  43531  jm2.27c  43545  proot1ex  43734  cvgdvgrat  44850  radcnvrat  44851  hashnzfzclim  44859  bcccl  44876  bccm1k  44879  binomcxplemrat  44887  binomcxplemfrat  44888  binomcxplemnotnn0  44893  xralrple2  45891  mccllem  46134  clim1fr1  46138  0ellimcdiv  46184  coseq0  46399  fperdvper  46454  dvdivbd  46458  dvnmptdivc  46473  dvnxpaek  46477  dvnprodlem2  46482  iblsplit  46501  itgcoscmulx  46504  itgsincmulx  46509  stoweidlem11  46546  stoweidlem26  46561  stoweidlem42  46577  wallispilem4  46603  wallispilem5  46604  wallispi  46605  wallispi2lem1  46606  wallispi2lem2  46607  wallispi2  46608  stirlinglem1  46609  stirlinglem3  46611  stirlinglem4  46612  stirlinglem5  46613  stirlinglem6  46614  stirlinglem7  46615  stirlinglem13  46621  stirlinglem14  46622  stirlinglem15  46623  dirkeritg  46637  dirkercncflem1  46638  dirkercncflem2  46639  fourierdlem26  46668  fourierdlem39  46681  fourierdlem56  46697  fourierdlem62  46703  fourierdlem72  46713  fourierdlem74  46715  fourierdlem75  46716  fourierdlem76  46717  fourierdlem80  46721  fourierdlem103  46744  fourierdlem104  46745  fouriersw  46766  elaa2lem  46768  etransclem15  46784  etransclem20  46789  etransclem21  46790  etransclem22  46791  etransclem23  46792  etransclem24  46793  etransclem25  46794  etransclem31  46800  etransclem32  46801  etransclem33  46802  etransclem34  46803  etransclem35  46804  etransclem47  46816  etransclem48  46817  hoiqssbllem2  47158  sigardiv  47396  sharhght  47400  cndivrenred  47861  fmtnoprmfac2lem1  48136  quad1  48203  requad01  48204  requad1  48205  fdivmptf  49124  affinecomb2  49286  eenglngeehlnmlem1  49320  eenglngeehlnmlem2  49321  itscnhlc0xyqsol  49348  itschlc0xyqsol1  49349  cotcl  50334