Theorem divcld 11919

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 11804	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ)
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925  (class class class)co 7353  ℂcc 11026  0cc0 11028   / cdiv 11796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-div 11797

This theorem is referenced by:  dmdcan2d  11949  mulsubdivbinom2  14188  hashf1  14383  abs1m  15262  abslem2  15266  sqreulem  15286  sqreu  15287  o1fsum  15739  divrcnv  15778  divcnv  15779  geolim  15796  geolim2  15797  geo2sum  15799  geo2lim  15801  fproddiv  15887  bpolycl  15978  bpolysum  15979  bpolydiflem  15980  bpoly4  15985  eftcl  15999  efaddlem  16019  tancl  16057  tanval2  16061  qredeq  16587  pcaddlem  16819  pjthlem1  25354  iblss  25723  itgeqa  25732  iblconst  25736  iblabsr  25748  iblmulc2  25749  itgsplit  25754  dvlem  25814  dvmulbr  25858  dvmulbrOLD  25859  dvcobr  25866  dvcobrOLD  25867  dvrec  25876  dvrecg  25894  dvmptdiv  25895  dvcnvlem  25897  dveflem  25900  dvsincos  25902  dvlip  25915  c1liplem1  25918  lhop1lem  25935  lhop1  25936  lhop2  25937  lhop  25938  ftc1lem4  25963  vieta1lem2  26236  vieta1  26237  elqaalem3  26246  aareccl  26251  aalioulem1  26257  taylfvallem1  26281  tayl0  26286  taylply2  26292  taylply2OLD  26293  taylply  26294  dvtaylp  26295  taylthlem2  26299  taylthlem2OLD  26300  ulmdvlem1  26326  tanregt0  26465  eff1olem  26474  argregt0  26536  argrege0  26537  argimgt0  26538  logcnlem4  26571  advlogexp  26581  logtaylsum  26587  logtayl2  26588  root1eq1  26682  logbcl  26694  cxplogb  26713  logbf  26716  angcld  26732  angrteqvd  26733  cosangneg2d  26734  angrtmuld  26735  ang180lem1  26736  ang180lem2  26737  ang180lem3  26738  ang180lem4  26739  ang180lem5  26740  lawcoslem1  26742  lawcos  26743  isosctrlem2  26746  isosctrlem3  26747  angpieqvdlem  26755  angpieqvdlem2  26756  angpieqvd  26758  dcubic1lem  26770  dcubic2  26771  dcubic1  26772  dcubic  26773  mcubic  26774  cubic2  26775  dquartlem1  26778  dquartlem2  26779  dquart  26780  quart1cl  26781  quart1lem  26782  quart1  26783  quartlem3  26786  quartlem4  26787  quart  26788  tanatan  26846  atantayl  26864  atantayl2  26865  atantayl3  26866  log2cnv  26871  birthdaylem2  26879  efrlim  26896  efrlimOLD  26897  dfef2  26898  cxploglim2  26906  fsumharmonic  26939  lgamgulmlem2  26957  lgamgulmlem3  26958  lgamgulmlem4  26959  lgamgulmlem5  26960  lgamgulmlem6  26961  lgamgulm2  26963  lgamcvg2  26982  gamcvg  26983  gamcvg2lem  26986  ftalem4  27003  ftalem5  27004  basellem8  27015  logexprlim  27153  bposlem9  27220  2lgslem3d  27327  2sqlem3  27348  dchrmusum2  27422  dchrvmasum2lem  27424  dchrvmasumiflem1  27429  dchrvmasumiflem2  27430  dchrvmaeq0  27432  dchrisum0re  27441  dchrisum0lem1b  27443  dchrisum0lem1  27444  dchrisum0lem2a  27445  dchrisum0lem2  27446  dchrisum0lem3  27447  dchrisum0  27448  mudivsum  27458  vmalogdivsum2  27466  vmalogdivsum  27467  2vmadivsumlem  27468  selberg2  27479  selberg3lem1  27485  selberg3  27487  selberg4lem1  27488  selbergr  27496  selberg3r  27497  selberg4r  27498  selberg34r  27499  pntrlog2bndlem1  27505  pntrlog2bndlem2  27506  pntrlog2bndlem3  27507  pntrlog2bndlem4  27508  pntrlog2bndlem5  27509  colinearalg  28874  axcontlem8  28935  nrt2irr  30436  pjhthlem1  31354  eigvalcl  31924  riesz3i  32025  quad3d  32712  bcm1n  32757  divnumden2  32779  zringfrac  33510  constrrtlc1  33718  constrrtcclem  33720  constrfin  33732  constrdircl  33751  constrreinvcl  33758  constrsqrtcl  33765  cos9thpiminplylem2  33769  cos9thpiminplylem3  33770  cos9thpiminply  33774  cos9thpinconstrlem1  33775  cos9thpinconstrlem2  33776  cos9thpinconstr  33777  oddpwdc  34341  signsplypnf  34537  signsply0  34538  itgexpif  34593  hgt750leme  34645  subfacval2  35179  divcnvlin  35725  bcprod  35730  iprodgam  35734  unbdqndv2lem1  36502  knoppndvlem2  36506  knoppndvlem7  36511  knoppndvlem9  36513  knoppndvlem10  36514  knoppndvlem16  36520  knoppndvlem17  36521  itg2addnclem  37670  iblmulc2nc  37684  ftc1cnnclem  37690  areacirclem1  37707  areacirclem4  37710  areacirc  37712  cntotbnd  37795  recbothd  41985  lcmineqlem12  42033  lcmineqlem18  42039  dvrelogpow2b  42061  aks4d1p1p2  42063  aks4d1p1p7  42067  aks6d1c2p2  42112  aks6d1c4  42117  2ap1caineq  42138  aks6d1c7lem1  42173  pellexlem2  42823  pellexlem6  42827  jm2.19  42986  jm2.27c  43000  proot1ex  43189  cvgdvgrat  44306  radcnvrat  44307  hashnzfzclim  44315  bcccl  44332  bccm1k  44335  binomcxplemrat  44343  binomcxplemfrat  44344  binomcxplemnotnn0  44349  xralrple2  45354  mccllem  45598  clim1fr1  45602  0ellimcdiv  45650  coseq0  45865  fperdvper  45920  dvdivbd  45924  dvnmptdivc  45939  dvnxpaek  45943  dvnprodlem2  45948  iblsplit  45967  itgcoscmulx  45970  itgsincmulx  45975  stoweidlem11  46012  stoweidlem26  46027  stoweidlem42  46043  wallispilem4  46069  wallispilem5  46070  wallispi  46071  wallispi2lem1  46072  wallispi2lem2  46073  wallispi2  46074  stirlinglem1  46075  stirlinglem3  46077  stirlinglem4  46078  stirlinglem5  46079  stirlinglem6  46080  stirlinglem7  46081  stirlinglem13  46087  stirlinglem14  46088  stirlinglem15  46089  dirkeritg  46103  dirkercncflem1  46104  dirkercncflem2  46105  fourierdlem26  46134  fourierdlem39  46147  fourierdlem56  46163  fourierdlem62  46169  fourierdlem72  46179  fourierdlem74  46181  fourierdlem75  46182  fourierdlem76  46183  fourierdlem80  46187  fourierdlem103  46210  fourierdlem104  46211  fouriersw  46232  elaa2lem  46234  etransclem15  46250  etransclem20  46255  etransclem21  46256  etransclem22  46257  etransclem23  46258  etransclem24  46259  etransclem25  46260  etransclem31  46266  etransclem32  46267  etransclem33  46268  etransclem34  46269  etransclem35  46270  etransclem47  46282  etransclem48  46283  hoiqssbllem2  46624  sigardiv  46862  sharhght  46866  cndivrenred  47310  fmtnoprmfac2lem1  47570  quad1  47624  requad01  47625  requad1  47626  fdivmptf  48546  affinecomb2  48708  eenglngeehlnmlem1  48742  eenglngeehlnmlem2  48743  itscnhlc0xyqsol  48770  itschlc0xyqsol1  48771  cotcl  49757