Theorem divcld 12100

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ≠ wne 2955  (class class class)co 7424  ℂcc 11205  0cc0 11207   / cdiv 11980

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-er 8724  df-en 8981  df-dom 8982  df-sdom 8983  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551  df-div 11981

This theorem is used by:  dmdcan2d  12130  mulsubdivbinom2  14413  hashf1  14609  abs1m  15512  abslem2  15516  sqreulem  15536  sqreu  15537  o1fsum  15989  divrcnv  16030  divcnv  16031  geolim  16048  geolim2  16049  geo2sum  16051  geo2lim  16053  fproddiv  16137  bpolycl  16227  bpolysum  16228  bpolydiflem  16229  bpoly4  16234  eftcl  16248  efaddlem  16268  tancl  16306  tanval2  16310  qredeq  16841  pcaddlem  17075  pjthlem1  25767  iblss  26134  itgeqa  26143  iblconst  26147  iblabsr  26159  iblmulc2  26160  itgsplit  26165  dvlem  26225  dvmulbr  26268  dvcobr  26275  dvrec  26284  dvrecg  26302  dvmptdiv  26303  dvcnvlem  26305  dveflem  26308  dvsincos  26310  dvlip  26322  c1liplem1  26325  lhop1lem  26342  lhop1  26343  lhop2  26344  lhop  26345  ftc1lem4  26368  vieta1lem2  26643  vieta1  26644  elqaalem3  26653  aareccl  26662  aalioulem1  26668  taylfvallem1  26693  tayl0  26698  taylply2  26704  taylply  26705  dvtaylp  26706  taylthlem2  26710  ulmdvlem1  26736  tanregt0  26876  eff1olem  26885  argregt0  26947  argrege0  26948  argimgt0  26949  logcnlem4  26982  advlogexp  26992  logtaylsum  26998  logtayl2  26999  root1eq1  27092  logbcl  27104  cxplogb  27123  logbf  27126  angcld  27142  angrteqvd  27143  cosangneg2d  27144  angrtmuld  27145  ang180lem1  27146  ang180lem2  27147  ang180lem3  27148  ang180lem4  27149  ang180lem5  27150  lawcoslem1  27152  lawcos  27153  isosctrlem2  27156  isosctrlem3  27157  angpieqvdlem  27165  angpieqvdlem2  27166  angpieqvd  27168  dcubic1lem  27180  dcubic2  27181  dcubic1  27182  dcubic  27183  mcubic  27184  cubic2  27185  dquartlem1  27188  dquartlem2  27189  dquart  27190  quart1cl  27191  quart1lem  27192  quart1  27193  quartlem3  27196  quartlem4  27197  quart  27198  tanatan  27256  atantayl  27274  atantayl2  27275  atantayl3  27276  log2cnv  27281  birthdaylem2  27289  efrlim  27306  dfef2  27307  cxploglim2  27315  fsumharmonic  27348  lgamgulmlem2  27366  lgamgulmlem3  27367  lgamgulmlem4  27368  lgamgulmlem5  27369  lgamgulmlem6  27370  lgamgulm2  27372  lgamcvg2  27391  gamcvg  27392  gamcvg2lem  27395  ftalem4  27412  ftalem5  27413  basellem8  27424  logexprlim  27561  bposlem9  27628  2lgslem3d  27735  2sqlem3  27756  dchrmusum2  27830  dchrvmasum2lem  27832  dchrvmasumiflem1  27837  dchrvmasumiflem2  27838  dchrvmaeq0  27840  dchrisum0re  27849  dchrisum0lem1b  27851  dchrisum0lem1  27852  dchrisum0lem2a  27853  dchrisum0lem2  27854  dchrisum0lem3  27855  dchrisum0  27856  mudivsum  27866  vmalogdivsum2  27874  vmalogdivsum  27875  2vmadivsumlem  27876  selberg2  27887  selberg3lem1  27893  selberg3  27895  selberg4lem1  27896  selbergr  27904  selberg3r  27905  selberg4r  27906  selberg34r  27907  pntrlog2bndlem1  27913  pntrlog2bndlem2  27914  pntrlog2bndlem3  27915  pntrlog2bndlem4  27916  pntrlog2bndlem5  27917  colinearalg  29497  axcontlem8  29558  nrt2irr  31083  pjhthlem1  32002  eigvalcl  32572  riesz3i  32673  quad3d  33391  bcm1n  33437  divnumden2  33457  zringfrac  34136  constrrtlc1  34414  constrrtcclem  34416  constrfin  34428  constrdircl  34447  constrreinvcl  34454  constrsqrtcl  34461  cos9thpiminplylem2  34465  cos9thpiminplylem3  34466  cos9thpiminply  34470  cos9thpinconstrlem1  34471  cos9thpinconstrlem2  34472  cos9thpinconstr  34473  oddpwdc  35036  signsplypnf  35229  signsply0  35230  itgexpif  35285  hgt750leme  35337  subfacval2  36042  divcnvlin  36594  bcprod  36599  iprodgam  36603  unbdqndv2lem1  37471  knoppndvlem2  37475  knoppndvlem7  37480  knoppndvlem9  37482  knoppndvlem10  37483  knoppndvlem16  37489  knoppndvlem17  37490  itg2addnclem  38698  iblmulc2nc  38712  ftc1cnnclem  38718  areacirclem1  38735  areacirclem4  38738  areacirc  38740  cntotbnd  38839  recbothd  43151  lcmineqlem12  43199  lcmineqlem18  43205  dvrelogpow2b  43227  aks4d1p1p2  43229  aks4d1p1p7  43233  aks6d1c2p2  43278  aks6d1c4  43283  2ap1caineq  43304  aks6d1c7lem1  43339  quadfac  43364  pellexlem2  43946  pellexlem6  43950  jm2.19  44109  jm2.27c  44123  proot1ex  44307  cvgdvgrat  45406  radcnvrat  45407  hashnzfzclim  45415  bcccl  45432  bccm1k  45435  binomcxplemrat  45443  binomcxplemfrat  45444  binomcxplemnotnn0  45449  xralrple2  46474  mccllem  46717  clim1fr1  46721  0ellimcdiv  46767  coseq0  46982  fperdvper  47037  dvdivbd  47041  dvnmptdivc  47056  dvnxpaek  47060  dvnprodlem2  47065  iblsplit  47084  itgcoscmulx  47087  itgsincmulx  47092  stoweidlem11  47129  stoweidlem26  47144  stoweidlem42  47160  wallispilem4  47186  wallispilem5  47187  wallispi  47188  wallispi2lem1  47189  wallispi2lem2  47190  wallispi2  47191  stirlinglem1  47192  stirlinglem3  47194  stirlinglem4  47195  stirlinglem5  47196  stirlinglem6  47197  stirlinglem7  47198  stirlinglem13  47204  stirlinglem14  47205  stirlinglem15  47206  dirkeritg  47220  dirkercncflem1  47221  dirkercncflem2  47222  fourierdlem26  47251  fourierdlem39  47264  fourierdlem56  47280  fourierdlem62  47286  fourierdlem72  47296  fourierdlem74  47298  fourierdlem75  47299  fourierdlem76  47300  fourierdlem80  47304  fourierdlem103  47327  fourierdlem104  47328  fouriersw  47349  elaa2lem  47351  etransclem15  47367  etransclem20  47372  etransclem21  47373  etransclem22  47374  etransclem23  47375  etransclem24  47376  etransclem25  47377  etransclem31  47383  etransclem32  47384  etransclem33  47385  etransclem34  47386  etransclem35  47387  etransclem47  47399  etransclem48  47400  hoiqssbllem2  47741  sigardiv  47979  sharhght  47983  cndivrenred  48484  fmtnoprmfac2lem1  48759  quad1  48826  requad01  48827  requad1  48828  fdivmptf  49761  affinecomb2  49923  eenglngeehlnmlem1  49958  eenglngeehlnmlem2  49959  itscnhlc0xyqsol  49985  itschlc0xyqsol1  49986  cotcl  51028  dvsec  51039  dvcsc  51040  dvcot  51041