Theorem divcld 11917

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2932  (class class class)co 7358  ℂcc 11024  0cc0 11026   / cdiv 11794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  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 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-div 11795

This theorem is referenced by:  dmdcan2d  11947  mulsubdivbinom2  14185  hashf1  14380  abs1m  15259  abslem2  15263  sqreulem  15283  sqreu  15284  o1fsum  15736  divrcnv  15775  divcnv  15776  geolim  15793  geolim2  15794  geo2sum  15796  geo2lim  15798  fproddiv  15884  bpolycl  15975  bpolysum  15976  bpolydiflem  15977  bpoly4  15982  eftcl  15996  efaddlem  16016  tancl  16054  tanval2  16058  qredeq  16584  pcaddlem  16816  pjthlem1  25393  iblss  25762  itgeqa  25771  iblconst  25775  iblabsr  25787  iblmulc2  25788  itgsplit  25793  dvlem  25853  dvmulbr  25897  dvmulbrOLD  25898  dvcobr  25905  dvcobrOLD  25906  dvrec  25915  dvrecg  25933  dvmptdiv  25934  dvcnvlem  25936  dveflem  25939  dvsincos  25941  dvlip  25954  c1liplem1  25957  lhop1lem  25974  lhop1  25975  lhop2  25976  lhop  25977  ftc1lem4  26002  vieta1lem2  26275  vieta1  26276  elqaalem3  26285  aareccl  26290  aalioulem1  26296  taylfvallem1  26320  tayl0  26325  taylply2  26331  taylply2OLD  26332  taylply  26333  dvtaylp  26334  taylthlem2  26338  taylthlem2OLD  26339  ulmdvlem1  26365  tanregt0  26504  eff1olem  26513  argregt0  26575  argrege0  26576  argimgt0  26577  logcnlem4  26610  advlogexp  26620  logtaylsum  26626  logtayl2  26627  root1eq1  26721  logbcl  26733  cxplogb  26752  logbf  26755  angcld  26771  angrteqvd  26772  cosangneg2d  26773  angrtmuld  26774  ang180lem1  26775  ang180lem2  26776  ang180lem3  26777  ang180lem4  26778  ang180lem5  26779  lawcoslem1  26781  lawcos  26782  isosctrlem2  26785  isosctrlem3  26786  angpieqvdlem  26794  angpieqvdlem2  26795  angpieqvd  26797  dcubic1lem  26809  dcubic2  26810  dcubic1  26811  dcubic  26812  mcubic  26813  cubic2  26814  dquartlem1  26817  dquartlem2  26818  dquart  26819  quart1cl  26820  quart1lem  26821  quart1  26822  quartlem3  26825  quartlem4  26826  quart  26827  tanatan  26885  atantayl  26903  atantayl2  26904  atantayl3  26905  log2cnv  26910  birthdaylem2  26918  efrlim  26935  efrlimOLD  26936  dfef2  26937  cxploglim2  26945  fsumharmonic  26978  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem4  26998  lgamgulmlem5  26999  lgamgulmlem6  27000  lgamgulm2  27002  lgamcvg2  27021  gamcvg  27022  gamcvg2lem  27025  ftalem4  27042  ftalem5  27043  basellem8  27054  logexprlim  27192  bposlem9  27259  2lgslem3d  27366  2sqlem3  27387  dchrmusum2  27461  dchrvmasum2lem  27463  dchrvmasumiflem1  27468  dchrvmasumiflem2  27469  dchrvmaeq0  27471  dchrisum0re  27480  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0lem2  27485  dchrisum0lem3  27486  dchrisum0  27487  mudivsum  27497  vmalogdivsum2  27505  vmalogdivsum  27506  2vmadivsumlem  27507  selberg2  27518  selberg3lem1  27524  selberg3  27526  selberg4lem1  27527  selbergr  27535  selberg3r  27536  selberg4r  27537  selberg34r  27538  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  colinearalg  28983  axcontlem8  29044  nrt2irr  30548  pjhthlem1  31466  eigvalcl  32036  riesz3i  32137  quad3d  32829  bcm1n  32875  divnumden2  32896  zringfrac  33635  constrrtlc1  33889  constrrtcclem  33891  constrfin  33903  constrdircl  33922  constrreinvcl  33929  constrsqrtcl  33936  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  cos9thpiminply  33945  cos9thpinconstrlem1  33946  cos9thpinconstrlem2  33947  cos9thpinconstr  33948  oddpwdc  34511  signsplypnf  34707  signsply0  34708  itgexpif  34763  hgt750leme  34815  subfacval2  35381  divcnvlin  35927  bcprod  35932  iprodgam  35936  unbdqndv2lem1  36709  knoppndvlem2  36713  knoppndvlem7  36718  knoppndvlem9  36720  knoppndvlem10  36721  knoppndvlem16  36727  knoppndvlem17  36728  itg2addnclem  37872  iblmulc2nc  37886  ftc1cnnclem  37892  areacirclem1  37909  areacirclem4  37912  areacirc  37914  cntotbnd  37997  recbothd  42246  lcmineqlem12  42294  lcmineqlem18  42300  dvrelogpow2b  42322  aks4d1p1p2  42324  aks4d1p1p7  42328  aks6d1c2p2  42373  aks6d1c4  42378  2ap1caineq  42399  aks6d1c7lem1  42434  pellexlem2  43072  pellexlem6  43076  jm2.19  43235  jm2.27c  43249  proot1ex  43438  cvgdvgrat  44554  radcnvrat  44555  hashnzfzclim  44563  bcccl  44580  bccm1k  44583  binomcxplemrat  44591  binomcxplemfrat  44592  binomcxplemnotnn0  44597  xralrple2  45599  mccllem  45843  clim1fr1  45847  0ellimcdiv  45893  coseq0  46108  fperdvper  46163  dvdivbd  46167  dvnmptdivc  46182  dvnxpaek  46186  dvnprodlem2  46191  iblsplit  46210  itgcoscmulx  46213  itgsincmulx  46218  stoweidlem11  46255  stoweidlem26  46270  stoweidlem42  46286  wallispilem4  46312  wallispilem5  46313  wallispi  46314  wallispi2lem1  46315  wallispi2lem2  46316  wallispi2  46317  stirlinglem1  46318  stirlinglem3  46320  stirlinglem4  46321  stirlinglem5  46322  stirlinglem6  46323  stirlinglem7  46324  stirlinglem13  46330  stirlinglem14  46331  stirlinglem15  46332  dirkeritg  46346  dirkercncflem1  46347  dirkercncflem2  46348  fourierdlem26  46377  fourierdlem39  46390  fourierdlem56  46406  fourierdlem62  46412  fourierdlem72  46422  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem80  46430  fourierdlem103  46453  fourierdlem104  46454  fouriersw  46475  elaa2lem  46477  etransclem15  46493  etransclem20  46498  etransclem21  46499  etransclem22  46500  etransclem23  46501  etransclem24  46502  etransclem25  46503  etransclem31  46509  etransclem32  46510  etransclem33  46511  etransclem34  46512  etransclem35  46513  etransclem47  46525  etransclem48  46526  hoiqssbllem2  46867  sigardiv  47105  sharhght  47109  cndivrenred  47552  fmtnoprmfac2lem1  47812  quad1  47866  requad01  47867  requad1  47868  fdivmptf  48787  affinecomb2  48949  eenglngeehlnmlem1  48983  eenglngeehlnmlem2  48984  itscnhlc0xyqsol  49011  itschlc0xyqsol1  49012  cotcl  49997