Theorem divcld 11681

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2942  (class class class)co 7255  ℂcc 10800  0cc0 10802   / cdiv 11562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563

This theorem is referenced by:  dmdcan2d  11711  mulsubdivbinom2  13904  hashf1  14099  abs1m  14975  abslem2  14979  sqreulem  14999  sqreu  15000  o1fsum  15453  divrcnv  15492  divcnv  15493  geolim  15510  geolim2  15511  geo2sum  15513  geo2lim  15515  fproddiv  15599  bpolycl  15690  bpolysum  15691  bpolydiflem  15692  bpoly4  15697  eftcl  15711  efaddlem  15730  tancl  15766  tanval2  15770  qredeq  16290  pcaddlem  16517  pjthlem1  24506  iblss  24874  itgeqa  24883  iblconst  24887  iblabsr  24899  iblmulc2  24900  itgsplit  24905  dvlem  24965  dvmulbr  25008  dvcobr  25015  dvrec  25024  dvrecg  25042  dvmptdiv  25043  dvcnvlem  25045  dveflem  25048  dvsincos  25050  dvlip  25062  c1liplem1  25065  lhop1lem  25082  lhop1  25083  lhop2  25084  lhop  25085  ftc1lem4  25108  vieta1lem2  25376  vieta1  25377  elqaalem3  25386  aareccl  25391  aalioulem1  25397  taylfvallem1  25421  tayl0  25426  taylply2  25432  taylply  25433  dvtaylp  25434  taylthlem2  25438  ulmdvlem1  25464  tanregt0  25600  eff1olem  25609  argregt0  25670  argrege0  25671  argimgt0  25672  logcnlem4  25705  advlogexp  25715  logtaylsum  25721  logtayl2  25722  root1eq1  25813  logbcl  25822  cxplogb  25841  logbf  25844  angcld  25860  angrteqvd  25861  cosangneg2d  25862  angrtmuld  25863  ang180lem1  25864  ang180lem2  25865  ang180lem3  25866  ang180lem4  25867  ang180lem5  25868  lawcoslem1  25870  lawcos  25871  isosctrlem2  25874  isosctrlem3  25875  angpieqvdlem  25883  angpieqvdlem2  25884  angpieqvd  25886  dcubic1lem  25898  dcubic2  25899  dcubic1  25900  dcubic  25901  mcubic  25902  cubic2  25903  dquartlem1  25906  dquartlem2  25907  dquart  25908  quart1cl  25909  quart1lem  25910  quart1  25911  quartlem3  25914  quartlem4  25915  quart  25916  tanatan  25974  atantayl  25992  atantayl2  25993  atantayl3  25994  log2cnv  25999  birthdaylem2  26007  efrlim  26024  dfef2  26025  cxploglim2  26033  fsumharmonic  26066  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem4  26086  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamgulm2  26090  lgamcvg2  26109  gamcvg  26110  gamcvg2lem  26113  ftalem4  26130  ftalem5  26131  basellem8  26142  logexprlim  26278  bposlem9  26345  2lgslem3d  26452  2sqlem3  26473  dchrmusum2  26547  dchrvmasum2lem  26549  dchrvmasumiflem1  26554  dchrvmasumiflem2  26555  dchrvmaeq0  26557  dchrisum0re  26566  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0lem3  26572  dchrisum0  26573  mudivsum  26583  vmalogdivsum2  26591  vmalogdivsum  26592  2vmadivsumlem  26593  selberg2  26604  selberg3lem1  26610  selberg3  26612  selberg4lem1  26613  selbergr  26621  selberg3r  26622  selberg4r  26623  selberg34r  26624  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  colinearalg  27181  axcontlem8  27242  pjhthlem1  29654  eigvalcl  30224  riesz3i  30325  bcm1n  31018  divnumden2  31034  oddpwdc  32221  signsplypnf  32429  signsply0  32430  itgexpif  32486  hgt750leme  32538  subfacval2  33049  divcnvlin  33604  bcprod  33610  iprodgam  33614  unbdqndv2lem1  34616  knoppndvlem2  34620  knoppndvlem7  34625  knoppndvlem9  34627  knoppndvlem10  34628  knoppndvlem16  34634  knoppndvlem17  34635  itg2addnclem  35755  iblmulc2nc  35769  ftc1cnnclem  35775  areacirclem1  35792  areacirclem4  35795  areacirc  35797  cntotbnd  35881  recbothd  39929  lcmineqlem12  39976  lcmineqlem18  39982  dvrelogpow2b  40004  aks4d1p1p2  40006  aks4d1p1p7  40010  2ap1caineq  40029  pellexlem2  40568  pellexlem6  40572  jm2.19  40731  jm2.27c  40745  proot1ex  40942  cvgdvgrat  41820  radcnvrat  41821  hashnzfzclim  41829  bcccl  41846  bccm1k  41849  binomcxplemrat  41857  binomcxplemfrat  41858  binomcxplemnotnn0  41863  xralrple2  42783  mccllem  43028  clim1fr1  43032  0ellimcdiv  43080  coseq0  43295  fperdvper  43350  dvdivbd  43354  dvnmptdivc  43369  dvnxpaek  43373  dvnprodlem2  43378  iblsplit  43397  itgcoscmulx  43400  itgsincmulx  43405  stoweidlem11  43442  stoweidlem26  43457  stoweidlem42  43473  wallispilem4  43499  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  wallispi2  43504  stirlinglem1  43505  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  dirkeritg  43533  dirkercncflem1  43534  dirkercncflem2  43535  fourierdlem26  43564  fourierdlem39  43577  fourierdlem56  43593  fourierdlem62  43599  fourierdlem72  43609  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem80  43617  fourierdlem103  43640  fourierdlem104  43641  fouriersw  43662  elaa2lem  43664  etransclem15  43680  etransclem20  43685  etransclem21  43686  etransclem22  43687  etransclem23  43688  etransclem24  43689  etransclem25  43690  etransclem31  43696  etransclem32  43697  etransclem33  43698  etransclem34  43699  etransclem35  43700  etransclem47  43712  etransclem48  43713  hoiqssbllem2  44051  sigardiv  44264  sharhght  44268  cndivrenred  44686  fmtnoprmfac2lem1  44906  quad1  44960  requad01  44961  requad1  44962  fdivmptf  45775  affinecomb2  45937  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  itscnhlc0xyqsol  45999  itschlc0xyqsol1  46000  cotcl  46340