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

Theorem addcld 10347
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 10306 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3syl2anc 575 1 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  (class class class)co 6877  cc 10222   + caddc 10227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 10284
This theorem depends on definitions:  df-bi 198  df-an 385
This theorem is referenced by:  cnegex  10505  addcom  10510  addcomd  10526  muladd11r  10537  negeu  10559  addsubass  10579  subsub2  10597  subsub4  10602  pnpcan  10608  pnncan  10610  addsub4  10612  pnpncand  10740  divdir  10998  cju  11304  cnref1o  12044  xov1plusxeqvd  12544  expaddz  13130  binom3  13211  sqoddm1div8  13254  mulsubdivbinom2  13272  muldivbinom2  13273  spllen  13732  crre  14080  remullem  14094  imval2  14117  cjreim2  14127  sqreulem  14325  addcn2  14550  o1add  14570  fsumadd  14696  isumadd  14724  binomlem  14786  binomfallfaclem2  14994  bpoly4  15013  fsumcube  15014  efaddlem  15046  ef4p  15066  cosf  15078  tanval2  15086  tanval3  15087  resin4p  15091  recos4p  15092  efival  15105  sinadd  15117  cosadd  15118  tanadd  15120  pwp1fsum  15337  sadadd2lem2  15394  sadadd2lem  15403  pythagtriplem1  15741  pythagtriplem12  15751  pythagtriplem17  15756  pcbc  15824  mul4sqlem  15877  4sqlem14  15882  vdwlem6  15910  vdwlem9  15913  mulgdirlem  17778  blcvx  22818  tchcphlem1  23250  cphipval2  23256  4cphipval2  23257  csbren  23400  ovollb2lem  23475  mbfadd  23648  itgcnlem  23776  itgaddlem2  23810  dvmptre  23952  dvsincos  23964  taylthlem2  24348  ptolemy  24469  tanregt0  24506  eff1olem  24515  cosargd  24574  tanarg  24585  logf1o2  24616  efopn  24624  cxpsqrtlem  24668  cxpeq  24718  ang180lem1  24759  ang180lem2  24760  ang180lem3  24761  ang180lem4  24762  pythag  24767  ssscongptld  24772  chordthmlem  24779  chordthmlem2  24780  chordthmlem3  24781  chordthmlem4  24782  chordthmlem5  24783  heron  24785  quad2  24786  dcubic1lem  24790  dcubic2  24791  dcubic1  24792  dcubic  24793  mcubic  24794  cubic2  24795  cubic  24796  binom4  24797  dquartlem1  24798  dquartlem2  24799  dquart  24800  quart1cl  24801  quart1lem  24802  quart1  24803  quartlem1  24804  quartlem2  24805  quartlem3  24806  quartlem4  24807  quart  24808  asinlem3  24818  asinf  24819  asinneg  24833  efiasin  24835  asinsinlem  24838  asinsin  24839  asinbnd  24846  atanlogaddlem  24860  dmgmaddnn0  24973  dmgmdivn0  24974  lgamgulmlem2  24976  lgamgulmlem3  24977  lgamgulmlem4  24978  lgamgulmlem5  24979  lgamgulmlem6  24980  lgamgulm2  24982  lgambdd  24983  lgamucov  24984  lgamcvg2  25001  gamcvg  25002  gamcvg2lem  25005  ftalem7  25025  basellem3  25029  bposlem9  25237  lgsquad2lem1  25329  2lgslem3d1  25348  dchrvmasumiflem2  25411  mulogsumlem  25440  mulog2sumlem1  25443  mulog2sumlem2  25444  mulog2sumlem3  25445  selberglem1  25454  selberg2  25460  selberg3lem1  25466  selbergr  25477  selberg3r  25478  pntrlog2bndlem1  25486  pntrlog2bndlem2  25487  pntrlog2bndlem5  25490  pntrlog2bndlem6  25492  pntrlog2bnd  25493  brbtwn2  26005  colinearalglem1  26006  colinearalglem2  26007  axeuclidlem  26062  axcontlem2  26065  axcontlem7  26070  axcontlem8  26071  finsumvtxdg2ssteplem4  26678  wwlksext2clwwlk  27213  4ipval2  27897  dipcj  27903  golem1  29464  lt2addrd  29849  bhmafibid1  29975  bhmafibid2  29976  2sqmod  29979  archirngz  30074  archiabllem2c  30080  cnre2csqima  30288  ballotlemsima  30908  hgt750lemb  31065  iprodgam  31955  dnizphlfeqhlf  32788  dnibndlem9  32798  knoppndvlem16  32840  itg2addnclem3  33777  itgaddnclem2  33783  itgaddnc  33784  ftc1anclem6  33804  ftc1anclem8  33806  dvasin  33810  areacirclem1  33814  areacirclem4  33817  areacirc  33819  pellexlem2  37897  pellexlem6  37901  pell1234qrreccl  37921  pell1234qrmulcl  37922  pell14qrdich  37936  rmxyneg  37987  rmxyadd  37988  jm2.19lem4  38061  jm2.26lem3  38070  itgpowd  38301  int-rightdistd  38984  binomcxplemnn0  39049  binomcxplemrat  39050  binomcxplemfrat  39051  binomcxplemdvbinom  39053  binomcxplemnotnn0  39056  sub2times  39969  clim1fr1  40314  limcperiod  40341  addlimc  40361  coseq0  40556  fprodaddrecnncnvlem  40604  dvxpaek  40636  dvnxpaek  40638  dvnmul  40639  itgiccshift  40676  itgperiod  40677  stoweidlem1  40698  stoweidlem11  40708  stoweidlem13  40710  wallispilem4  40765  wallispilem5  40766  wallispi  40767  wallispi2lem1  40768  wallispi2lem2  40769  wallispi2  40770  stirlinglem1  40771  stirlinglem3  40773  stirlinglem4  40774  stirlinglem5  40775  stirlinglem6  40776  stirlinglem7  40777  stirlinglem10  40780  stirlinglem11  40781  stirlinglem12  40782  stirlinglem13  40783  stirlinglem15  40785  dirkerper  40793  dirkertrigeqlem1  40795  dirkertrigeqlem2  40796  dirkertrigeqlem3  40797  dirkeritg  40799  dirkercncflem2  40801  dirkercncflem4  40803  fourierdlem18  40822  fourierdlem26  40830  fourierdlem30  40834  fourierdlem48  40851  fourierdlem49  40852  fourierdlem79  40882  fourierdlem83  40886  fourierdlem92  40895  fourierdlem93  40896  fourierdlem103  40906  fourierdlem104  40907  fourierdlem111  40914  fourierdlem112  40915  smfmullem1  41481  sigaraf  41525  sigaras  41527  fmtnorec4  42037  fldivmod  42882  dignn0flhalflem1  42978  sinhpcosh  43053
  Copyright terms: Public domain W3C validator