MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcld Structured version   Visualization version   GIF version

Theorem addcld 9915
Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
addcld.2 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
addcld (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Proof of Theorem addcld
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addcl 9874 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3syl2anc 690 1 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  (class class class)co 6526  cc 9790   + caddc 9795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 9852
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  cnegex  10068  addcom  10073  addcomd  10089  muladd11r  10100  negeu  10122  addsubass  10142  subsub2  10160  subsub4  10165  pnpcan  10171  pnncan  10173  addsub4  10175  pnpncand  10303  divdir  10561  cju  10865  cnref1o  11661  xov1plusxeqvd  12147  expaddz  12723  binom3  12804  sqoddm1div8  12847  mulsubdivbinom2  12865  muldivbinom2  12866  spllen  13304  crre  13650  remullem  13664  imval2  13687  cjreim2  13697  sqreulem  13895  addcn2  14120  o1add  14140  fsumadd  14265  isumadd  14288  binomlem  14348  binomfallfaclem2  14558  bpoly4  14577  fsumcube  14578  efaddlem  14610  ef4p  14630  cosf  14642  tanval2  14650  tanval3  14651  resin4p  14655  recos4p  14656  efival  14669  sinadd  14681  cosadd  14682  tanadd  14684  pwp1fsum  14900  sadadd2lem2  14958  sadadd2lem  14967  pythagtriplem1  15307  pythagtriplem12  15317  pythagtriplem17  15322  pcbc  15390  mul4sqlem  15443  4sqlem14  15448  vdwlem6  15476  vdwlem9  15479  mulgdirlem  17343  blcvx  22356  tchcphlem1  22786  cphipval2  22792  4cphipval2  22793  csbren  22934  ovollb2lem  23007  mbfadd  23178  itgcnlem  23306  itgaddlem2  23340  dvmptre  23482  dvsincos  23492  taylthlem2  23876  ptolemy  23996  tanregt0  24033  eff1olem  24042  cosargd  24102  tanarg  24113  logf1o2  24140  efopn  24148  cxpsqrtlem  24192  cxpeq  24242  ang180lem1  24283  ang180lem2  24284  ang180lem3  24285  ang180lem4  24286  pythag  24291  ssscongptld  24296  chordthmlem  24303  chordthmlem2  24304  chordthmlem3  24305  chordthmlem4  24306  chordthmlem5  24307  heron  24309  quad2  24310  dcubic1lem  24314  dcubic2  24315  dcubic1  24316  dcubic  24317  mcubic  24318  cubic2  24319  cubic  24320  binom4  24321  dquartlem1  24322  dquartlem2  24323  dquart  24324  quart1cl  24325  quart1lem  24326  quart1  24327  quartlem1  24328  quartlem2  24329  quartlem3  24330  quartlem4  24331  quart  24332  asinlem3  24342  asinf  24343  asinneg  24357  efiasin  24359  asinsinlem  24362  asinsin  24363  asinbnd  24370  atanlogaddlem  24384  dmgmaddnn0  24497  dmgmdivn0  24498  lgamgulmlem2  24500  lgamgulmlem3  24501  lgamgulmlem4  24502  lgamgulmlem5  24503  lgamgulmlem6  24504  lgamgulm2  24506  lgambdd  24507  lgamucov  24508  lgamcvg2  24525  gamcvg  24526  gamcvg2lem  24529  ftalem7  24549  basellem3  24553  bposlem9  24761  lgsquad2lem1  24853  2lgslem3d1  24872  dchrvmasumiflem2  24935  mulogsumlem  24964  mulog2sumlem1  24967  mulog2sumlem2  24968  mulog2sumlem3  24969  selberglem1  24978  selberg2  24984  selberg3lem1  24990  selbergr  25001  selberg3r  25002  pntrlog2bndlem1  25010  pntrlog2bndlem2  25011  pntrlog2bndlem5  25014  pntrlog2bndlem6  25016  pntrlog2bnd  25017  brbtwn2  25530  colinearalglem1  25531  colinearalglem2  25532  axeuclidlem  25587  axcontlem2  25590  axcontlem7  25595  axcontlem8  25596  4ipval2  26740  dipcj  26746  golem1  28307  lt2addrd  28696  bhmafibid1  28768  bhmafibid2  28769  2sqmod  28772  archirngz  28867  archiabllem2c  28873  cnre2csqima  29078  ballotlemsima  29697  iprodgam  30674  dnizphlfeqhlf  31429  dnibndlem9  31439  knoppndvlem16  31481  itg2addnclem3  32416  itgaddnclem2  32422  itgaddnc  32423  ftc1anclem6  32443  ftc1anclem8  32445  dvasin  32449  areacirclem1  32453  areacirclem4  32456  areacirc  32458  pellexlem2  36195  pellexlem6  36199  pell1234qrreccl  36219  pell1234qrmulcl  36220  pell14qrdich  36234  rmxyneg  36286  rmxyadd  36287  jm2.19lem4  36360  jm2.26lem3  36369  itgpowd  36602  int-rightdistd  37288  binomcxplemnn0  37353  binomcxplemrat  37354  binomcxplemfrat  37355  binomcxplemdvbinom  37357  binomcxplemnotnn0  37360  sub2times  38209  clim1fr1  38451  limcperiod  38478  addlimc  38498  coseq0  38530  fprodaddrecnncnvlem  38579  dvxpaek  38613  dvnxpaek  38615  dvnmul  38616  itgiccshift  38655  itgperiod  38656  stoweidlem1  38677  stoweidlem11  38687  stoweidlem13  38689  wallispilem4  38744  wallispilem5  38745  wallispi  38746  wallispi2lem1  38747  wallispi2lem2  38748  wallispi2  38749  stirlinglem1  38750  stirlinglem3  38752  stirlinglem4  38753  stirlinglem5  38754  stirlinglem6  38755  stirlinglem7  38756  stirlinglem10  38759  stirlinglem11  38760  stirlinglem12  38761  stirlinglem13  38762  stirlinglem15  38764  dirkerper  38772  dirkertrigeqlem1  38774  dirkertrigeqlem2  38775  dirkertrigeqlem3  38776  dirkeritg  38778  dirkercncflem2  38780  dirkercncflem4  38782  fourierdlem18  38801  fourierdlem26  38809  fourierdlem30  38813  fourierdlem48  38830  fourierdlem49  38831  fourierdlem79  38861  fourierdlem83  38865  fourierdlem92  38874  fourierdlem93  38875  fourierdlem103  38885  fourierdlem104  38886  fourierdlem111  38893  fourierdlem112  38894  smfmullem1  39459  sigaraf  39474  sigaras  39476  fmtnorec4  39783  fldivmod  42088  dignn0flhalflem1  42188  sinhpcosh  42222
  Copyright terms: Public domain W3C validator