Theorem divcld 11934

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925  (class class class)co 7369  ℂcc 11042  0cc0 11044   / cdiv 11811

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

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 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812

This theorem is referenced by:  dmdcan2d  11964  mulsubdivbinom2  14203  hashf1  14398  abs1m  15278  abslem2  15282  sqreulem  15302  sqreu  15303  o1fsum  15755  divrcnv  15794  divcnv  15795  geolim  15812  geolim2  15813  geo2sum  15815  geo2lim  15817  fproddiv  15903  bpolycl  15994  bpolysum  15995  bpolydiflem  15996  bpoly4  16001  eftcl  16015  efaddlem  16035  tancl  16073  tanval2  16077  qredeq  16603  pcaddlem  16835  pjthlem1  25313  iblss  25682  itgeqa  25691  iblconst  25695  iblabsr  25707  iblmulc2  25708  itgsplit  25713  dvlem  25773  dvmulbr  25817  dvmulbrOLD  25818  dvcobr  25825  dvcobrOLD  25826  dvrec  25835  dvrecg  25853  dvmptdiv  25854  dvcnvlem  25856  dveflem  25859  dvsincos  25861  dvlip  25874  c1liplem1  25877  lhop1lem  25894  lhop1  25895  lhop2  25896  lhop  25897  ftc1lem4  25922  vieta1lem2  26195  vieta1  26196  elqaalem3  26205  aareccl  26210  aalioulem1  26216  taylfvallem1  26240  tayl0  26245  taylply2  26251  taylply2OLD  26252  taylply  26253  dvtaylp  26254  taylthlem2  26258  taylthlem2OLD  26259  ulmdvlem1  26285  tanregt0  26424  eff1olem  26433  argregt0  26495  argrege0  26496  argimgt0  26497  logcnlem4  26530  advlogexp  26540  logtaylsum  26546  logtayl2  26547  root1eq1  26641  logbcl  26653  cxplogb  26672  logbf  26675  angcld  26691  angrteqvd  26692  cosangneg2d  26693  angrtmuld  26694  ang180lem1  26695  ang180lem2  26696  ang180lem3  26697  ang180lem4  26698  ang180lem5  26699  lawcoslem1  26701  lawcos  26702  isosctrlem2  26705  isosctrlem3  26706  angpieqvdlem  26714  angpieqvdlem2  26715  angpieqvd  26717  dcubic1lem  26729  dcubic2  26730  dcubic1  26731  dcubic  26732  mcubic  26733  cubic2  26734  dquartlem1  26737  dquartlem2  26738  dquart  26739  quart1cl  26740  quart1lem  26741  quart1  26742  quartlem3  26745  quartlem4  26746  quart  26747  tanatan  26805  atantayl  26823  atantayl2  26824  atantayl3  26825  log2cnv  26830  birthdaylem2  26838  efrlim  26855  efrlimOLD  26856  dfef2  26857  cxploglim2  26865  fsumharmonic  26898  lgamgulmlem2  26916  lgamgulmlem3  26917  lgamgulmlem4  26918  lgamgulmlem5  26919  lgamgulmlem6  26920  lgamgulm2  26922  lgamcvg2  26941  gamcvg  26942  gamcvg2lem  26945  ftalem4  26962  ftalem5  26963  basellem8  26974  logexprlim  27112  bposlem9  27179  2lgslem3d  27286  2sqlem3  27307  dchrmusum2  27381  dchrvmasum2lem  27383  dchrvmasumiflem1  27388  dchrvmasumiflem2  27389  dchrvmaeq0  27391  dchrisum0re  27400  dchrisum0lem1b  27402  dchrisum0lem1  27403  dchrisum0lem2a  27404  dchrisum0lem2  27405  dchrisum0lem3  27406  dchrisum0  27407  mudivsum  27417  vmalogdivsum2  27425  vmalogdivsum  27426  2vmadivsumlem  27427  selberg2  27438  selberg3lem1  27444  selberg3  27446  selberg4lem1  27447  selbergr  27455  selberg3r  27456  selberg4r  27457  selberg34r  27458  pntrlog2bndlem1  27464  pntrlog2bndlem2  27465  pntrlog2bndlem3  27466  pntrlog2bndlem4  27467  pntrlog2bndlem5  27468  colinearalg  28813  axcontlem8  28874  nrt2irr  30375  pjhthlem1  31293  eigvalcl  31863  riesz3i  31964  quad3d  32646  bcm1n  32691  divnumden2  32713  zringfrac  33498  constrrtlc1  33695  constrrtcclem  33697  constrfin  33709  constrdircl  33728  constrreinvcl  33735  constrsqrtcl  33742  cos9thpiminplylem2  33746  cos9thpiminplylem3  33747  cos9thpiminply  33751  cos9thpinconstrlem1  33752  cos9thpinconstrlem2  33753  cos9thpinconstr  33754  oddpwdc  34318  signsplypnf  34514  signsply0  34515  itgexpif  34570  hgt750leme  34622  subfacval2  35147  divcnvlin  35693  bcprod  35698  iprodgam  35702  unbdqndv2lem1  36470  knoppndvlem2  36474  knoppndvlem7  36479  knoppndvlem9  36481  knoppndvlem10  36482  knoppndvlem16  36488  knoppndvlem17  36489  itg2addnclem  37638  iblmulc2nc  37652  ftc1cnnclem  37658  areacirclem1  37675  areacirclem4  37678  areacirc  37680  cntotbnd  37763  recbothd  41953  lcmineqlem12  42001  lcmineqlem18  42007  dvrelogpow2b  42029  aks4d1p1p2  42031  aks4d1p1p7  42035  aks6d1c2p2  42080  aks6d1c4  42085  2ap1caineq  42106  aks6d1c7lem1  42141  pellexlem2  42791  pellexlem6  42795  jm2.19  42955  jm2.27c  42969  proot1ex  43158  cvgdvgrat  44275  radcnvrat  44276  hashnzfzclim  44284  bcccl  44301  bccm1k  44304  binomcxplemrat  44312  binomcxplemfrat  44313  binomcxplemnotnn0  44318  xralrple2  45323  mccllem  45568  clim1fr1  45572  0ellimcdiv  45620  coseq0  45835  fperdvper  45890  dvdivbd  45894  dvnmptdivc  45909  dvnxpaek  45913  dvnprodlem2  45918  iblsplit  45937  itgcoscmulx  45940  itgsincmulx  45945  stoweidlem11  45982  stoweidlem26  45997  stoweidlem42  46013  wallispilem4  46039  wallispilem5  46040  wallispi  46041  wallispi2lem1  46042  wallispi2lem2  46043  wallispi2  46044  stirlinglem1  46045  stirlinglem3  46047  stirlinglem4  46048  stirlinglem5  46049  stirlinglem6  46050  stirlinglem7  46051  stirlinglem13  46057  stirlinglem14  46058  stirlinglem15  46059  dirkeritg  46073  dirkercncflem1  46074  dirkercncflem2  46075  fourierdlem26  46104  fourierdlem39  46117  fourierdlem56  46133  fourierdlem62  46139  fourierdlem72  46149  fourierdlem74  46151  fourierdlem75  46152  fourierdlem76  46153  fourierdlem80  46157  fourierdlem103  46180  fourierdlem104  46181  fouriersw  46202  elaa2lem  46204  etransclem15  46220  etransclem20  46225  etransclem21  46226  etransclem22  46227  etransclem23  46228  etransclem24  46229  etransclem25  46230  etransclem31  46236  etransclem32  46237  etransclem33  46238  etransclem34  46239  etransclem35  46240  etransclem47  46252  etransclem48  46253  hoiqssbllem2  46594  sigardiv  46832  sharhght  46836  cndivrenred  47280  fmtnoprmfac2lem1  47540  quad1  47594  requad01  47595  requad1  47596  fdivmptf  48503  affinecomb2  48665  eenglngeehlnmlem1  48699  eenglngeehlnmlem2  48700  itscnhlc0xyqsol  48727  itschlc0xyqsol1  48728  cotcl  49714