Theorem divcld 11977

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

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2941  (class class class)co 7396  ℂcc 11095  0cc0 11097   / cdiv 11858

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712  ax-resscn 11154  ax-1cn 11155  ax-icn 11156  ax-addcl 11157  ax-addrcl 11158  ax-mulcl 11159  ax-mulrcl 11160  ax-mulcom 11161  ax-addass 11162  ax-mulass 11163  ax-distr 11164  ax-i2m1 11165  ax-1ne0 11166  ax-1rid 11167  ax-rnegex 11168  ax-rrecex 11169  ax-cnre 11170  ax-pre-lttri 11171  ax-pre-lttrn 11172  ax-pre-ltadd 11173  ax-pre-mulgt0 11174

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-br 5145  df-opab 5207  df-mpt 5228  df-id 5570  df-po 5584  df-so 5585  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-riota 7352  df-ov 7399  df-oprab 7400  df-mpo 7401  df-er 8691  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11237  df-mnf 11238  df-xr 11239  df-ltxr 11240  df-le 11241  df-sub 11433  df-neg 11434  df-div 11859

This theorem is referenced by:  dmdcan2d  12007  mulsubdivbinom2  14209  hashf1  14405  abs1m  15269  abslem2  15273  sqreulem  15293  sqreu  15294  o1fsum  15746  divrcnv  15785  divcnv  15786  geolim  15803  geolim2  15804  geo2sum  15806  geo2lim  15808  fproddiv  15892  bpolycl  15983  bpolysum  15984  bpolydiflem  15985  bpoly4  15990  eftcl  16004  efaddlem  16023  tancl  16059  tanval2  16063  qredeq  16581  pcaddlem  16808  pjthlem1  24923  iblss  25291  itgeqa  25300  iblconst  25304  iblabsr  25316  iblmulc2  25317  itgsplit  25322  dvlem  25382  dvmulbr  25425  dvcobr  25432  dvrec  25441  dvrecg  25459  dvmptdiv  25460  dvcnvlem  25462  dveflem  25465  dvsincos  25467  dvlip  25479  c1liplem1  25482  lhop1lem  25499  lhop1  25500  lhop2  25501  lhop  25502  ftc1lem4  25525  vieta1lem2  25793  vieta1  25794  elqaalem3  25803  aareccl  25808  aalioulem1  25814  taylfvallem1  25838  tayl0  25843  taylply2  25849  taylply  25850  dvtaylp  25851  taylthlem2  25855  ulmdvlem1  25881  tanregt0  26017  eff1olem  26026  argregt0  26087  argrege0  26088  argimgt0  26089  logcnlem4  26122  advlogexp  26132  logtaylsum  26138  logtayl2  26139  root1eq1  26230  logbcl  26239  cxplogb  26258  logbf  26261  angcld  26277  angrteqvd  26278  cosangneg2d  26279  angrtmuld  26280  ang180lem1  26281  ang180lem2  26282  ang180lem3  26283  ang180lem4  26284  ang180lem5  26285  lawcoslem1  26287  lawcos  26288  isosctrlem2  26291  isosctrlem3  26292  angpieqvdlem  26300  angpieqvdlem2  26301  angpieqvd  26303  dcubic1lem  26315  dcubic2  26316  dcubic1  26317  dcubic  26318  mcubic  26319  cubic2  26320  dquartlem1  26323  dquartlem2  26324  dquart  26325  quart1cl  26326  quart1lem  26327  quart1  26328  quartlem3  26331  quartlem4  26332  quart  26333  tanatan  26391  atantayl  26409  atantayl2  26410  atantayl3  26411  log2cnv  26416  birthdaylem2  26424  efrlim  26441  dfef2  26442  cxploglim2  26450  fsumharmonic  26483  lgamgulmlem2  26501  lgamgulmlem3  26502  lgamgulmlem4  26503  lgamgulmlem5  26504  lgamgulmlem6  26505  lgamgulm2  26507  lgamcvg2  26526  gamcvg  26527  gamcvg2lem  26530  ftalem4  26547  ftalem5  26548  basellem8  26559  logexprlim  26695  bposlem9  26762  2lgslem3d  26869  2sqlem3  26890  dchrmusum2  26964  dchrvmasum2lem  26966  dchrvmasumiflem1  26971  dchrvmasumiflem2  26972  dchrvmaeq0  26974  dchrisum0re  26983  dchrisum0lem1b  26985  dchrisum0lem1  26986  dchrisum0lem2a  26987  dchrisum0lem2  26988  dchrisum0lem3  26989  dchrisum0  26990  mudivsum  27000  vmalogdivsum2  27008  vmalogdivsum  27009  2vmadivsumlem  27010  selberg2  27021  selberg3lem1  27027  selberg3  27029  selberg4lem1  27030  selbergr  27038  selberg3r  27039  selberg4r  27040  selberg34r  27041  pntrlog2bndlem1  27047  pntrlog2bndlem2  27048  pntrlog2bndlem3  27049  pntrlog2bndlem4  27050  pntrlog2bndlem5  27051  colinearalg  28135  axcontlem8  28196  pjhthlem1  30609  eigvalcl  31179  riesz3i  31280  bcm1n  31977  divnumden2  31995  oddpwdc  33284  signsplypnf  33492  signsply0  33493  itgexpif  33549  hgt750leme  33601  subfacval2  34109  divcnvlin  34633  bcprod  34639  iprodgam  34643  unbdqndv2lem1  35290  knoppndvlem2  35294  knoppndvlem7  35299  knoppndvlem9  35301  knoppndvlem10  35302  knoppndvlem16  35308  knoppndvlem17  35309  itg2addnclem  36444  iblmulc2nc  36458  ftc1cnnclem  36464  areacirclem1  36481  areacirclem4  36484  areacirc  36486  cntotbnd  36570  recbothd  40764  lcmineqlem12  40811  lcmineqlem18  40817  dvrelogpow2b  40839  aks4d1p1p2  40841  aks4d1p1p7  40845  aks6d1c2p2  40863  2ap1caineq  40867  pellexlem2  41439  pellexlem6  41443  jm2.19  41603  jm2.27c  41617  proot1ex  41814  cvgdvgrat  42943  radcnvrat  42944  hashnzfzclim  42952  bcccl  42969  bccm1k  42972  binomcxplemrat  42980  binomcxplemfrat  42981  binomcxplemnotnn0  42986  xralrple2  43937  mccllem  44186  clim1fr1  44190  0ellimcdiv  44238  coseq0  44453  fperdvper  44508  dvdivbd  44512  dvnmptdivc  44527  dvnxpaek  44531  dvnprodlem2  44536  iblsplit  44555  itgcoscmulx  44558  itgsincmulx  44563  stoweidlem11  44600  stoweidlem26  44615  stoweidlem42  44631  wallispilem4  44657  wallispilem5  44658  wallispi  44659  wallispi2lem1  44660  wallispi2lem2  44661  wallispi2  44662  stirlinglem1  44663  stirlinglem3  44665  stirlinglem4  44666  stirlinglem5  44667  stirlinglem6  44668  stirlinglem7  44669  stirlinglem13  44675  stirlinglem14  44676  stirlinglem15  44677  dirkeritg  44691  dirkercncflem1  44692  dirkercncflem2  44693  fourierdlem26  44722  fourierdlem39  44735  fourierdlem56  44751  fourierdlem62  44757  fourierdlem72  44767  fourierdlem74  44769  fourierdlem75  44770  fourierdlem76  44771  fourierdlem80  44775  fourierdlem103  44798  fourierdlem104  44799  fouriersw  44820  elaa2lem  44822  etransclem15  44838  etransclem20  44843  etransclem21  44844  etransclem22  44845  etransclem23  44846  etransclem24  44847  etransclem25  44848  etransclem31  44854  etransclem32  44855  etransclem33  44856  etransclem34  44857  etransclem35  44858  etransclem47  44870  etransclem48  44871  hoiqssbllem2  45212  sigardiv  45450  sharhght  45454  cndivrenred  45887  fmtnoprmfac2lem1  46107  quad1  46161  requad01  46162  requad1  46163  fdivmptf  47067  affinecomb2  47229  eenglngeehlnmlem1  47263  eenglngeehlnmlem2  47264  itscnhlc0xyqsol  47291  itschlc0xyqsol1  47292  cotcl  47637