Theorem divcld 11922

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  (class class class)co 7360  ℂcc 11027  0cc0 11029   / cdiv 11798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799

This theorem is referenced by:  dmdcan2d  11952  mulsubdivbinom2  14215  hashf1  14410  abs1m  15289  abslem2  15293  sqreulem  15313  sqreu  15314  o1fsum  15767  divrcnv  15808  divcnv  15809  geolim  15826  geolim2  15827  geo2sum  15829  geo2lim  15831  fproddiv  15917  bpolycl  16008  bpolysum  16009  bpolydiflem  16010  bpoly4  16015  eftcl  16029  efaddlem  16049  tancl  16087  tanval2  16091  qredeq  16617  pcaddlem  16850  pjthlem1  25414  iblss  25782  itgeqa  25791  iblconst  25795  iblabsr  25807  iblmulc2  25808  itgsplit  25813  dvlem  25873  dvmulbr  25916  dvcobr  25923  dvrec  25932  dvrecg  25950  dvmptdiv  25951  dvcnvlem  25953  dveflem  25956  dvsincos  25958  dvlip  25970  c1liplem1  25973  lhop1lem  25990  lhop1  25991  lhop2  25992  lhop  25993  ftc1lem4  26016  vieta1lem2  26288  vieta1  26289  elqaalem3  26298  aareccl  26303  aalioulem1  26309  taylfvallem1  26333  tayl0  26338  taylply2  26344  taylply2OLD  26345  taylply  26346  dvtaylp  26347  taylthlem2  26351  taylthlem2OLD  26352  ulmdvlem1  26378  tanregt0  26516  eff1olem  26525  argregt0  26587  argrege0  26588  argimgt0  26589  logcnlem4  26622  advlogexp  26632  logtaylsum  26638  logtayl2  26639  root1eq1  26732  logbcl  26744  cxplogb  26763  logbf  26766  angcld  26782  angrteqvd  26783  cosangneg2d  26784  angrtmuld  26785  ang180lem1  26786  ang180lem2  26787  ang180lem3  26788  ang180lem4  26789  ang180lem5  26790  lawcoslem1  26792  lawcos  26793  isosctrlem2  26796  isosctrlem3  26797  angpieqvdlem  26805  angpieqvdlem2  26806  angpieqvd  26808  dcubic1lem  26820  dcubic2  26821  dcubic1  26822  dcubic  26823  mcubic  26824  cubic2  26825  dquartlem1  26828  dquartlem2  26829  dquart  26830  quart1cl  26831  quart1lem  26832  quart1  26833  quartlem3  26836  quartlem4  26837  quart  26838  tanatan  26896  atantayl  26914  atantayl2  26915  atantayl3  26916  log2cnv  26921  birthdaylem2  26929  efrlim  26946  efrlimOLD  26947  dfef2  26948  cxploglim2  26956  fsumharmonic  26989  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamgulmlem4  27009  lgamgulmlem5  27010  lgamgulmlem6  27011  lgamgulm2  27013  lgamcvg2  27032  gamcvg  27033  gamcvg2lem  27036  ftalem4  27053  ftalem5  27054  basellem8  27065  logexprlim  27202  bposlem9  27269  2lgslem3d  27376  2sqlem3  27397  dchrmusum2  27471  dchrvmasum2lem  27473  dchrvmasumiflem1  27478  dchrvmasumiflem2  27479  dchrvmaeq0  27481  dchrisum0re  27490  dchrisum0lem1b  27492  dchrisum0lem1  27493  dchrisum0lem2a  27494  dchrisum0lem2  27495  dchrisum0lem3  27496  dchrisum0  27497  mudivsum  27507  vmalogdivsum2  27515  vmalogdivsum  27516  2vmadivsumlem  27517  selberg2  27528  selberg3lem1  27534  selberg3  27536  selberg4lem1  27537  selbergr  27545  selberg3r  27546  selberg4r  27547  selberg34r  27548  pntrlog2bndlem1  27554  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  colinearalg  28993  axcontlem8  29054  nrt2irr  30558  pjhthlem1  31477  eigvalcl  32047  riesz3i  32148  quad3d  32837  bcm1n  32883  divnumden2  32904  zringfrac  33629  constrrtlc1  33892  constrrtcclem  33894  constrfin  33906  constrdircl  33925  constrreinvcl  33932  constrsqrtcl  33939  cos9thpiminplylem2  33943  cos9thpiminplylem3  33944  cos9thpiminply  33948  cos9thpinconstrlem1  33949  cos9thpinconstrlem2  33950  cos9thpinconstr  33951  oddpwdc  34514  signsplypnf  34710  signsply0  34711  itgexpif  34766  hgt750leme  34818  subfacval2  35385  divcnvlin  35931  bcprod  35936  iprodgam  35940  unbdqndv2lem1  36785  knoppndvlem2  36789  knoppndvlem7  36794  knoppndvlem9  36796  knoppndvlem10  36797  knoppndvlem16  36803  knoppndvlem17  36804  itg2addnclem  38006  iblmulc2nc  38020  ftc1cnnclem  38026  areacirclem1  38043  areacirclem4  38046  areacirc  38048  cntotbnd  38131  recbothd  42445  lcmineqlem12  42493  lcmineqlem18  42499  dvrelogpow2b  42521  aks4d1p1p2  42523  aks4d1p1p7  42527  aks6d1c2p2  42572  aks6d1c4  42577  2ap1caineq  42598  aks6d1c7lem1  42633  pellexlem2  43276  pellexlem6  43280  jm2.19  43439  jm2.27c  43453  proot1ex  43642  cvgdvgrat  44758  radcnvrat  44759  hashnzfzclim  44767  bcccl  44784  bccm1k  44787  binomcxplemrat  44795  binomcxplemfrat  44796  binomcxplemnotnn0  44801  xralrple2  45802  mccllem  46045  clim1fr1  46049  0ellimcdiv  46095  coseq0  46310  fperdvper  46365  dvdivbd  46369  dvnmptdivc  46384  dvnxpaek  46388  dvnprodlem2  46393  iblsplit  46412  itgcoscmulx  46415  itgsincmulx  46420  stoweidlem11  46457  stoweidlem26  46472  stoweidlem42  46488  wallispilem4  46514  wallispilem5  46515  wallispi  46516  wallispi2lem1  46517  wallispi2lem2  46518  wallispi2  46519  stirlinglem1  46520  stirlinglem3  46522  stirlinglem4  46523  stirlinglem5  46524  stirlinglem6  46525  stirlinglem7  46526  stirlinglem13  46532  stirlinglem14  46533  stirlinglem15  46534  dirkeritg  46548  dirkercncflem1  46549  dirkercncflem2  46550  fourierdlem26  46579  fourierdlem39  46592  fourierdlem56  46608  fourierdlem62  46614  fourierdlem72  46624  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem80  46632  fourierdlem103  46655  fourierdlem104  46656  fouriersw  46677  elaa2lem  46679  etransclem15  46695  etransclem20  46700  etransclem21  46701  etransclem22  46702  etransclem23  46703  etransclem24  46704  etransclem25  46705  etransclem31  46711  etransclem32  46712  etransclem33  46713  etransclem34  46714  etransclem35  46715  etransclem47  46727  etransclem48  46728  hoiqssbllem2  47069  sigardiv  47307  sharhght  47311  cndivrenred  47766  fmtnoprmfac2lem1  48041  quad1  48108  requad01  48109  requad1  48110  fdivmptf  49029  affinecomb2  49191  eenglngeehlnmlem1  49225  eenglngeehlnmlem2  49226  itscnhlc0xyqsol  49253  itschlc0xyqsol1  49254  cotcl  50239