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

Theorem addcld 10251
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 10210 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3syl2anc 696 1 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  (class class class)co 6813  cc 10126   + caddc 10131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 10188
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  cnegex  10409  addcom  10414  addcomd  10430  muladd11r  10441  negeu  10463  addsubass  10483  subsub2  10501  subsub4  10506  pnpcan  10512  pnncan  10514  addsub4  10516  pnpncand  10644  divdir  10902  cju  11208  cnref1o  12020  xov1plusxeqvd  12511  expaddz  13098  binom3  13179  sqoddm1div8  13222  mulsubdivbinom2  13240  muldivbinom2  13241  spllen  13705  crre  14053  remullem  14067  imval2  14090  cjreim2  14100  sqreulem  14298  addcn2  14523  o1add  14543  fsumadd  14669  isumadd  14697  binomlem  14760  binomfallfaclem2  14970  bpoly4  14989  fsumcube  14990  efaddlem  15022  ef4p  15042  cosf  15054  tanval2  15062  tanval3  15063  resin4p  15067  recos4p  15068  efival  15081  sinadd  15093  cosadd  15094  tanadd  15096  pwp1fsum  15316  sadadd2lem2  15374  sadadd2lem  15383  pythagtriplem1  15723  pythagtriplem12  15733  pythagtriplem17  15738  pcbc  15806  mul4sqlem  15859  4sqlem14  15864  vdwlem6  15892  vdwlem9  15895  mulgdirlem  17773  blcvx  22802  tchcphlem1  23234  cphipval2  23240  4cphipval2  23241  csbren  23382  ovollb2lem  23456  mbfadd  23627  itgcnlem  23755  itgaddlem2  23789  dvmptre  23931  dvsincos  23943  taylthlem2  24327  ptolemy  24447  tanregt0  24484  eff1olem  24493  cosargd  24553  tanarg  24564  logf1o2  24595  efopn  24603  cxpsqrtlem  24647  cxpeq  24697  ang180lem1  24738  ang180lem2  24739  ang180lem3  24740  ang180lem4  24741  pythag  24746  ssscongptld  24751  chordthmlem  24758  chordthmlem2  24759  chordthmlem3  24760  chordthmlem4  24761  chordthmlem5  24762  heron  24764  quad2  24765  dcubic1lem  24769  dcubic2  24770  dcubic1  24771  dcubic  24772  mcubic  24773  cubic2  24774  cubic  24775  binom4  24776  dquartlem1  24777  dquartlem2  24778  dquart  24779  quart1cl  24780  quart1lem  24781  quart1  24782  quartlem1  24783  quartlem2  24784  quartlem3  24785  quartlem4  24786  quart  24787  asinlem3  24797  asinf  24798  asinneg  24812  efiasin  24814  asinsinlem  24817  asinsin  24818  asinbnd  24825  atanlogaddlem  24839  dmgmaddnn0  24952  dmgmdivn0  24953  lgamgulmlem2  24955  lgamgulmlem3  24956  lgamgulmlem4  24957  lgamgulmlem5  24958  lgamgulmlem6  24959  lgamgulm2  24961  lgambdd  24962  lgamucov  24963  lgamcvg2  24980  gamcvg  24981  gamcvg2lem  24984  ftalem7  25004  basellem3  25008  bposlem9  25216  lgsquad2lem1  25308  2lgslem3d1  25327  dchrvmasumiflem2  25390  mulogsumlem  25419  mulog2sumlem1  25422  mulog2sumlem2  25423  mulog2sumlem3  25424  selberglem1  25433  selberg2  25439  selberg3lem1  25445  selbergr  25456  selberg3r  25457  pntrlog2bndlem1  25465  pntrlog2bndlem2  25466  pntrlog2bndlem5  25469  pntrlog2bndlem6  25471  pntrlog2bnd  25472  brbtwn2  25984  colinearalglem1  25985  colinearalglem2  25986  axeuclidlem  26041  axcontlem2  26044  axcontlem7  26049  axcontlem8  26050  finsumvtxdg2ssteplem4  26654  wwlksext2clwwlk  27187  4ipval2  27872  dipcj  27878  golem1  29439  lt2addrd  29825  bhmafibid1  29953  bhmafibid2  29954  2sqmod  29957  archirngz  30052  archiabllem2c  30058  cnre2csqima  30266  ballotlemsima  30886  hgt750lemb  31043  iprodgam  31935  dnizphlfeqhlf  32772  dnibndlem9  32782  knoppndvlem16  32824  itg2addnclem3  33776  itgaddnclem2  33782  itgaddnc  33783  ftc1anclem6  33803  ftc1anclem8  33805  dvasin  33809  areacirclem1  33813  areacirclem4  33816  areacirc  33818  pellexlem2  37896  pellexlem6  37900  pell1234qrreccl  37920  pell1234qrmulcl  37921  pell14qrdich  37935  rmxyneg  37987  rmxyadd  37988  jm2.19lem4  38061  jm2.26lem3  38070  itgpowd  38302  int-rightdistd  38985  binomcxplemnn0  39050  binomcxplemrat  39051  binomcxplemfrat  39052  binomcxplemdvbinom  39054  binomcxplemnotnn0  39057  sub2times  39984  clim1fr1  40336  limcperiod  40363  addlimc  40383  coseq0  40578  fprodaddrecnncnvlem  40626  dvxpaek  40658  dvnxpaek  40660  dvnmul  40661  itgiccshift  40699  itgperiod  40700  stoweidlem1  40721  stoweidlem11  40731  stoweidlem13  40733  wallispilem4  40788  wallispilem5  40789  wallispi  40790  wallispi2lem1  40791  wallispi2lem2  40792  wallispi2  40793  stirlinglem1  40794  stirlinglem3  40796  stirlinglem4  40797  stirlinglem5  40798  stirlinglem6  40799  stirlinglem7  40800  stirlinglem10  40803  stirlinglem11  40804  stirlinglem12  40805  stirlinglem13  40806  stirlinglem15  40808  dirkerper  40816  dirkertrigeqlem1  40818  dirkertrigeqlem2  40819  dirkertrigeqlem3  40820  dirkeritg  40822  dirkercncflem2  40824  dirkercncflem4  40826  fourierdlem18  40845  fourierdlem26  40853  fourierdlem30  40857  fourierdlem48  40874  fourierdlem49  40875  fourierdlem79  40905  fourierdlem83  40909  fourierdlem92  40918  fourierdlem93  40919  fourierdlem103  40929  fourierdlem104  40930  fourierdlem111  40937  fourierdlem112  40938  smfmullem1  41504  sigaraf  41548  sigaras  41550  fmtnorec4  41971  fldivmod  42823  dignn0flhalflem1  42919  sinhpcosh  42994
  Copyright terms: Public domain W3C validator