Theorem addcld 11155

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

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addcl 11111	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 590	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027   + caddc 11032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 11089

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  cnegex  11318  addcom  11323  addcomd  11339  muladd11r  11350  negeu  11374  addsubass  11394  subsub2  11413  subsub4  11418  pnncan  11426  addsub4  11428  addsubsub23  11549  pnpncand  11562  addmulsub  11603  subaddmulsub  11604  mulsubaddmulsub  11605  divdir  11825  cju  12146  cnref1o  12926  xov1plusxeqvd  13442  modaddb  13859  expaddz  14059  binom3  14177  sqoddm1div8  14196  mulsubdivbinom2  14215  muldivbinom2  14216  spllen  14707  crre  15067  remullem  15081  imval2  15104  cjreim2  15114  sqreulem  15313  bhmafibid1cn  15419  bhmafibid2cn  15420  bhmafibid1  15421  bhmafibid2  15422  addcn2  15547  o1add  15567  rlimadd  15596  fsumadd  15693  isumadd  15720  binomlem  15785  binomfallfaclem2  15996  bpoly4  16015  fsumcube  16016  efaddlem  16049  ef4p  16071  cosf  16083  tanval2  16091  tanval3  16092  resin4p  16096  recos4p  16097  efival  16110  sinadd  16122  cosadd  16123  tanadd  16125  pwp1fsum  16351  sadadd2lem2  16410  sadadd2lem  16419  pythagtriplem1  16778  pythagtriplem12  16788  pythagtriplem17  16793  pcbc  16862  mul4sqlem  16915  4sqlem14  16920  vdwlem6  16948  vdwlem9  16951  mulgdirlem  19072  blcvx  24781  cphpyth  25201  tcphcphlem1  25220  cphipval2  25226  4cphipval2  25227  csbren  25384  ovollb2lem  25473  mbfadd  25646  itgcnlem  25775  itgaddlem2  25809  dvmptre  25954  dvsincos  25966  itgpowd  26035  taylthlem2  26357  ptolemy  26478  tanregt0  26521  eff1olem  26530  cosargd  26590  tanarg  26601  logf1o2  26632  efopn  26640  cxpsqrtlem  26684  cxpeq  26739  ang180lem1  26791  ang180lem2  26792  ang180lem3  26793  ang180lem4  26794  pythag  26799  ssscongptld  26804  chordthmlem  26814  chordthmlem2  26815  chordthmlem3  26816  chordthmlem4  26817  chordthmlem5  26818  heron  26820  quad2  26821  dcubic1lem  26825  dcubic2  26826  dcubic1  26827  dcubic  26828  mcubic  26829  cubic2  26830  cubic  26831  binom4  26832  dquartlem1  26833  dquartlem2  26834  dquart  26835  quart1cl  26836  quart1lem  26837  quart1  26838  quartlem1  26839  quartlem2  26840  quartlem3  26841  quartlem4  26842  quart  26843  asinlem3  26853  asinf  26854  asinneg  26868  efiasin  26870  asinsinlem  26873  asinsin  26874  asinbnd  26881  atanlogaddlem  26895  dmgmaddnn0  27008  dmgmdivn0  27009  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem4  27013  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgambdd  27018  lgamucov  27019  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  ftalem7  27060  basellem3  27064  bposlem9  27273  lgsquad2lem1  27365  2lgslem3d1  27384  2sqmod  27417  dchrvmasumiflem2  27483  mulogsumlem  27512  mulog2sumlem1  27515  mulog2sumlem2  27516  mulog2sumlem3  27517  selberglem1  27526  selberg2  27532  selberg3lem1  27538  selbergr  27549  selberg3r  27550  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntrlog2bnd  27565  brbtwn2  28992  colinearalglem1  28993  colinearalglem2  28994  axeuclidlem  29049  axcontlem2  29052  axcontlem7  29057  axcontlem8  29058  finsumvtxdg2ssteplem4  29635  wwlksext2clwwlk  30145  4ipval2  30797  dipcj  30803  golem1  32360  submuladdd  32832  binom2subadd  32833  pythagreim  32837  quad3d  32841  lt2addrd  32842  cycpmco2lem3  33209  cycpmco2lem4  33210  cycpmco2lem5  33211  cycpmco2lem6  33212  cycpmco2  33214  archirngz  33270  archiabllem2c  33276  zringfrac  33637  ccfldextdgrr  33856  constrrtll  33915  constrrtlc1  33916  constrrtcclem  33918  constrrtcc  33919  constrfin  33930  nn0constr  33945  constraddcl  33946  constrrecl  33953  constrresqrtcl  33961  constrsqrtcl  33963  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  cos9thpiminply  33972  cos9thpinconstrlem1  33973  cos9thpinconstrlem2  33974  cnre2csqima  34095  ballotlemsima  34700  hgt750lemb  34840  iprodgam  35970  dnizphlfeqhlf  36782  dnibndlem9  36792  knoppndvlem16  36833  qdiff  37687  itg2addnclem3  38040  itgaddnclem2  38046  itgaddnc  38047  ftc1anclem6  38065  ftc1anclem8  38067  dvasin  38071  areacirclem1  38075  areacirclem4  38078  areacirc  38080  lcmineqlem6  42519  lcmineqlem11  42524  lcmineqlem18  42531  aks4d1p1p2  42555  aks4d1p1p6  42558  aks4d1p1p7  42559  aks4d1p1p5  42560  posbezout  42585  2np3bcnp1  42629  2ap1caineq  42630  sticksstones12a  42642  bcle2d  42664  mvrrsubd  42751  lsubrotld  42754  oddnumth  42788  sumcubes  42790  cxp112d  42818  cxp111d  42819  sn-negex12  42894  sn-addrid  42898  sn-subeu  42904  sn-0tie0  42941  zaddcomlem  42953  zaddcom  42954  cnreeu  42980  dffltz  43084  cu3addd  43130  3cubeslem2  43134  3cubeslem3l  43135  3cubeslem3r  43136  3cubeslem4  43138  pellexlem2  43275  pellexlem6  43279  pell1234qrreccl  43299  pell1234qrmulcl  43300  pell14qrdich  43314  rmxyneg  43365  rmxyadd  43366  jm2.19lem4  43437  jm2.26lem3  43446  sqrtcval  44085  int-rightdistd  44624  binomcxplemnn0  44793  binomcxplemrat  44794  binomcxplemfrat  44795  binomcxplemdvbinom  44797  binomcxplemnotnn0  44800  sub2times  45721  clim1fr1  46046  limcperiod  46073  addlimc  46091  coseq0  46307  fprodaddrecnncnvlem  46352  dvxpaek  46383  dvnxpaek  46385  dvnmul  46386  itgiccshift  46423  itgperiod  46424  stoweidlem1  46444  stoweidlem11  46454  stoweidlem13  46456  wallispilem4  46511  wallispilem5  46512  wallispi  46513  wallispi2lem1  46514  wallispi2lem2  46515  wallispi2  46516  stirlinglem1  46517  stirlinglem3  46519  stirlinglem4  46520  stirlinglem5  46521  stirlinglem6  46522  stirlinglem7  46523  stirlinglem10  46526  stirlinglem11  46527  stirlinglem12  46528  stirlinglem13  46529  stirlinglem15  46531  dirkerper  46539  dirkertrigeqlem1  46541  dirkertrigeqlem2  46542  dirkertrigeqlem3  46543  dirkeritg  46545  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem18  46568  fourierdlem26  46576  fourierdlem30  46580  fourierdlem48  46597  fourierdlem49  46598  fourierdlem79  46628  fourierdlem83  46632  fourierdlem92  46641  fourierdlem93  46642  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fourierdlem112  46661  smfmullem1  47234  sigaraf  47296  sigaras  47298  sin5tlem1  47336  sin5tlem4  47339  sin5tlem5  47340  readdcnnred  47766  fldivmod  47807  fmtnorec4  48027  quad1  48111  requad01  48112  requad2  48114  gpgedgvtx1  48553  dignn0flhalflem1  49106  affinecomb2  49194  eenglngeehlnmlem1  49228  itschlc0yqe  49251  itsclc0yqsollem1  49253  itsclc0yqsol  49255  itscnhlc0xyqsol  49256  itsclc0xyqsolr  49260  2itscplem3  49271  itscnhlinecirc02plem1  49273  inlinecirc02plem  49277  sinhpcosh  50230