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

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2941  (class class class)co 7406  ℂcc 11105  0cc0 11107   / cdiv 11868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869

This theorem is referenced by:  dmdcan2d  12017  mulsubdivbinom2  14219  hashf1  14415  abs1m  15279  abslem2  15283  sqreulem  15303  sqreu  15304  o1fsum  15756  divrcnv  15795  divcnv  15796  geolim  15813  geolim2  15814  geo2sum  15816  geo2lim  15818  fproddiv  15902  bpolycl  15993  bpolysum  15994  bpolydiflem  15995  bpoly4  16000  eftcl  16014  efaddlem  16033  tancl  16069  tanval2  16073  qredeq  16591  pcaddlem  16818  pjthlem1  24946  iblss  25314  itgeqa  25323  iblconst  25327  iblabsr  25339  iblmulc2  25340  itgsplit  25345  dvlem  25405  dvmulbr  25448  dvcobr  25455  dvrec  25464  dvrecg  25482  dvmptdiv  25483  dvcnvlem  25485  dveflem  25488  dvsincos  25490  dvlip  25502  c1liplem1  25505  lhop1lem  25522  lhop1  25523  lhop2  25524  lhop  25525  ftc1lem4  25548  vieta1lem2  25816  vieta1  25817  elqaalem3  25826  aareccl  25831  aalioulem1  25837  taylfvallem1  25861  tayl0  25866  taylply2  25872  taylply  25873  dvtaylp  25874  taylthlem2  25878  ulmdvlem1  25904  tanregt0  26040  eff1olem  26049  argregt0  26110  argrege0  26111  argimgt0  26112  logcnlem4  26145  advlogexp  26155  logtaylsum  26161  logtayl2  26162  root1eq1  26253  logbcl  26262  cxplogb  26281  logbf  26284  angcld  26300  angrteqvd  26301  cosangneg2d  26302  angrtmuld  26303  ang180lem1  26304  ang180lem2  26305  ang180lem3  26306  ang180lem4  26307  ang180lem5  26308  lawcoslem1  26310  lawcos  26311  isosctrlem2  26314  isosctrlem3  26315  angpieqvdlem  26323  angpieqvdlem2  26324  angpieqvd  26326  dcubic1lem  26338  dcubic2  26339  dcubic1  26340  dcubic  26341  mcubic  26342  cubic2  26343  dquartlem1  26346  dquartlem2  26347  dquart  26348  quart1cl  26349  quart1lem  26350  quart1  26351  quartlem3  26354  quartlem4  26355  quart  26356  tanatan  26414  atantayl  26432  atantayl2  26433  atantayl3  26434  log2cnv  26439  birthdaylem2  26447  efrlim  26464  dfef2  26465  cxploglim2  26473  fsumharmonic  26506  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamgulmlem4  26526  lgamgulmlem5  26527  lgamgulmlem6  26528  lgamgulm2  26530  lgamcvg2  26549  gamcvg  26550  gamcvg2lem  26553  ftalem4  26570  ftalem5  26571  basellem8  26582  logexprlim  26718  bposlem9  26785  2lgslem3d  26892  2sqlem3  26913  dchrmusum2  26987  dchrvmasum2lem  26989  dchrvmasumiflem1  26994  dchrvmasumiflem2  26995  dchrvmaeq0  26997  dchrisum0re  27006  dchrisum0lem1b  27008  dchrisum0lem1  27009  dchrisum0lem2a  27010  dchrisum0lem2  27011  dchrisum0lem3  27012  dchrisum0  27013  mudivsum  27023  vmalogdivsum2  27031  vmalogdivsum  27032  2vmadivsumlem  27033  selberg2  27044  selberg3lem1  27050  selberg3  27052  selberg4lem1  27053  selbergr  27061  selberg3r  27062  selberg4r  27063  selberg34r  27064  pntrlog2bndlem1  27070  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  colinearalg  28158  axcontlem8  28219  pjhthlem1  30632  eigvalcl  31202  riesz3i  31303  bcm1n  31994  divnumden2  32012  oddpwdc  33342  signsplypnf  33550  signsply0  33551  itgexpif  33607  hgt750leme  33659  subfacval2  34167  divcnvlin  34691  bcprod  34697  iprodgam  34701  gg-dvmulbr  35164  gg-dvcobr  35165  unbdqndv2lem1  35374  knoppndvlem2  35378  knoppndvlem7  35383  knoppndvlem9  35385  knoppndvlem10  35386  knoppndvlem16  35392  knoppndvlem17  35393  itg2addnclem  36528  iblmulc2nc  36542  ftc1cnnclem  36548  areacirclem1  36565  areacirclem4  36568  areacirc  36570  cntotbnd  36653  recbothd  40847  lcmineqlem12  40894  lcmineqlem18  40900  dvrelogpow2b  40922  aks4d1p1p2  40924  aks4d1p1p7  40928  aks6d1c2p2  40946  2ap1caineq  40950  pellexlem2  41554  pellexlem6  41558  jm2.19  41718  jm2.27c  41732  proot1ex  41929  cvgdvgrat  43058  radcnvrat  43059  hashnzfzclim  43067  bcccl  43084  bccm1k  43087  binomcxplemrat  43095  binomcxplemfrat  43096  binomcxplemnotnn0  43101  xralrple2  44051  mccllem  44300  clim1fr1  44304  0ellimcdiv  44352  coseq0  44567  fperdvper  44622  dvdivbd  44626  dvnmptdivc  44641  dvnxpaek  44645  dvnprodlem2  44650  iblsplit  44669  itgcoscmulx  44672  itgsincmulx  44677  stoweidlem11  44714  stoweidlem26  44729  stoweidlem42  44745  wallispilem4  44771  wallispilem5  44772  wallispi  44773  wallispi2lem1  44774  wallispi2lem2  44775  wallispi2  44776  stirlinglem1  44777  stirlinglem3  44779  stirlinglem4  44780  stirlinglem5  44781  stirlinglem6  44782  stirlinglem7  44783  stirlinglem13  44789  stirlinglem14  44790  stirlinglem15  44791  dirkeritg  44805  dirkercncflem1  44806  dirkercncflem2  44807  fourierdlem26  44836  fourierdlem39  44849  fourierdlem56  44865  fourierdlem62  44871  fourierdlem72  44881  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem80  44889  fourierdlem103  44912  fourierdlem104  44913  fouriersw  44934  elaa2lem  44936  etransclem15  44952  etransclem20  44957  etransclem21  44958  etransclem22  44959  etransclem23  44960  etransclem24  44961  etransclem25  44962  etransclem31  44968  etransclem32  44969  etransclem33  44970  etransclem34  44971  etransclem35  44972  etransclem47  44984  etransclem48  44985  hoiqssbllem2  45326  sigardiv  45564  sharhght  45568  cndivrenred  46001  fmtnoprmfac2lem1  46221  quad1  46275  requad01  46276  requad1  46277  fdivmptf  47181  affinecomb2  47343  eenglngeehlnmlem1  47377  eenglngeehlnmlem2  47378  itscnhlc0xyqsol  47405  itschlc0xyqsol1  47406  cotcl  47751