Theorem divcld 11908

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2929  (class class class)co 7355  ℂcc 11015  0cc0 11017   / cdiv 11785

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 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093  ax-pre-mulgt0 11094

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-sub 11357  df-neg 11358  df-div 11786

This theorem is referenced by:  dmdcan2d  11938  mulsubdivbinom2  14176  hashf1  14371  abs1m  15250  abslem2  15254  sqreulem  15274  sqreu  15275  o1fsum  15727  divrcnv  15766  divcnv  15767  geolim  15784  geolim2  15785  geo2sum  15787  geo2lim  15789  fproddiv  15875  bpolycl  15966  bpolysum  15967  bpolydiflem  15968  bpoly4  15973  eftcl  15987  efaddlem  16007  tancl  16045  tanval2  16049  qredeq  16575  pcaddlem  16807  pjthlem1  25384  iblss  25753  itgeqa  25762  iblconst  25766  iblabsr  25778  iblmulc2  25779  itgsplit  25784  dvlem  25844  dvmulbr  25888  dvmulbrOLD  25889  dvcobr  25896  dvcobrOLD  25897  dvrec  25906  dvrecg  25924  dvmptdiv  25925  dvcnvlem  25927  dveflem  25930  dvsincos  25932  dvlip  25945  c1liplem1  25948  lhop1lem  25965  lhop1  25966  lhop2  25967  lhop  25968  ftc1lem4  25993  vieta1lem2  26266  vieta1  26267  elqaalem3  26276  aareccl  26281  aalioulem1  26287  taylfvallem1  26311  tayl0  26316  taylply2  26322  taylply2OLD  26323  taylply  26324  dvtaylp  26325  taylthlem2  26329  taylthlem2OLD  26330  ulmdvlem1  26356  tanregt0  26495  eff1olem  26504  argregt0  26566  argrege0  26567  argimgt0  26568  logcnlem4  26601  advlogexp  26611  logtaylsum  26617  logtayl2  26618  root1eq1  26712  logbcl  26724  cxplogb  26743  logbf  26746  angcld  26762  angrteqvd  26763  cosangneg2d  26764  angrtmuld  26765  ang180lem1  26766  ang180lem2  26767  ang180lem3  26768  ang180lem4  26769  ang180lem5  26770  lawcoslem1  26772  lawcos  26773  isosctrlem2  26776  isosctrlem3  26777  angpieqvdlem  26785  angpieqvdlem2  26786  angpieqvd  26788  dcubic1lem  26800  dcubic2  26801  dcubic1  26802  dcubic  26803  mcubic  26804  cubic2  26805  dquartlem1  26808  dquartlem2  26809  dquart  26810  quart1cl  26811  quart1lem  26812  quart1  26813  quartlem3  26816  quartlem4  26817  quart  26818  tanatan  26876  atantayl  26894  atantayl2  26895  atantayl3  26896  log2cnv  26901  birthdaylem2  26909  efrlim  26926  efrlimOLD  26927  dfef2  26928  cxploglim2  26936  fsumharmonic  26969  lgamgulmlem2  26987  lgamgulmlem3  26988  lgamgulmlem4  26989  lgamgulmlem5  26990  lgamgulmlem6  26991  lgamgulm2  26993  lgamcvg2  27012  gamcvg  27013  gamcvg2lem  27016  ftalem4  27033  ftalem5  27034  basellem8  27045  logexprlim  27183  bposlem9  27250  2lgslem3d  27357  2sqlem3  27378  dchrmusum2  27452  dchrvmasum2lem  27454  dchrvmasumiflem1  27459  dchrvmasumiflem2  27460  dchrvmaeq0  27462  dchrisum0re  27471  dchrisum0lem1b  27473  dchrisum0lem1  27474  dchrisum0lem2a  27475  dchrisum0lem2  27476  dchrisum0lem3  27477  dchrisum0  27478  mudivsum  27488  vmalogdivsum2  27496  vmalogdivsum  27497  2vmadivsumlem  27498  selberg2  27509  selberg3lem1  27515  selberg3  27517  selberg4lem1  27518  selbergr  27526  selberg3r  27527  selberg4r  27528  selberg34r  27529  pntrlog2bndlem1  27535  pntrlog2bndlem2  27536  pntrlog2bndlem3  27537  pntrlog2bndlem4  27538  pntrlog2bndlem5  27539  colinearalg  28909  axcontlem8  28970  nrt2irr  30474  pjhthlem1  31392  eigvalcl  31962  riesz3i  32063  quad3d  32757  bcm1n  32803  divnumden2  32824  zringfrac  33563  constrrtlc1  33817  constrrtcclem  33819  constrfin  33831  constrdircl  33850  constrreinvcl  33857  constrsqrtcl  33864  cos9thpiminplylem2  33868  cos9thpiminplylem3  33869  cos9thpiminply  33873  cos9thpinconstrlem1  33874  cos9thpinconstrlem2  33875  cos9thpinconstr  33876  oddpwdc  34439  signsplypnf  34635  signsply0  34636  itgexpif  34691  hgt750leme  34743  subfacval2  35303  divcnvlin  35849  bcprod  35854  iprodgam  35858  unbdqndv2lem1  36625  knoppndvlem2  36629  knoppndvlem7  36634  knoppndvlem9  36636  knoppndvlem10  36637  knoppndvlem16  36643  knoppndvlem17  36644  itg2addnclem  37784  iblmulc2nc  37798  ftc1cnnclem  37804  areacirclem1  37821  areacirclem4  37824  areacirc  37826  cntotbnd  37909  recbothd  42158  lcmineqlem12  42206  lcmineqlem18  42212  dvrelogpow2b  42234  aks4d1p1p2  42236  aks4d1p1p7  42240  aks6d1c2p2  42285  aks6d1c4  42290  2ap1caineq  42311  aks6d1c7lem1  42346  pellexlem2  42987  pellexlem6  42991  jm2.19  43150  jm2.27c  43164  proot1ex  43353  cvgdvgrat  44470  radcnvrat  44471  hashnzfzclim  44479  bcccl  44496  bccm1k  44499  binomcxplemrat  44507  binomcxplemfrat  44508  binomcxplemnotnn0  44513  xralrple2  45515  mccllem  45759  clim1fr1  45763  0ellimcdiv  45809  coseq0  46024  fperdvper  46079  dvdivbd  46083  dvnmptdivc  46098  dvnxpaek  46102  dvnprodlem2  46107  iblsplit  46126  itgcoscmulx  46129  itgsincmulx  46134  stoweidlem11  46171  stoweidlem26  46186  stoweidlem42  46202  wallispilem4  46228  wallispilem5  46229  wallispi  46230  wallispi2lem1  46231  wallispi2lem2  46232  wallispi2  46233  stirlinglem1  46234  stirlinglem3  46236  stirlinglem4  46237  stirlinglem5  46238  stirlinglem6  46239  stirlinglem7  46240  stirlinglem13  46246  stirlinglem14  46247  stirlinglem15  46248  dirkeritg  46262  dirkercncflem1  46263  dirkercncflem2  46264  fourierdlem26  46293  fourierdlem39  46306  fourierdlem56  46322  fourierdlem62  46328  fourierdlem72  46338  fourierdlem74  46340  fourierdlem75  46341  fourierdlem76  46342  fourierdlem80  46346  fourierdlem103  46369  fourierdlem104  46370  fouriersw  46391  elaa2lem  46393  etransclem15  46409  etransclem20  46414  etransclem21  46415  etransclem22  46416  etransclem23  46417  etransclem24  46418  etransclem25  46419  etransclem31  46425  etransclem32  46426  etransclem33  46427  etransclem34  46428  etransclem35  46429  etransclem47  46441  etransclem48  46442  hoiqssbllem2  46783  sigardiv  47021  sharhght  47025  cndivrenred  47468  fmtnoprmfac2lem1  47728  quad1  47782  requad01  47783  requad1  47784  fdivmptf  48703  affinecomb2  48865  eenglngeehlnmlem1  48899  eenglngeehlnmlem2  48900  itscnhlc0xyqsol  48927  itschlc0xyqsol1  48928  cotcl  49913