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

Theorem addcld 11181
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 11140 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3syl2anc 585 1 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  (class class class)co 7362  cc 11056   + caddc 11061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 11118
This theorem depends on definitions:  df-bi 206  df-an 398
This theorem is referenced by:  cnegex  11343  addcom  11348  addcomd  11364  muladd11r  11375  negeu  11398  addsubass  11418  subsub2  11436  subsub4  11441  pnncan  11449  addsub4  11451  pnpncand  11583  addmulsub  11624  subaddmulsub  11625  mulsubaddmulsub  11626  divdir  11845  cju  12156  cnref1o  12917  xov1plusxeqvd  13422  expaddz  14019  binom3  14134  sqoddm1div8  14153  mulsubdivbinom2  14169  muldivbinom2  14170  spllen  14649  crre  15006  remullem  15020  imval2  15043  cjreim2  15053  sqreulem  15251  bhmafibid1cn  15355  bhmafibid2cn  15356  bhmafibid1  15357  bhmafibid2  15358  addcn2  15483  o1add  15503  rlimadd  15532  fsumadd  15632  isumadd  15659  binomlem  15721  binomfallfaclem2  15930  bpoly4  15949  fsumcube  15950  efaddlem  15982  ef4p  16002  cosf  16014  tanval2  16022  tanval3  16023  resin4p  16027  recos4p  16028  efival  16041  sinadd  16053  cosadd  16054  tanadd  16056  pwp1fsum  16280  sadadd2lem2  16337  sadadd2lem  16346  pythagtriplem1  16695  pythagtriplem12  16705  pythagtriplem17  16710  pcbc  16779  mul4sqlem  16832  4sqlem14  16837  vdwlem6  16865  vdwlem9  16868  mulgdirlem  18914  blcvx  24177  cphpyth  24596  tcphcphlem1  24615  cphipval2  24621  4cphipval2  24622  csbren  24779  ovollb2lem  24868  mbfadd  25041  itgcnlem  25170  itgaddlem2  25204  dvmptre  25349  dvsincos  25361  itgpowd  25430  taylthlem2  25749  ptolemy  25869  tanregt0  25911  eff1olem  25920  cosargd  25979  tanarg  25990  logf1o2  26021  efopn  26029  cxpsqrtlem  26073  cxpeq  26126  ang180lem1  26175  ang180lem2  26176  ang180lem3  26177  ang180lem4  26178  pythag  26183  ssscongptld  26188  chordthmlem  26198  chordthmlem2  26199  chordthmlem3  26200  chordthmlem4  26201  chordthmlem5  26202  heron  26204  quad2  26205  dcubic1lem  26209  dcubic2  26210  dcubic1  26211  dcubic  26212  mcubic  26213  cubic2  26214  cubic  26215  binom4  26216  dquartlem1  26217  dquartlem2  26218  dquart  26219  quart1cl  26220  quart1lem  26221  quart1  26222  quartlem1  26223  quartlem2  26224  quartlem3  26225  quartlem4  26226  quart  26227  asinlem3  26237  asinf  26238  asinneg  26252  efiasin  26254  asinsinlem  26257  asinsin  26258  asinbnd  26265  atanlogaddlem  26279  dmgmaddnn0  26392  dmgmdivn0  26393  lgamgulmlem2  26395  lgamgulmlem3  26396  lgamgulmlem4  26397  lgamgulmlem5  26398  lgamgulmlem6  26399  lgamgulm2  26401  lgambdd  26402  lgamucov  26403  lgamcvg2  26420  gamcvg  26421  gamcvg2lem  26424  ftalem7  26444  basellem3  26448  bposlem9  26656  lgsquad2lem1  26748  2lgslem3d1  26767  2sqmod  26800  dchrvmasumiflem2  26866  mulogsumlem  26895  mulog2sumlem1  26898  mulog2sumlem2  26899  mulog2sumlem3  26900  selberglem1  26909  selberg2  26915  selberg3lem1  26921  selbergr  26932  selberg3r  26933  pntrlog2bndlem1  26941  pntrlog2bndlem2  26942  pntrlog2bndlem5  26945  pntrlog2bndlem6  26947  pntrlog2bnd  26948  brbtwn2  27896  colinearalglem1  27897  colinearalglem2  27898  axeuclidlem  27953  axcontlem2  27956  axcontlem7  27961  axcontlem8  27962  finsumvtxdg2ssteplem4  28538  wwlksext2clwwlk  29043  4ipval2  29692  dipcj  29698  golem1  31255  lt2addrd  31698  cycpmco2lem3  32019  cycpmco2lem4  32020  cycpmco2lem5  32021  cycpmco2lem6  32022  cycpmco2  32024  archirngz  32067  archiabllem2c  32073  ccfldextdgrr  32396  cnre2csqima  32532  ballotlemsima  33155  hgt750lemb  33309  iprodgam  34354  dnizphlfeqhlf  34968  dnibndlem9  34978  knoppndvlem16  35019  itg2addnclem3  36160  itgaddnclem2  36166  itgaddnc  36167  ftc1anclem6  36185  ftc1anclem8  36187  dvasin  36191  areacirclem1  36195  areacirclem4  36198  areacirc  36200  lcmineqlem6  40520  lcmineqlem11  40525  lcmineqlem18  40532  aks4d1p1p2  40556  aks4d1p1p6  40559  aks4d1p1p7  40560  aks4d1p1p5  40561  2np3bcnp1  40581  2ap1caineq  40582  sticksstones12a  40594  metakunt29  40634  mvrrsubd  40818  lsubrotld  40821  sn-negex12  40914  sn-addid1  40918  sn-subeu  40924  sn-0tie0  40937  zaddcomlem  40949  zaddcom  40950  cnreeu  40966  dffltz  41001  cu3addd  41032  3cubeslem2  41037  3cubeslem3l  41038  3cubeslem3r  41039  3cubeslem4  41041  pellexlem2  41182  pellexlem6  41186  pell1234qrreccl  41206  pell1234qrmulcl  41207  pell14qrdich  41221  rmxyneg  41273  rmxyadd  41274  jm2.19lem4  41345  jm2.26lem3  41354  sqrtcval  41987  int-rightdistd  42527  binomcxplemnn0  42703  binomcxplemrat  42704  binomcxplemfrat  42705  binomcxplemdvbinom  42707  binomcxplemnotnn0  42710  sub2times  43580  clim1fr1  43916  limcperiod  43943  addlimc  43963  coseq0  44179  fprodaddrecnncnvlem  44224  dvxpaek  44255  dvnxpaek  44257  dvnmul  44258  itgiccshift  44295  itgperiod  44296  stoweidlem1  44316  stoweidlem11  44326  stoweidlem13  44328  wallispilem4  44383  wallispilem5  44384  wallispi  44385  wallispi2lem1  44386  wallispi2lem2  44387  wallispi2  44388  stirlinglem1  44389  stirlinglem3  44391  stirlinglem4  44392  stirlinglem5  44393  stirlinglem6  44394  stirlinglem7  44395  stirlinglem10  44398  stirlinglem11  44399  stirlinglem12  44400  stirlinglem13  44401  stirlinglem15  44403  dirkerper  44411  dirkertrigeqlem1  44413  dirkertrigeqlem2  44414  dirkertrigeqlem3  44415  dirkeritg  44417  dirkercncflem2  44419  dirkercncflem4  44421  fourierdlem18  44440  fourierdlem26  44448  fourierdlem30  44452  fourierdlem48  44469  fourierdlem49  44470  fourierdlem79  44500  fourierdlem83  44504  fourierdlem92  44513  fourierdlem93  44514  fourierdlem103  44524  fourierdlem104  44525  fourierdlem111  44532  fourierdlem112  44533  smfmullem1  45106  sigaraf  45168  sigaras  45170  readdcnnred  45609  fmtnorec4  45815  quad1  45886  requad01  45887  requad2  45889  fldivmod  46678  dignn0flhalflem1  46775  affinecomb2  46863  eenglngeehlnmlem1  46897  itschlc0yqe  46920  itsclc0yqsollem1  46922  itsclc0yqsol  46924  itscnhlc0xyqsol  46925  itsclc0xyqsolr  46929  2itscplem3  46940  itscnhlinecirc02plem1  46942  inlinecirc02plem  46946  sinhpcosh  47259
  Copyright terms: Public domain W3C validator