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

Theorem addcld 10097
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 10056 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3syl2anc 694 1 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  (class class class)co 6690  cc 9972   + caddc 9977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 10034
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  cnegex  10255  addcom  10260  addcomd  10276  muladd11r  10287  negeu  10309  addsubass  10329  subsub2  10347  subsub4  10352  pnpcan  10358  pnncan  10360  addsub4  10362  pnpncand  10490  divdir  10748  cju  11054  cnref1o  11865  xov1plusxeqvd  12356  expaddz  12944  binom3  13025  sqoddm1div8  13068  mulsubdivbinom2  13086  muldivbinom2  13087  spllen  13551  crre  13898  remullem  13912  imval2  13935  cjreim2  13945  sqreulem  14143  addcn2  14368  o1add  14388  fsumadd  14514  isumadd  14542  binomlem  14605  binomfallfaclem2  14815  bpoly4  14834  fsumcube  14835  efaddlem  14867  ef4p  14887  cosf  14899  tanval2  14907  tanval3  14908  resin4p  14912  recos4p  14913  efival  14926  sinadd  14938  cosadd  14939  tanadd  14941  pwp1fsum  15161  sadadd2lem2  15219  sadadd2lem  15228  pythagtriplem1  15568  pythagtriplem12  15578  pythagtriplem17  15583  pcbc  15651  mul4sqlem  15704  4sqlem14  15709  vdwlem6  15737  vdwlem9  15740  mulgdirlem  17619  blcvx  22648  tchcphlem1  23080  cphipval2  23086  4cphipval2  23087  csbren  23228  ovollb2lem  23302  mbfadd  23473  itgcnlem  23601  itgaddlem2  23635  dvmptre  23777  dvsincos  23789  taylthlem2  24173  ptolemy  24293  tanregt0  24330  eff1olem  24339  cosargd  24399  tanarg  24410  logf1o2  24441  efopn  24449  cxpsqrtlem  24493  cxpeq  24543  ang180lem1  24584  ang180lem2  24585  ang180lem3  24586  ang180lem4  24587  pythag  24592  ssscongptld  24597  chordthmlem  24604  chordthmlem2  24605  chordthmlem3  24606  chordthmlem4  24607  chordthmlem5  24608  heron  24610  quad2  24611  dcubic1lem  24615  dcubic2  24616  dcubic1  24617  dcubic  24618  mcubic  24619  cubic2  24620  cubic  24621  binom4  24622  dquartlem1  24623  dquartlem2  24624  dquart  24625  quart1cl  24626  quart1lem  24627  quart1  24628  quartlem1  24629  quartlem2  24630  quartlem3  24631  quartlem4  24632  quart  24633  asinlem3  24643  asinf  24644  asinneg  24658  efiasin  24660  asinsinlem  24663  asinsin  24664  asinbnd  24671  atanlogaddlem  24685  dmgmaddnn0  24798  dmgmdivn0  24799  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamgulmlem4  24803  lgamgulmlem5  24804  lgamgulmlem6  24805  lgamgulm2  24807  lgambdd  24808  lgamucov  24809  lgamcvg2  24826  gamcvg  24827  gamcvg2lem  24830  ftalem7  24850  basellem3  24854  bposlem9  25062  lgsquad2lem1  25154  2lgslem3d1  25173  dchrvmasumiflem2  25236  mulogsumlem  25265  mulog2sumlem1  25268  mulog2sumlem2  25269  mulog2sumlem3  25270  selberglem1  25279  selberg2  25285  selberg3lem1  25291  selbergr  25302  selberg3r  25303  pntrlog2bndlem1  25311  pntrlog2bndlem2  25312  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntrlog2bnd  25318  brbtwn2  25830  colinearalglem1  25831  colinearalglem2  25832  axeuclidlem  25887  axcontlem2  25890  axcontlem7  25895  axcontlem8  25896  finsumvtxdg2ssteplem4  26500  wwlksext2clwwlk  27021  4ipval2  27691  dipcj  27697  golem1  29258  lt2addrd  29644  bhmafibid1  29772  bhmafibid2  29773  2sqmod  29776  archirngz  29871  archiabllem2c  29877  cnre2csqima  30085  ballotlemsima  30705  hgt750lemb  30862  iprodgam  31754  dnizphlfeqhlf  32591  dnibndlem9  32601  knoppndvlem16  32643  itg2addnclem3  33593  itgaddnclem2  33599  itgaddnc  33600  ftc1anclem6  33620  ftc1anclem8  33622  dvasin  33626  areacirclem1  33630  areacirclem4  33633  areacirc  33635  pellexlem2  37711  pellexlem6  37715  pell1234qrreccl  37735  pell1234qrmulcl  37736  pell14qrdich  37750  rmxyneg  37802  rmxyadd  37803  jm2.19lem4  37876  jm2.26lem3  37885  itgpowd  38117  int-rightdistd  38800  binomcxplemnn0  38865  binomcxplemrat  38866  binomcxplemfrat  38867  binomcxplemdvbinom  38869  binomcxplemnotnn0  38872  sub2times  39799  clim1fr1  40151  limcperiod  40178  addlimc  40198  coseq0  40393  fprodaddrecnncnvlem  40441  dvxpaek  40473  dvnxpaek  40475  dvnmul  40476  itgiccshift  40514  itgperiod  40515  stoweidlem1  40536  stoweidlem11  40546  stoweidlem13  40548  wallispilem4  40603  wallispilem5  40604  wallispi  40605  wallispi2lem1  40606  wallispi2lem2  40607  wallispi2  40608  stirlinglem1  40609  stirlinglem3  40611  stirlinglem4  40612  stirlinglem5  40613  stirlinglem6  40614  stirlinglem7  40615  stirlinglem10  40618  stirlinglem11  40619  stirlinglem12  40620  stirlinglem13  40621  stirlinglem15  40623  dirkerper  40631  dirkertrigeqlem1  40633  dirkertrigeqlem2  40634  dirkertrigeqlem3  40635  dirkeritg  40637  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem18  40660  fourierdlem26  40668  fourierdlem30  40672  fourierdlem48  40689  fourierdlem49  40690  fourierdlem79  40720  fourierdlem83  40724  fourierdlem92  40733  fourierdlem93  40734  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  smfmullem1  41319  sigaraf  41363  sigaras  41365  fmtnorec4  41786  fldivmod  42638  dignn0flhalflem1  42734  sinhpcosh  42809
  Copyright terms: Public domain W3C validator