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 1379	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2119   ≠ wne 2934  (class class class)co 7356  ℂ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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  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 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-po 5526  df-so 5527  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  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  25422  iblss  25790  itgeqa  25799  iblconst  25803  iblabsr  25815  iblmulc2  25816  itgsplit  25821  dvlem  25881  dvmulbr  25924  dvcobr  25931  dvrec  25940  dvrecg  25958  dvmptdiv  25959  dvcnvlem  25961  dveflem  25964  dvsincos  25966  dvlip  25978  c1liplem1  25981  lhop1lem  25998  lhop1  25999  lhop2  26000  lhop  26001  ftc1lem4  26024  vieta1lem2  26295  vieta1  26296  elqaalem3  26305  aareccl  26310  aalioulem1  26316  taylfvallem1  26340  tayl0  26345  taylply2  26351  taylply  26352  dvtaylp  26353  taylthlem2  26357  ulmdvlem1  26383  tanregt0  26521  eff1olem  26530  argregt0  26592  argrege0  26593  argimgt0  26594  logcnlem4  26627  advlogexp  26637  logtaylsum  26643  logtayl2  26644  root1eq1  26737  logbcl  26749  cxplogb  26768  logbf  26771  angcld  26787  angrteqvd  26788  cosangneg2d  26789  angrtmuld  26790  ang180lem1  26791  ang180lem2  26792  ang180lem3  26793  ang180lem4  26794  ang180lem5  26795  lawcoslem1  26797  lawcos  26798  isosctrlem2  26801  isosctrlem3  26802  angpieqvdlem  26810  angpieqvdlem2  26811  angpieqvd  26813  dcubic1lem  26825  dcubic2  26826  dcubic1  26827  dcubic  26828  mcubic  26829  cubic2  26830  dquartlem1  26833  dquartlem2  26834  dquart  26835  quart1cl  26836  quart1lem  26837  quart1  26838  quartlem3  26841  quartlem4  26842  quart  26843  tanatan  26901  atantayl  26919  atantayl2  26920  atantayl3  26921  log2cnv  26926  birthdaylem2  26934  efrlim  26951  dfef2  26952  cxploglim2  26960  fsumharmonic  26993  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem4  27013  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  ftalem4  27057  ftalem5  27058  basellem8  27069  logexprlim  27206  bposlem9  27273  2lgslem3d  27380  2sqlem3  27401  dchrmusum2  27475  dchrvmasum2lem  27477  dchrvmasumiflem1  27482  dchrvmasumiflem2  27483  dchrvmaeq0  27485  dchrisum0re  27494  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2a  27498  dchrisum0lem2  27499  dchrisum0lem3  27500  dchrisum0  27501  mudivsum  27511  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  selberg2  27532  selberg3lem1  27538  selberg3  27540  selberg4lem1  27541  selbergr  27549  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  colinearalg  28997  axcontlem8  29058  nrt2irr  30561  pjhthlem1  31480  eigvalcl  32050  riesz3i  32151  quad3d  32841  bcm1n  32887  divnumden2  32908  zringfrac  33637  constrrtlc1  33916  constrrtcclem  33918  constrfin  33930  constrdircl  33949  constrreinvcl  33956  constrsqrtcl  33963  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  cos9thpiminply  33972  cos9thpinconstrlem1  33973  cos9thpinconstrlem2  33974  cos9thpinconstr  33975  oddpwdc  34538  signsplypnf  34734  signsply0  34735  itgexpif  34790  hgt750leme  34842  subfacval2  35415  divcnvlin  35961  bcprod  35966  iprodgam  35970  unbdqndv2lem1  36815  knoppndvlem2  36819  knoppndvlem7  36824  knoppndvlem9  36826  knoppndvlem10  36827  knoppndvlem16  36833  knoppndvlem17  36834  itg2addnclem  38038  iblmulc2nc  38052  ftc1cnnclem  38058  areacirclem1  38075  areacirclem4  38078  areacirc  38080  cntotbnd  38163  recbothd  42477  lcmineqlem12  42525  lcmineqlem18  42531  dvrelogpow2b  42553  aks4d1p1p2  42555  aks4d1p1p7  42559  aks6d1c2p2  42604  aks6d1c4  42609  2ap1caineq  42630  aks6d1c7lem1  42665  pellexlem2  43275  pellexlem6  43279  jm2.19  43438  jm2.27c  43452  proot1ex  43641  cvgdvgrat  44757  radcnvrat  44758  hashnzfzclim  44766  bcccl  44783  bccm1k  44786  binomcxplemrat  44794  binomcxplemfrat  44795  binomcxplemnotnn0  44800  xralrple2  45799  mccllem  46042  clim1fr1  46046  0ellimcdiv  46092  coseq0  46307  fperdvper  46362  dvdivbd  46366  dvnmptdivc  46381  dvnxpaek  46385  dvnprodlem2  46390  iblsplit  46409  itgcoscmulx  46412  itgsincmulx  46417  stoweidlem11  46454  stoweidlem26  46469  stoweidlem42  46485  wallispilem4  46511  wallispilem5  46512  wallispi  46513  wallispi2lem1  46514  wallispi2lem2  46515  wallispi2  46516  stirlinglem1  46517  stirlinglem3  46519  stirlinglem4  46520  stirlinglem5  46521  stirlinglem6  46522  stirlinglem7  46523  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  dirkeritg  46545  dirkercncflem1  46546  dirkercncflem2  46547  fourierdlem26  46576  fourierdlem39  46589  fourierdlem56  46605  fourierdlem62  46611  fourierdlem72  46621  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem80  46629  fourierdlem103  46652  fourierdlem104  46653  fouriersw  46674  elaa2lem  46676  etransclem15  46692  etransclem20  46697  etransclem21  46698  etransclem22  46699  etransclem23  46700  etransclem24  46701  etransclem25  46702  etransclem31  46708  etransclem32  46709  etransclem33  46710  etransclem34  46711  etransclem35  46712  etransclem47  46724  etransclem48  46725  hoiqssbllem2  47066  sigardiv  47304  sharhght  47308  cndivrenred  47769  fmtnoprmfac2lem1  48044  quad1  48111  requad01  48112  requad1  48113  fdivmptf  49032  affinecomb2  49194  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  itscnhlc0xyqsol  49256  itschlc0xyqsol1  49257  cotcl  50242