Theorem divcld 12022

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2933  (class class class)co 7410  ℂcc 11132  0cc0 11134   / cdiv 11899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-po 5566  df-so 5567  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-div 11900

This theorem is referenced by:  dmdcan2d  12052  mulsubdivbinom2  14285  hashf1  14480  abs1m  15359  abslem2  15363  sqreulem  15383  sqreu  15384  o1fsum  15834  divrcnv  15873  divcnv  15874  geolim  15891  geolim2  15892  geo2sum  15894  geo2lim  15896  fproddiv  15982  bpolycl  16073  bpolysum  16074  bpolydiflem  16075  bpoly4  16080  eftcl  16094  efaddlem  16114  tancl  16152  tanval2  16156  qredeq  16681  pcaddlem  16913  pjthlem1  25394  iblss  25763  itgeqa  25772  iblconst  25776  iblabsr  25788  iblmulc2  25789  itgsplit  25794  dvlem  25854  dvmulbr  25898  dvmulbrOLD  25899  dvcobr  25906  dvcobrOLD  25907  dvrec  25916  dvrecg  25934  dvmptdiv  25935  dvcnvlem  25937  dveflem  25940  dvsincos  25942  dvlip  25955  c1liplem1  25958  lhop1lem  25975  lhop1  25976  lhop2  25977  lhop  25978  ftc1lem4  26003  vieta1lem2  26276  vieta1  26277  elqaalem3  26286  aareccl  26291  aalioulem1  26297  taylfvallem1  26321  tayl0  26326  taylply2  26332  taylply2OLD  26333  taylply  26334  dvtaylp  26335  taylthlem2  26339  taylthlem2OLD  26340  ulmdvlem1  26366  tanregt0  26505  eff1olem  26514  argregt0  26576  argrege0  26577  argimgt0  26578  logcnlem4  26611  advlogexp  26621  logtaylsum  26627  logtayl2  26628  root1eq1  26722  logbcl  26734  cxplogb  26753  logbf  26756  angcld  26772  angrteqvd  26773  cosangneg2d  26774  angrtmuld  26775  ang180lem1  26776  ang180lem2  26777  ang180lem3  26778  ang180lem4  26779  ang180lem5  26780  lawcoslem1  26782  lawcos  26783  isosctrlem2  26786  isosctrlem3  26787  angpieqvdlem  26795  angpieqvdlem2  26796  angpieqvd  26798  dcubic1lem  26810  dcubic2  26811  dcubic1  26812  dcubic  26813  mcubic  26814  cubic2  26815  dquartlem1  26818  dquartlem2  26819  dquart  26820  quart1cl  26821  quart1lem  26822  quart1  26823  quartlem3  26826  quartlem4  26827  quart  26828  tanatan  26886  atantayl  26904  atantayl2  26905  atantayl3  26906  log2cnv  26911  birthdaylem2  26919  efrlim  26936  efrlimOLD  26937  dfef2  26938  cxploglim2  26946  fsumharmonic  26979  lgamgulmlem2  26997  lgamgulmlem3  26998  lgamgulmlem4  26999  lgamgulmlem5  27000  lgamgulmlem6  27001  lgamgulm2  27003  lgamcvg2  27022  gamcvg  27023  gamcvg2lem  27026  ftalem4  27043  ftalem5  27044  basellem8  27055  logexprlim  27193  bposlem9  27260  2lgslem3d  27367  2sqlem3  27388  dchrmusum2  27462  dchrvmasum2lem  27464  dchrvmasumiflem1  27469  dchrvmasumiflem2  27470  dchrvmaeq0  27472  dchrisum0re  27481  dchrisum0lem1b  27483  dchrisum0lem1  27484  dchrisum0lem2a  27485  dchrisum0lem2  27486  dchrisum0lem3  27487  dchrisum0  27488  mudivsum  27498  vmalogdivsum2  27506  vmalogdivsum  27507  2vmadivsumlem  27508  selberg2  27519  selberg3lem1  27525  selberg3  27527  selberg4lem1  27528  selbergr  27536  selberg3r  27537  selberg4r  27538  selberg34r  27539  pntrlog2bndlem1  27545  pntrlog2bndlem2  27546  pntrlog2bndlem3  27547  pntrlog2bndlem4  27548  pntrlog2bndlem5  27549  colinearalg  28894  axcontlem8  28955  nrt2irr  30459  pjhthlem1  31377  eigvalcl  31947  riesz3i  32048  quad3d  32732  bcm1n  32777  divnumden2  32799  zringfrac  33574  constrrtlc1  33771  constrrtcclem  33773  constrfin  33785  constrdircl  33804  constrreinvcl  33811  constrsqrtcl  33818  cos9thpiminplylem2  33822  cos9thpiminplylem3  33823  cos9thpiminply  33827  cos9thpinconstrlem1  33828  oddpwdc  34391  signsplypnf  34587  signsply0  34588  itgexpif  34643  hgt750leme  34695  subfacval2  35214  divcnvlin  35755  bcprod  35760  iprodgam  35764  unbdqndv2lem1  36532  knoppndvlem2  36536  knoppndvlem7  36541  knoppndvlem9  36543  knoppndvlem10  36544  knoppndvlem16  36550  knoppndvlem17  36551  itg2addnclem  37700  iblmulc2nc  37714  ftc1cnnclem  37720  areacirclem1  37737  areacirclem4  37740  areacirc  37742  cntotbnd  37825  recbothd  42010  lcmineqlem12  42058  lcmineqlem18  42064  dvrelogpow2b  42086  aks4d1p1p2  42088  aks4d1p1p7  42092  aks6d1c2p2  42137  aks6d1c4  42142  2ap1caineq  42163  aks6d1c7lem1  42198  pellexlem2  42828  pellexlem6  42832  jm2.19  42992  jm2.27c  43006  proot1ex  43195  cvgdvgrat  44312  radcnvrat  44313  hashnzfzclim  44321  bcccl  44338  bccm1k  44341  binomcxplemrat  44349  binomcxplemfrat  44350  binomcxplemnotnn0  44355  xralrple2  45361  mccllem  45606  clim1fr1  45610  0ellimcdiv  45658  coseq0  45873  fperdvper  45928  dvdivbd  45932  dvnmptdivc  45947  dvnxpaek  45951  dvnprodlem2  45956  iblsplit  45975  itgcoscmulx  45978  itgsincmulx  45983  stoweidlem11  46020  stoweidlem26  46035  stoweidlem42  46051  wallispilem4  46077  wallispilem5  46078  wallispi  46079  wallispi2lem1  46080  wallispi2lem2  46081  wallispi2  46082  stirlinglem1  46083  stirlinglem3  46085  stirlinglem4  46086  stirlinglem5  46087  stirlinglem6  46088  stirlinglem7  46089  stirlinglem13  46095  stirlinglem14  46096  stirlinglem15  46097  dirkeritg  46111  dirkercncflem1  46112  dirkercncflem2  46113  fourierdlem26  46142  fourierdlem39  46155  fourierdlem56  46171  fourierdlem62  46177  fourierdlem72  46187  fourierdlem74  46189  fourierdlem75  46190  fourierdlem76  46191  fourierdlem80  46195  fourierdlem103  46218  fourierdlem104  46219  fouriersw  46240  elaa2lem  46242  etransclem15  46258  etransclem20  46263  etransclem21  46264  etransclem22  46265  etransclem23  46266  etransclem24  46267  etransclem25  46268  etransclem31  46274  etransclem32  46275  etransclem33  46276  etransclem34  46277  etransclem35  46278  etransclem47  46290  etransclem48  46291  hoiqssbllem2  46632  sigardiv  46870  sharhght  46874  cndivrenred  47315  fmtnoprmfac2lem1  47560  quad1  47614  requad01  47615  requad1  47616  fdivmptf  48501  affinecomb2  48663  eenglngeehlnmlem1  48697  eenglngeehlnmlem2  48698  itscnhlc0xyqsol  48725  itschlc0xyqsol1  48726  cotcl  49596