Theorem divcld 11127

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

Syntax hints:   → wi 4   ∈ wcel 2164   ≠ wne 2999  (class class class)co 6905  ℂcc 10250  0cc0 10252   / cdiv 11009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-po 5263  df-so 5264  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-er 8009  df-en 8223  df-dom 8224  df-sdom 8225  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010

This theorem is referenced by:  dmdcan2d  11157  mulsubdivbinom2  13342  hashf1  13530  abs1m  14452  abslem2  14456  sqreulem  14476  sqreu  14477  o1fsum  14919  divrcnv  14958  divcnv  14959  geolim  14975  geolim2  14976  geo2sum  14978  geo2lim  14980  fproddiv  15064  bpolycl  15155  bpolysum  15156  bpolydiflem  15157  bpoly4  15162  eftcl  15176  efaddlem  15195  tancl  15231  tanval2  15235  qredeq  15743  pcaddlem  15963  pjthlem1  23605  iblss  23970  itgeqa  23979  iblconst  23983  iblabsr  23995  iblmulc2  23996  itgsplit  24001  dvlem  24059  dvmulbr  24101  dvcobr  24108  dvrec  24117  dvrecg  24135  dvmptdiv  24136  dvcnvlem  24138  dveflem  24141  dvsincos  24143  dvlip  24155  c1liplem1  24158  lhop1lem  24175  lhop1  24176  lhop2  24177  lhop  24178  ftc1lem4  24201  vieta1lem2  24465  vieta1  24466  elqaalem3  24475  aareccl  24480  aalioulem1  24486  taylfvallem1  24510  tayl0  24515  taylply2  24521  taylply  24522  dvtaylp  24523  taylthlem2  24527  ulmdvlem1  24553  tanregt0  24685  eff1olem  24694  argregt0  24755  argrege0  24756  argimgt0  24757  logcnlem4  24790  advlogexp  24800  logtaylsum  24806  logtayl2  24807  root1eq1  24898  logbcl  24907  cxplogb  24926  logbf  24929  angcld  24945  angrteqvd  24946  cosangneg2d  24947  angrtmuld  24948  ang180lem1  24949  ang180lem2  24950  ang180lem3  24951  ang180lem4  24952  ang180lem5  24953  lawcoslem1  24955  lawcos  24956  isosctrlem2  24959  isosctrlem3  24960  angpieqvdlem  24968  angpieqvdlem2  24969  angpieqvd  24971  dcubic1lem  24983  dcubic2  24984  dcubic1  24985  dcubic  24986  mcubic  24987  cubic2  24988  dquartlem1  24991  dquartlem2  24992  dquart  24993  quart1cl  24994  quart1lem  24995  quart1  24996  quartlem3  24999  quartlem4  25000  quart  25001  tanatan  25059  atantayl  25077  atantayl2  25078  atantayl3  25079  log2cnv  25084  birthdaylem2  25092  efrlim  25109  dfef2  25110  cxploglim2  25118  fsumharmonic  25151  lgamgulmlem2  25169  lgamgulmlem3  25170  lgamgulmlem4  25171  lgamgulmlem5  25172  lgamgulmlem6  25173  lgamgulm2  25175  lgamcvg2  25194  gamcvg  25195  gamcvg2lem  25198  ftalem4  25215  ftalem5  25216  basellem8  25227  logexprlim  25363  bposlem9  25430  2lgslem3d  25537  2sqlem3  25558  dchrmusum2  25596  dchrvmasum2lem  25598  dchrvmasumiflem1  25603  dchrvmasumiflem2  25604  dchrvmaeq0  25606  dchrisum0re  25615  dchrisum0lem1b  25617  dchrisum0lem1  25618  dchrisum0lem2a  25619  dchrisum0lem2  25620  dchrisum0lem3  25621  dchrisum0  25622  mudivsum  25632  vmalogdivsum2  25640  vmalogdivsum  25641  2vmadivsumlem  25642  selberg2  25653  selberg3lem1  25659  selberg3  25661  selberg4lem1  25662  selbergr  25670  selberg3r  25671  selberg4r  25672  selberg34r  25673  pntrlog2bndlem1  25679  pntrlog2bndlem2  25680  pntrlog2bndlem3  25681  pntrlog2bndlem4  25682  pntrlog2bndlem5  25683  colinearalg  26209  axcontlem8  26270  pjhthlem1  28794  eigvalcl  29364  riesz3i  29465  bcm1n  30090  divnumden2  30100  oddpwdc  30950  signsplypnf  31163  signsply0  31164  itgexpif  31222  hgt750leme  31274  subfacval2  31704  divcnvlin  32149  bcprod  32155  iprodgam  32159  unbdqndv2lem1  33021  knoppndvlem2  33025  knoppndvlem7  33030  knoppndvlem9  33032  knoppndvlem10  33033  knoppndvlem16  33039  knoppndvlem17  33040  itg2addnclem  33997  iblmulc2nc  34011  ftc1cnnclem  34019  areacirclem1  34036  areacirclem4  34039  areacirc  34041  cntotbnd  34130  pellexlem2  38231  pellexlem6  38235  jm2.19  38396  jm2.27c  38410  proot1ex  38615  cvgdvgrat  39345  radcnvrat  39346  hashnzfzclim  39354  bcccl  39371  bccm1k  39374  binomcxplemrat  39382  binomcxplemfrat  39383  binomcxplemnotnn0  39388  xralrple2  40360  mccllem  40617  clim1fr1  40621  0ellimcdiv  40669  coseq0  40863  fperdvper  40921  dvdivbd  40926  dvnmptdivc  40941  dvnxpaek  40945  dvnprodlem2  40950  iblsplit  40969  itgcoscmulx  40972  itgsincmulx  40977  stoweidlem11  41015  stoweidlem26  41030  stoweidlem42  41046  wallispilem4  41072  wallispilem5  41073  wallispi  41074  wallispi2lem1  41075  wallispi2lem2  41076  wallispi2  41077  stirlinglem1  41078  stirlinglem3  41080  stirlinglem4  41081  stirlinglem5  41082  stirlinglem6  41083  stirlinglem7  41084  stirlinglem13  41090  stirlinglem14  41091  stirlinglem15  41092  dirkeritg  41106  dirkercncflem1  41107  dirkercncflem2  41108  fourierdlem26  41137  fourierdlem39  41150  fourierdlem56  41166  fourierdlem62  41172  fourierdlem72  41182  fourierdlem74  41184  fourierdlem75  41185  fourierdlem76  41186  fourierdlem80  41190  fourierdlem103  41213  fourierdlem104  41214  fouriersw  41235  elaa2lem  41237  etransclem15  41253  etransclem20  41258  etransclem21  41259  etransclem22  41260  etransclem23  41261  etransclem24  41262  etransclem25  41263  etransclem31  41269  etransclem32  41270  etransclem33  41271  etransclem34  41272  etransclem35  41273  etransclem47  41285  etransclem48  41286  hoiqssbllem2  41624  sigardiv  41837  sharhght  41841  fmtnoprmfac2lem1  42301  fdivmptf  43175  affinecomb2  43265  eenglngeehlnmlem1  43281  eenglngeehlnmlem2  43282  itsclc0lem5  43305  cotcl  43384