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

Theorem addcld 10649
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 10608 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  (class class class)co 7145  cc 10524   + caddc 10529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 10586
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  cnegex  10810  addcom  10815  addcomd  10831  muladd11r  10842  negeu  10865  addsubass  10885  subsub2  10903  subsub4  10908  pnncan  10916  addsub4  10918  pnpncand  11050  addmulsub  11091  subaddmulsub  11092  mulsubaddmulsub  11093  divdir  11312  cju  11623  cnref1o  12374  xov1plusxeqvd  12874  expaddz  13463  binom3  13575  sqoddm1div8  13594  mulsubdivbinom2  13612  muldivbinom2  13613  spllen  14106  crre  14463  remullem  14477  imval2  14500  cjreim2  14510  sqreulem  14709  bhmafibid1cn  14813  bhmafibid2cn  14814  bhmafibid1  14815  bhmafibid2  14816  addcn2  14940  o1add  14960  fsumadd  15086  isumadd  15112  binomlem  15174  binomfallfaclem2  15384  bpoly4  15403  fsumcube  15404  efaddlem  15436  ef4p  15456  cosf  15468  tanval2  15476  tanval3  15477  resin4p  15481  recos4p  15482  efival  15495  sinadd  15507  cosadd  15508  tanadd  15510  pwp1fsum  15732  sadadd2lem2  15789  sadadd2lem  15798  pythagtriplem1  16143  pythagtriplem12  16153  pythagtriplem17  16158  pcbc  16226  mul4sqlem  16279  4sqlem14  16284  vdwlem6  16312  vdwlem9  16315  mulgdirlem  18198  blcvx  23335  tcphcphlem1  23767  cphipval2  23773  4cphipval2  23774  csbren  23931  ovollb2lem  24018  mbfadd  24191  itgcnlem  24319  itgaddlem2  24353  dvmptre  24495  dvsincos  24507  taylthlem2  24891  ptolemy  25011  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  25532  dmgmdivn0  25533  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamgulmlem4  25537  lgamgulmlem5  25538  lgamgulmlem6  25539  lgamgulm2  25541  lgambdd  25542  lgamucov  25543  lgamcvg2  25560  gamcvg  25561  gamcvg2lem  25564  ftalem7  25584  basellem3  25588  bposlem9  25796  lgsquad2lem1  25888  2lgslem3d1  25907  2sqmod  25940  dchrvmasumiflem2  26006  mulogsumlem  26035  mulog2sumlem1  26038  mulog2sumlem2  26039  mulog2sumlem3  26040  selberglem1  26049  selberg2  26055  selberg3lem1  26061  selbergr  26072  selberg3r  26073  pntrlog2bndlem1  26081  pntrlog2bndlem2  26082  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntrlog2bnd  26088  brbtwn2  26619  colinearalglem1  26620  colinearalglem2  26621  axeuclidlem  26676  axcontlem2  26679  axcontlem7  26684  axcontlem8  26685  finsumvtxdg2ssteplem4  27258  wwlksext2clwwlk  27764  4ipval2  28413  dipcj  28419  golem1  29976  lt2addrd  30402  cycpmco2lem3  30698  cycpmco2lem4  30699  cycpmco2lem5  30700  cycpmco2lem6  30701  cycpmco2  30703  archirngz  30746  archiabllem2c  30752  ccfldextdgrr  30957  cnre2csqima  31054  ballotlemsima  31673  hgt750lemb  31827  iprodgam  32872  dnizphlfeqhlf  33713  dnibndlem9  33723  knoppndvlem16  33764  itg2addnclem3  34827  itgaddnclem2  34833  itgaddnc  34834  ftc1anclem6  34854  ftc1anclem8  34856  dvasin  34860  areacirclem1  34864  areacirclem4  34867  areacirc  34869  dffltz  39151  cu3addd  39157  3cubeslem2  39162  3cubeslem3l  39163  3cubeslem3r  39164  3cubeslem4  39166  pellexlem2  39307  pellexlem6  39311  pell1234qrreccl  39331  pell1234qrmulcl  39332  pell14qrdich  39346  rmxyneg  39397  rmxyadd  39398  jm2.19lem4  39469  jm2.26lem3  39478  itgpowd  39701  int-rightdistd  40414  binomcxplemnn0  40561  binomcxplemrat  40562  binomcxplemfrat  40563  binomcxplemdvbinom  40565  binomcxplemnotnn0  40568  sub2times  41420  clim1fr1  41762  limcperiod  41789  addlimc  41809  coseq0  42025  fprodaddrecnncnvlem  42073  dvxpaek  42105  dvnxpaek  42107  dvnmul  42108  itgiccshift  42145  itgperiod  42146  stoweidlem1  42167  stoweidlem11  42177  stoweidlem13  42179  wallispilem4  42234  wallispilem5  42235  wallispi  42236  wallispi2lem1  42237  wallispi2lem2  42238  wallispi2  42239  stirlinglem1  42240  stirlinglem3  42242  stirlinglem4  42243  stirlinglem5  42244  stirlinglem6  42245  stirlinglem7  42246  stirlinglem10  42249  stirlinglem11  42250  stirlinglem12  42251  stirlinglem13  42252  stirlinglem15  42254  dirkerper  42262  dirkertrigeqlem1  42264  dirkertrigeqlem2  42265  dirkertrigeqlem3  42266  dirkeritg  42268  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem18  42291  fourierdlem26  42299  fourierdlem30  42303  fourierdlem48  42320  fourierdlem49  42321  fourierdlem79  42351  fourierdlem83  42355  fourierdlem92  42364  fourierdlem93  42365  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  fourierdlem112  42384  smfmullem1  42947  sigaraf  42991  sigaras  42993  readdcnnred  43384  fmtnorec4  43558  quad1  43632  requad01  43633  requad2  43635  fldivmod  44476  dignn0flhalflem1  44573  affinecomb2  44588  eenglngeehlnmlem1  44622  itschlc0yqe  44645  itsclc0yqsollem1  44647  itsclc0yqsol  44649  itscnhlc0xyqsol  44650  itsclc0xyqsolr  44654  2itscplem3  44665  itscnhlinecirc02plem1  44667  inlinecirc02plem  44671  sinhpcosh  44737
  Copyright terms: Public domain W3C validator