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

Theorem addcld 10648
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 10607 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  (class class class)co 7145  cc 10523   + caddc 10528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 10585
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  cnegex  10809  addcom  10814  addcomd  10830  muladd11r  10841  negeu  10864  addsubass  10884  subsub2  10902  subsub4  10907  pnncan  10915  addsub4  10917  pnpncand  11049  addmulsub  11090  subaddmulsub  11091  mulsubaddmulsub  11092  divdir  11311  cju  11622  cnref1o  12372  xov1plusxeqvd  12872  expaddz  13461  binom3  13573  sqoddm1div8  13592  mulsubdivbinom2  13610  muldivbinom2  13611  spllen  14104  crre  14461  remullem  14475  imval2  14498  cjreim2  14508  sqreulem  14707  bhmafibid1cn  14811  bhmafibid2cn  14812  bhmafibid1  14813  bhmafibid2  14814  addcn2  14938  o1add  14958  fsumadd  15084  isumadd  15110  binomlem  15172  binomfallfaclem2  15382  bpoly4  15401  fsumcube  15402  efaddlem  15434  ef4p  15454  cosf  15466  tanval2  15474  tanval3  15475  resin4p  15479  recos4p  15480  efival  15493  sinadd  15505  cosadd  15506  tanadd  15508  pwp1fsum  15730  sadadd2lem2  15787  sadadd2lem  15796  pythagtriplem1  16141  pythagtriplem12  16151  pythagtriplem17  16156  pcbc  16224  mul4sqlem  16277  4sqlem14  16282  vdwlem6  16310  vdwlem9  16313  mulgdirlem  18196  blcvx  23333  tcphcphlem1  23765  cphipval2  23771  4cphipval2  23772  csbren  23929  ovollb2lem  24016  mbfadd  24189  itgcnlem  24317  itgaddlem2  24351  dvmptre  24493  dvsincos  24505  taylthlem2  24889  ptolemy  25009  tanregt0  25050  eff1olem  25059  cosargd  25118  tanarg  25129  logf1o2  25160  efopn  25168  cxpsqrtlem  25212  cxpeq  25265  ang180lem1  25314  ang180lem2  25315  ang180lem3  25316  ang180lem4  25317  pythag  25322  ssscongptld  25327  chordthmlem  25337  chordthmlem2  25338  chordthmlem3  25339  chordthmlem4  25340  chordthmlem5  25341  heron  25343  quad2  25344  dcubic1lem  25348  dcubic2  25349  dcubic1  25350  dcubic  25351  mcubic  25352  cubic2  25353  cubic  25354  binom4  25355  dquartlem1  25356  dquartlem2  25357  dquart  25358  quart1cl  25359  quart1lem  25360  quart1  25361  quartlem1  25362  quartlem2  25363  quartlem3  25364  quartlem4  25365  quart  25366  asinlem3  25376  asinf  25377  asinneg  25391  efiasin  25393  asinsinlem  25396  asinsin  25397  asinbnd  25404  atanlogaddlem  25418  dmgmaddnn0  25531  dmgmdivn0  25532  lgamgulmlem2  25534  lgamgulmlem3  25535  lgamgulmlem4  25536  lgamgulmlem5  25537  lgamgulmlem6  25538  lgamgulm2  25540  lgambdd  25541  lgamucov  25542  lgamcvg2  25559  gamcvg  25560  gamcvg2lem  25563  ftalem7  25583  basellem3  25587  bposlem9  25795  lgsquad2lem1  25887  2lgslem3d1  25906  2sqmod  25939  dchrvmasumiflem2  26005  mulogsumlem  26034  mulog2sumlem1  26037  mulog2sumlem2  26038  mulog2sumlem3  26039  selberglem1  26048  selberg2  26054  selberg3lem1  26060  selbergr  26071  selberg3r  26072  pntrlog2bndlem1  26080  pntrlog2bndlem2  26081  pntrlog2bndlem5  26084  pntrlog2bndlem6  26086  pntrlog2bnd  26087  brbtwn2  26618  colinearalglem1  26619  colinearalglem2  26620  axeuclidlem  26675  axcontlem2  26678  axcontlem7  26683  axcontlem8  26684  finsumvtxdg2ssteplem4  27257  wwlksext2clwwlk  27763  4ipval2  28412  dipcj  28418  golem1  29975  lt2addrd  30401  cycpmco2lem3  30697  cycpmco2lem4  30698  cycpmco2lem5  30699  cycpmco2lem6  30700  cycpmco2  30702  archirngz  30745  archiabllem2c  30751  ccfldextdgrr  30956  cnre2csqima  31053  ballotlemsima  31672  hgt750lemb  31826  iprodgam  32871  dnizphlfeqhlf  33712  dnibndlem9  33722  knoppndvlem16  33763  itg2addnclem3  34826  itgaddnclem2  34832  itgaddnc  34833  ftc1anclem6  34853  ftc1anclem8  34855  dvasin  34859  areacirclem1  34863  areacirclem4  34866  areacirc  34868  dffltz  39149  cu3addd  39155  3cubeslem2  39160  3cubeslem3l  39161  3cubeslem3r  39162  3cubeslem4  39164  pellexlem2  39305  pellexlem6  39309  pell1234qrreccl  39329  pell1234qrmulcl  39330  pell14qrdich  39344  rmxyneg  39395  rmxyadd  39396  jm2.19lem4  39467  jm2.26lem3  39476  itgpowd  39699  int-rightdistd  40411  binomcxplemnn0  40558  binomcxplemrat  40559  binomcxplemfrat  40560  binomcxplemdvbinom  40562  binomcxplemnotnn0  40565  sub2times  41416  clim1fr1  41758  limcperiod  41785  addlimc  41805  coseq0  42021  fprodaddrecnncnvlem  42069  dvxpaek  42101  dvnxpaek  42103  dvnmul  42104  itgiccshift  42141  itgperiod  42142  stoweidlem1  42163  stoweidlem11  42173  stoweidlem13  42175  wallispilem4  42230  wallispilem5  42231  wallispi  42232  wallispi2lem1  42233  wallispi2lem2  42234  wallispi2  42235  stirlinglem1  42236  stirlinglem3  42238  stirlinglem4  42239  stirlinglem5  42240  stirlinglem6  42241  stirlinglem7  42242  stirlinglem10  42245  stirlinglem11  42246  stirlinglem12  42247  stirlinglem13  42248  stirlinglem15  42250  dirkerper  42258  dirkertrigeqlem1  42260  dirkertrigeqlem2  42261  dirkertrigeqlem3  42262  dirkeritg  42264  dirkercncflem2  42266  dirkercncflem4  42268  fourierdlem18  42287  fourierdlem26  42295  fourierdlem30  42299  fourierdlem48  42316  fourierdlem49  42317  fourierdlem79  42347  fourierdlem83  42351  fourierdlem92  42360  fourierdlem93  42361  fourierdlem103  42371  fourierdlem104  42372  fourierdlem111  42379  fourierdlem112  42380  smfmullem1  42943  sigaraf  42987  sigaras  42989  readdcnnred  43380  fmtnorec4  43588  quad1  43662  requad01  43663  requad2  43665  fldivmod  44506  dignn0flhalflem1  44603  affinecomb2  44618  eenglngeehlnmlem1  44652  itschlc0yqe  44675  itsclc0yqsollem1  44677  itsclc0yqsol  44679  itscnhlc0xyqsol  44680  itsclc0xyqsolr  44684  2itscplem3  44695  itscnhlinecirc02plem1  44697  inlinecirc02plem  44701  sinhpcosh  44767
  Copyright terms: Public domain W3C validator