Theorem divcld 12015

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2955  (class class class)co 7413  ℂcc 11122  0cc0 11124   / cdiv 11895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-div 11896

This theorem is used by:  dmdcan2d  12045  mulsubdivbinom2  14326  hashf1  14522  abs1m  15423  abslem2  15427  sqreulem  15447  sqreu  15448  o1fsum  15900  divrcnv  15941  divcnv  15942  geolim  15959  geolim2  15960  geo2sum  15962  geo2lim  15964  fproddiv  16048  bpolycl  16138  bpolysum  16139  bpolydiflem  16140  bpoly4  16145  eftcl  16159  efaddlem  16179  tancl  16217  tanval2  16221  qredeq  16747  pcaddlem  16980  pjthlem1  25665  iblss  26032  itgeqa  26041  iblconst  26045  iblabsr  26057  iblmulc2  26058  itgsplit  26063  dvlem  26123  dvmulbr  26166  dvcobr  26173  dvrec  26182  dvrecg  26200  dvmptdiv  26201  dvcnvlem  26203  dveflem  26206  dvsincos  26208  dvlip  26220  c1liplem1  26223  lhop1lem  26240  lhop1  26241  lhop2  26242  lhop  26243  ftc1lem4  26266  vieta1lem2  26543  vieta1  26544  elqaalem3  26553  aareccl  26562  aalioulem1  26568  taylfvallem1  26593  tayl0  26598  taylply2  26604  taylply  26605  dvtaylp  26606  taylthlem2  26610  ulmdvlem1  26636  tanregt0  26776  eff1olem  26785  argregt0  26847  argrege0  26848  argimgt0  26849  logcnlem4  26882  advlogexp  26892  logtaylsum  26898  logtayl2  26899  root1eq1  26992  logbcl  27004  cxplogb  27023  logbf  27026  angcld  27042  angrteqvd  27043  cosangneg2d  27044  angrtmuld  27045  ang180lem1  27046  ang180lem2  27047  ang180lem3  27048  ang180lem4  27049  ang180lem5  27050  lawcoslem1  27052  lawcos  27053  isosctrlem2  27056  isosctrlem3  27057  angpieqvdlem  27065  angpieqvdlem2  27066  angpieqvd  27068  dcubic1lem  27080  dcubic2  27081  dcubic1  27082  dcubic  27083  mcubic  27084  cubic2  27085  dquartlem1  27088  dquartlem2  27089  dquart  27090  quart1cl  27091  quart1lem  27092  quart1  27093  quartlem3  27096  quartlem4  27097  quart  27098  tanatan  27156  atantayl  27174  atantayl2  27175  atantayl3  27176  log2cnv  27181  birthdaylem2  27189  efrlim  27206  dfef2  27207  cxploglim2  27215  fsumharmonic  27248  lgamgulmlem2  27266  lgamgulmlem3  27267  lgamgulmlem4  27268  lgamgulmlem5  27269  lgamgulmlem6  27270  lgamgulm2  27272  lgamcvg2  27291  gamcvg  27292  gamcvg2lem  27295  ftalem4  27312  ftalem5  27313  basellem8  27324  logexprlim  27461  bposlem9  27528  2lgslem3d  27635  2sqlem3  27656  dchrmusum2  27730  dchrvmasum2lem  27732  dchrvmasumiflem1  27737  dchrvmasumiflem2  27738  dchrvmaeq0  27740  dchrisum0re  27749  dchrisum0lem1b  27751  dchrisum0lem1  27752  dchrisum0lem2a  27753  dchrisum0lem2  27754  dchrisum0lem3  27755  dchrisum0  27756  mudivsum  27766  vmalogdivsum2  27774  vmalogdivsum  27775  2vmadivsumlem  27776  selberg2  27787  selberg3lem1  27793  selberg3  27795  selberg4lem1  27796  selbergr  27804  selberg3r  27805  selberg4r  27806  selberg34r  27807  pntrlog2bndlem1  27813  pntrlog2bndlem2  27814  pntrlog2bndlem3  27815  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  colinearalg  29367  axcontlem8  29428  nrt2irr  30953  pjhthlem1  31872  eigvalcl  32442  riesz3i  32543  quad3d  33220  bcm1n  33266  divnumden2  33286  zringfrac  33964  constrrtlc1  34242  constrrtcclem  34244  constrfin  34256  constrdircl  34275  constrreinvcl  34282  constrsqrtcl  34289  cos9thpiminplylem2  34293  cos9thpiminplylem3  34294  cos9thpiminply  34298  cos9thpinconstrlem1  34299  cos9thpinconstrlem2  34300  cos9thpinconstr  34301  oddpwdc  34865  signsplypnf  35058  signsply0  35059  itgexpif  35114  hgt750leme  35166  subfacval2  35766  divcnvlin  36312  bcprod  36317  iprodgam  36321  unbdqndv2lem1  37206  knoppndvlem2  37210  knoppndvlem7  37215  knoppndvlem9  37217  knoppndvlem10  37218  knoppndvlem16  37224  knoppndvlem17  37225  itg2addnclem  38420  iblmulc2nc  38434  ftc1cnnclem  38440  areacirclem1  38457  areacirclem4  38460  areacirc  38462  cntotbnd  38546  recbothd  42858  lcmineqlem12  42906  lcmineqlem18  42912  dvrelogpow2b  42934  aks4d1p1p2  42936  aks4d1p1p7  42940  aks6d1c2p2  42985  aks6d1c4  42990  2ap1caineq  43011  aks6d1c7lem1  43046  quadfac  43071  pellexlem2  43671  pellexlem6  43675  jm2.19  43834  jm2.27c  43848  proot1ex  44037  cvgdvgrat  45137  radcnvrat  45138  hashnzfzclim  45146  bcccl  45163  bccm1k  45166  binomcxplemrat  45174  binomcxplemfrat  45175  binomcxplemnotnn0  45180  xralrple2  46184  mccllem  46427  clim1fr1  46431  0ellimcdiv  46477  coseq0  46692  fperdvper  46747  dvdivbd  46751  dvnmptdivc  46766  dvnxpaek  46770  dvnprodlem2  46775  iblsplit  46794  itgcoscmulx  46797  itgsincmulx  46802  stoweidlem11  46839  stoweidlem26  46854  stoweidlem42  46870  wallispilem4  46896  wallispilem5  46897  wallispi  46898  wallispi2lem1  46899  wallispi2lem2  46900  wallispi2  46901  stirlinglem1  46902  stirlinglem3  46904  stirlinglem4  46905  stirlinglem5  46906  stirlinglem6  46907  stirlinglem7  46908  stirlinglem13  46914  stirlinglem14  46915  stirlinglem15  46916  dirkeritg  46930  dirkercncflem1  46931  dirkercncflem2  46932  fourierdlem26  46961  fourierdlem39  46974  fourierdlem56  46990  fourierdlem62  46996  fourierdlem72  47006  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem80  47014  fourierdlem103  47037  fourierdlem104  47038  fouriersw  47059  elaa2lem  47061  etransclem15  47077  etransclem20  47082  etransclem21  47083  etransclem22  47084  etransclem23  47085  etransclem24  47086  etransclem25  47087  etransclem31  47093  etransclem32  47094  etransclem33  47095  etransclem34  47096  etransclem35  47097  etransclem47  47109  etransclem48  47110  hoiqssbllem2  47451  sigardiv  47689  sharhght  47693  cndivrenred  48194  fmtnoprmfac2lem1  48469  quad1  48536  requad01  48537  requad1  48538  fdivmptf  49471  affinecomb2  49633  eenglngeehlnmlem1  49667  eenglngeehlnmlem2  49668  itscnhlc0xyqsol  49695  itschlc0xyqsol1  49696  cotcl  50678  dvsec  50689  dvcsc  50690  dvcot  50691