Theorem divcld 11447

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

Syntax hints:   → wi 4   ∈ wcel 2112   ≠ wne 2952  (class class class)co 7151  ℂcc 10566  0cc0 10568   / cdiv 11328

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644  ax-pre-mulgt0 10645

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-po 5444  df-so 5445  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-pnf 10708  df-mnf 10709  df-xr 10710  df-ltxr 10711  df-le 10712  df-sub 10903  df-neg 10904  df-div 11329

This theorem is referenced by:  dmdcan2d  11477  mulsubdivbinom2  13665  hashf1  13860  abs1m  14736  abslem2  14740  sqreulem  14760  sqreu  14761  o1fsum  15209  divrcnv  15248  divcnv  15249  geolim  15267  geolim2  15268  geo2sum  15270  geo2lim  15272  fproddiv  15356  bpolycl  15447  bpolysum  15448  bpolydiflem  15449  bpoly4  15454  eftcl  15468  efaddlem  15487  tancl  15523  tanval2  15527  qredeq  16046  pcaddlem  16272  pjthlem1  24130  iblss  24497  itgeqa  24506  iblconst  24510  iblabsr  24522  iblmulc2  24523  itgsplit  24528  dvlem  24588  dvmulbr  24631  dvcobr  24638  dvrec  24647  dvrecg  24665  dvmptdiv  24666  dvcnvlem  24668  dveflem  24671  dvsincos  24673  dvlip  24685  c1liplem1  24688  lhop1lem  24705  lhop1  24706  lhop2  24707  lhop  24708  ftc1lem4  24731  vieta1lem2  24999  vieta1  25000  elqaalem3  25009  aareccl  25014  aalioulem1  25020  taylfvallem1  25044  tayl0  25049  taylply2  25055  taylply  25056  dvtaylp  25057  taylthlem2  25061  ulmdvlem1  25087  tanregt0  25223  eff1olem  25232  argregt0  25293  argrege0  25294  argimgt0  25295  logcnlem4  25328  advlogexp  25338  logtaylsum  25344  logtayl2  25345  root1eq1  25436  logbcl  25445  cxplogb  25464  logbf  25467  angcld  25483  angrteqvd  25484  cosangneg2d  25485  angrtmuld  25486  ang180lem1  25487  ang180lem2  25488  ang180lem3  25489  ang180lem4  25490  ang180lem5  25491  lawcoslem1  25493  lawcos  25494  isosctrlem2  25497  isosctrlem3  25498  angpieqvdlem  25506  angpieqvdlem2  25507  angpieqvd  25509  dcubic1lem  25521  dcubic2  25522  dcubic1  25523  dcubic  25524  mcubic  25525  cubic2  25526  dquartlem1  25529  dquartlem2  25530  dquart  25531  quart1cl  25532  quart1lem  25533  quart1  25534  quartlem3  25537  quartlem4  25538  quart  25539  tanatan  25597  atantayl  25615  atantayl2  25616  atantayl3  25617  log2cnv  25622  birthdaylem2  25630  efrlim  25647  dfef2  25648  cxploglim2  25656  fsumharmonic  25689  lgamgulmlem2  25707  lgamgulmlem3  25708  lgamgulmlem4  25709  lgamgulmlem5  25710  lgamgulmlem6  25711  lgamgulm2  25713  lgamcvg2  25732  gamcvg  25733  gamcvg2lem  25736  ftalem4  25753  ftalem5  25754  basellem8  25765  logexprlim  25901  bposlem9  25968  2lgslem3d  26075  2sqlem3  26096  dchrmusum2  26170  dchrvmasum2lem  26172  dchrvmasumiflem1  26177  dchrvmasumiflem2  26178  dchrvmaeq0  26180  dchrisum0re  26189  dchrisum0lem1b  26191  dchrisum0lem1  26192  dchrisum0lem2a  26193  dchrisum0lem2  26194  dchrisum0lem3  26195  dchrisum0  26196  mudivsum  26206  vmalogdivsum2  26214  vmalogdivsum  26215  2vmadivsumlem  26216  selberg2  26227  selberg3lem1  26233  selberg3  26235  selberg4lem1  26236  selbergr  26244  selberg3r  26245  selberg4r  26246  selberg34r  26247  pntrlog2bndlem1  26253  pntrlog2bndlem2  26254  pntrlog2bndlem3  26255  pntrlog2bndlem4  26256  pntrlog2bndlem5  26257  colinearalg  26796  axcontlem8  26857  pjhthlem1  29266  eigvalcl  29836  riesz3i  29937  bcm1n  30633  divnumden2  30649  oddpwdc  31833  signsplypnf  32041  signsply0  32042  itgexpif  32098  hgt750leme  32150  subfacval2  32658  divcnvlin  33206  bcprod  33212  iprodgam  33216  unbdqndv2lem1  34231  knoppndvlem2  34235  knoppndvlem7  34240  knoppndvlem9  34242  knoppndvlem10  34243  knoppndvlem16  34249  knoppndvlem17  34250  itg2addnclem  35381  iblmulc2nc  35395  ftc1cnnclem  35401  areacirclem1  35418  areacirclem4  35421  areacirc  35423  cntotbnd  35507  recbothd  39553  lcmineqlem12  39600  lcmineqlem18  39606  dvrelogpow2b  39627  aks4d1p1p2  39629  aks4d1p1p7  39633  2ap1caineq  39639  pellexlem2  40137  pellexlem6  40141  jm2.19  40300  jm2.27c  40314  proot1ex  40511  cvgdvgrat  41383  radcnvrat  41384  hashnzfzclim  41392  bcccl  41409  bccm1k  41412  binomcxplemrat  41420  binomcxplemfrat  41421  binomcxplemnotnn0  41426  xralrple2  42347  mccllem  42598  clim1fr1  42602  0ellimcdiv  42650  coseq0  42865  fperdvper  42920  dvdivbd  42924  dvnmptdivc  42939  dvnxpaek  42943  dvnprodlem2  42948  iblsplit  42967  itgcoscmulx  42970  itgsincmulx  42975  stoweidlem11  43012  stoweidlem26  43027  stoweidlem42  43043  wallispilem4  43069  wallispilem5  43070  wallispi  43071  wallispi2lem1  43072  wallispi2lem2  43073  wallispi2  43074  stirlinglem1  43075  stirlinglem3  43077  stirlinglem4  43078  stirlinglem5  43079  stirlinglem6  43080  stirlinglem7  43081  stirlinglem13  43087  stirlinglem14  43088  stirlinglem15  43089  dirkeritg  43103  dirkercncflem1  43104  dirkercncflem2  43105  fourierdlem26  43134  fourierdlem39  43147  fourierdlem56  43163  fourierdlem62  43169  fourierdlem72  43179  fourierdlem74  43181  fourierdlem75  43182  fourierdlem76  43183  fourierdlem80  43187  fourierdlem103  43210  fourierdlem104  43211  fouriersw  43232  elaa2lem  43234  etransclem15  43250  etransclem20  43255  etransclem21  43256  etransclem22  43257  etransclem23  43258  etransclem24  43259  etransclem25  43260  etransclem31  43266  etransclem32  43267  etransclem33  43268  etransclem34  43269  etransclem35  43270  etransclem47  43282  etransclem48  43283  hoiqssbllem2  43621  sigardiv  43834  sharhght  43838  cndivrenred  44224  fmtnoprmfac2lem1  44444  quad1  44498  requad01  44499  requad1  44500  fdivmptf  45313  affinecomb2  45475  eenglngeehlnmlem1  45509  eenglngeehlnmlem2  45510  itscnhlc0xyqsol  45537  itschlc0xyqsol1  45538  cotcl  45662