Theorem divcld 11987

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

Syntax hints:   → wi 4   ∈ wcel 2149   ≠ wne 2964  (class class class)co 7408  ℂcc 11094  0cc0 11096   / cdiv 11867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-div 11868

This theorem is referenced by:  dmdcan2d  12017  mulsubdivbinom2  14294  hashf1  14490  abs1m  15383  abslem2  15387  sqreulem  15407  sqreu  15408  o1fsum  15861  divrcnv  15902  divcnv  15903  geolim  15920  geolim2  15921  geo2sum  15923  geo2lim  15925  fproddiv  16011  bpolycl  16102  bpolysum  16103  bpolydiflem  16104  bpoly4  16109  eftcl  16123  efaddlem  16143  tancl  16181  tanval2  16185  qredeq  16711  pcaddlem  16944  pjthlem1  25561  iblss  25929  itgeqa  25938  iblconst  25942  iblabsr  25954  iblmulc2  25955  itgsplit  25960  dvlem  26020  dvmulbr  26063  dvcobr  26070  dvrec  26079  dvrecg  26097  dvmptdiv  26098  dvcnvlem  26100  dveflem  26103  dvsincos  26105  dvlip  26117  c1liplem1  26120  lhop1lem  26137  lhop1  26138  lhop2  26139  lhop  26140  ftc1lem4  26163  vieta1lem2  26437  vieta1  26438  elqaalem3  26447  aareccl  26452  aalioulem1  26458  taylfvallem1  26482  tayl0  26487  taylply2  26493  taylply  26494  dvtaylp  26495  taylthlem2  26499  ulmdvlem1  26525  tanregt0  26666  eff1olem  26675  argregt0  26737  argrege0  26738  argimgt0  26739  logcnlem4  26772  advlogexp  26782  logtaylsum  26788  logtayl2  26789  root1eq1  26882  logbcl  26894  cxplogb  26913  logbf  26916  angcld  26932  angrteqvd  26933  cosangneg2d  26934  angrtmuld  26935  ang180lem1  26936  ang180lem2  26937  ang180lem3  26938  ang180lem4  26939  ang180lem5  26940  lawcoslem1  26942  lawcos  26943  isosctrlem2  26946  isosctrlem3  26947  angpieqvdlem  26955  angpieqvdlem2  26956  angpieqvd  26958  dcubic1lem  26970  dcubic2  26971  dcubic1  26972  dcubic  26973  mcubic  26974  cubic2  26975  dquartlem1  26978  dquartlem2  26979  dquart  26980  quart1cl  26981  quart1lem  26982  quart1  26983  quartlem3  26986  quartlem4  26987  quart  26988  tanatan  27046  atantayl  27064  atantayl2  27065  atantayl3  27066  log2cnv  27071  birthdaylem2  27079  efrlim  27096  dfef2  27097  cxploglim2  27105  fsumharmonic  27138  lgamgulmlem2  27156  lgamgulmlem3  27157  lgamgulmlem4  27158  lgamgulmlem5  27159  lgamgulmlem6  27160  lgamgulm2  27162  lgamcvg2  27181  gamcvg  27182  gamcvg2lem  27185  ftalem4  27202  ftalem5  27203  basellem8  27214  logexprlim  27351  bposlem9  27418  2lgslem3d  27525  2sqlem3  27546  dchrmusum2  27620  dchrvmasum2lem  27622  dchrvmasumiflem1  27627  dchrvmasumiflem2  27628  dchrvmaeq0  27630  dchrisum0re  27639  dchrisum0lem1b  27641  dchrisum0lem1  27642  dchrisum0lem2a  27643  dchrisum0lem2  27644  dchrisum0lem3  27645  dchrisum0  27646  mudivsum  27656  vmalogdivsum2  27664  vmalogdivsum  27665  2vmadivsumlem  27666  selberg2  27677  selberg3lem1  27683  selberg3  27685  selberg4lem1  27686  selbergr  27694  selberg3r  27695  selberg4r  27696  selberg34r  27697  pntrlog2bndlem1  27703  pntrlog2bndlem2  27704  pntrlog2bndlem3  27705  pntrlog2bndlem4  27706  pntrlog2bndlem5  27707  colinearalg  29197  axcontlem8  29258  nrt2irr  30761  pjhthlem1  31680  eigvalcl  32250  riesz3i  32351  quad3d  33031  bcm1n  33077  divnumden2  33097  zringfrac  33785  constrrtlc1  34063  constrrtcclem  34065  constrfin  34077  constrdircl  34096  constrreinvcl  34103  constrsqrtcl  34110  cos9thpiminplylem2  34114  cos9thpiminplylem3  34115  cos9thpiminply  34119  cos9thpinconstrlem1  34120  cos9thpinconstrlem2  34121  cos9thpinconstr  34122  oddpwdc  34685  signsplypnf  34878  signsply0  34879  itgexpif  34934  hgt750leme  34986  subfacval2  35574  divcnvlin  36120  bcprod  36125  iprodgam  36129  unbdqndv2lem1  36983  knoppndvlem2  36987  knoppndvlem7  36992  knoppndvlem9  36994  knoppndvlem10  36995  knoppndvlem16  37001  knoppndvlem17  37002  itg2addnclem  38205  iblmulc2nc  38219  ftc1cnnclem  38225  areacirclem1  38242  areacirclem4  38245  areacirc  38247  cntotbnd  38330  recbothd  42644  lcmineqlem12  42692  lcmineqlem18  42698  dvrelogpow2b  42720  aks4d1p1p2  42722  aks4d1p1p7  42726  aks6d1c2p2  42771  aks6d1c4  42776  2ap1caineq  42797  aks6d1c7lem1  42832  quadfac  42857  pellexlem2  43444  pellexlem6  43448  jm2.19  43607  jm2.27c  43621  proot1ex  43810  cvgdvgrat  44910  radcnvrat  44911  hashnzfzclim  44919  bcccl  44936  bccm1k  44939  binomcxplemrat  44947  binomcxplemfrat  44948  binomcxplemnotnn0  44953  xralrple2  45957  mccllem  46200  clim1fr1  46204  0ellimcdiv  46250  coseq0  46465  fperdvper  46520  dvdivbd  46524  dvnmptdivc  46539  dvnxpaek  46543  dvnprodlem2  46548  iblsplit  46567  itgcoscmulx  46570  itgsincmulx  46575  stoweidlem11  46612  stoweidlem26  46627  stoweidlem42  46643  wallispilem4  46669  wallispilem5  46670  wallispi  46671  wallispi2lem1  46672  wallispi2lem2  46673  wallispi2  46674  stirlinglem1  46675  stirlinglem3  46677  stirlinglem4  46678  stirlinglem5  46679  stirlinglem6  46680  stirlinglem7  46681  stirlinglem13  46687  stirlinglem14  46688  stirlinglem15  46689  dirkeritg  46703  dirkercncflem1  46704  dirkercncflem2  46705  fourierdlem26  46734  fourierdlem39  46747  fourierdlem56  46763  fourierdlem62  46769  fourierdlem72  46779  fourierdlem74  46781  fourierdlem75  46782  fourierdlem76  46783  fourierdlem80  46787  fourierdlem103  46810  fourierdlem104  46811  fouriersw  46832  elaa2lem  46834  etransclem15  46850  etransclem20  46855  etransclem21  46856  etransclem22  46857  etransclem23  46858  etransclem24  46859  etransclem25  46860  etransclem31  46866  etransclem32  46867  etransclem33  46868  etransclem34  46869  etransclem35  46870  etransclem47  46882  etransclem48  46883  hoiqssbllem2  47224  sigardiv  47462  sharhght  47466  cndivrenred  47927  fmtnoprmfac2lem1  48202  quad1  48269  requad01  48270  requad1  48271  fdivmptf  49201  affinecomb2  49363  eenglngeehlnmlem1  49397  eenglngeehlnmlem2  49398  itscnhlc0xyqsol  49425  itschlc0xyqsol1  49426  cotcl  50410