Theorem divcld 12041

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

Syntax hints:   → wi 4   ∈ wcel 2106   ≠ wne 2938  (class class class)co 7431  ℂcc 11151  0cc0 11153   / cdiv 11918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-po 5597  df-so 5598  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919

This theorem is referenced by:  dmdcan2d  12071  mulsubdivbinom2  14298  hashf1  14493  abs1m  15371  abslem2  15375  sqreulem  15395  sqreu  15396  o1fsum  15846  divrcnv  15885  divcnv  15886  geolim  15903  geolim2  15904  geo2sum  15906  geo2lim  15908  fproddiv  15994  bpolycl  16085  bpolysum  16086  bpolydiflem  16087  bpoly4  16092  eftcl  16106  efaddlem  16126  tancl  16162  tanval2  16166  qredeq  16691  pcaddlem  16922  pjthlem1  25485  iblss  25855  itgeqa  25864  iblconst  25868  iblabsr  25880  iblmulc2  25881  itgsplit  25886  dvlem  25946  dvmulbr  25990  dvmulbrOLD  25991  dvcobr  25998  dvcobrOLD  25999  dvrec  26008  dvrecg  26026  dvmptdiv  26027  dvcnvlem  26029  dveflem  26032  dvsincos  26034  dvlip  26047  c1liplem1  26050  lhop1lem  26067  lhop1  26068  lhop2  26069  lhop  26070  ftc1lem4  26095  vieta1lem2  26368  vieta1  26369  elqaalem3  26378  aareccl  26383  aalioulem1  26389  taylfvallem1  26413  tayl0  26418  taylply2  26424  taylply2OLD  26425  taylply  26426  dvtaylp  26427  taylthlem2  26431  taylthlem2OLD  26432  ulmdvlem1  26458  tanregt0  26596  eff1olem  26605  argregt0  26667  argrege0  26668  argimgt0  26669  logcnlem4  26702  advlogexp  26712  logtaylsum  26718  logtayl2  26719  root1eq1  26813  logbcl  26825  cxplogb  26844  logbf  26847  angcld  26863  angrteqvd  26864  cosangneg2d  26865  angrtmuld  26866  ang180lem1  26867  ang180lem2  26868  ang180lem3  26869  ang180lem4  26870  ang180lem5  26871  lawcoslem1  26873  lawcos  26874  isosctrlem2  26877  isosctrlem3  26878  angpieqvdlem  26886  angpieqvdlem2  26887  angpieqvd  26889  dcubic1lem  26901  dcubic2  26902  dcubic1  26903  dcubic  26904  mcubic  26905  cubic2  26906  dquartlem1  26909  dquartlem2  26910  dquart  26911  quart1cl  26912  quart1lem  26913  quart1  26914  quartlem3  26917  quartlem4  26918  quart  26919  tanatan  26977  atantayl  26995  atantayl2  26996  atantayl3  26997  log2cnv  27002  birthdaylem2  27010  efrlim  27027  efrlimOLD  27028  dfef2  27029  cxploglim2  27037  fsumharmonic  27070  lgamgulmlem2  27088  lgamgulmlem3  27089  lgamgulmlem4  27090  lgamgulmlem5  27091  lgamgulmlem6  27092  lgamgulm2  27094  lgamcvg2  27113  gamcvg  27114  gamcvg2lem  27117  ftalem4  27134  ftalem5  27135  basellem8  27146  logexprlim  27284  bposlem9  27351  2lgslem3d  27458  2sqlem3  27479  dchrmusum2  27553  dchrvmasum2lem  27555  dchrvmasumiflem1  27560  dchrvmasumiflem2  27561  dchrvmaeq0  27563  dchrisum0re  27572  dchrisum0lem1b  27574  dchrisum0lem1  27575  dchrisum0lem2a  27576  dchrisum0lem2  27577  dchrisum0lem3  27578  dchrisum0  27579  mudivsum  27589  vmalogdivsum2  27597  vmalogdivsum  27598  2vmadivsumlem  27599  selberg2  27610  selberg3lem1  27616  selberg3  27618  selberg4lem1  27619  selbergr  27627  selberg3r  27628  selberg4r  27629  selberg34r  27630  pntrlog2bndlem1  27636  pntrlog2bndlem2  27637  pntrlog2bndlem3  27638  pntrlog2bndlem4  27639  pntrlog2bndlem5  27640  colinearalg  28940  axcontlem8  29001  nrt2irr  30502  pjhthlem1  31420  eigvalcl  31990  riesz3i  32091  quad3d  32761  bcm1n  32803  divnumden2  32822  zringfrac  33562  constrrtlc1  33738  constrrtcclem  33740  constrfin  33751  oddpwdc  34336  signsplypnf  34544  signsply0  34545  itgexpif  34600  hgt750leme  34652  subfacval2  35172  divcnvlin  35713  bcprod  35718  iprodgam  35722  unbdqndv2lem1  36492  knoppndvlem2  36496  knoppndvlem7  36501  knoppndvlem9  36503  knoppndvlem10  36504  knoppndvlem16  36510  knoppndvlem17  36511  itg2addnclem  37658  iblmulc2nc  37672  ftc1cnnclem  37678  areacirclem1  37695  areacirclem4  37698  areacirc  37700  cntotbnd  37783  recbothd  41974  lcmineqlem12  42022  lcmineqlem18  42028  dvrelogpow2b  42050  aks4d1p1p2  42052  aks4d1p1p7  42056  aks6d1c2p2  42101  aks6d1c4  42106  2ap1caineq  42127  aks6d1c7lem1  42162  pellexlem2  42818  pellexlem6  42822  jm2.19  42982  jm2.27c  42996  proot1ex  43185  cvgdvgrat  44309  radcnvrat  44310  hashnzfzclim  44318  bcccl  44335  bccm1k  44338  binomcxplemrat  44346  binomcxplemfrat  44347  binomcxplemnotnn0  44352  xralrple2  45304  mccllem  45553  clim1fr1  45557  0ellimcdiv  45605  coseq0  45820  fperdvper  45875  dvdivbd  45879  dvnmptdivc  45894  dvnxpaek  45898  dvnprodlem2  45903  iblsplit  45922  itgcoscmulx  45925  itgsincmulx  45930  stoweidlem11  45967  stoweidlem26  45982  stoweidlem42  45998  wallispilem4  46024  wallispilem5  46025  wallispi  46026  wallispi2lem1  46027  wallispi2lem2  46028  wallispi2  46029  stirlinglem1  46030  stirlinglem3  46032  stirlinglem4  46033  stirlinglem5  46034  stirlinglem6  46035  stirlinglem7  46036  stirlinglem13  46042  stirlinglem14  46043  stirlinglem15  46044  dirkeritg  46058  dirkercncflem1  46059  dirkercncflem2  46060  fourierdlem26  46089  fourierdlem39  46102  fourierdlem56  46118  fourierdlem62  46124  fourierdlem72  46134  fourierdlem74  46136  fourierdlem75  46137  fourierdlem76  46138  fourierdlem80  46142  fourierdlem103  46165  fourierdlem104  46166  fouriersw  46187  elaa2lem  46189  etransclem15  46205  etransclem20  46210  etransclem21  46211  etransclem22  46212  etransclem23  46213  etransclem24  46214  etransclem25  46215  etransclem31  46221  etransclem32  46222  etransclem33  46223  etransclem34  46224  etransclem35  46225  etransclem47  46237  etransclem48  46238  hoiqssbllem2  46579  sigardiv  46817  sharhght  46821  cndivrenred  47256  fmtnoprmfac2lem1  47491  quad1  47545  requad01  47546  requad1  47547  fdivmptf  48391  affinecomb2  48553  eenglngeehlnmlem1  48587  eenglngeehlnmlem2  48588  itscnhlc0xyqsol  48615  itschlc0xyqsol1  48616  cotcl  48983