Theorem addcld 11243

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 11197	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7419  ℂcc 11113   + caddc 11118

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 11175

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  cnegex  11406  addcom  11411  addcomd  11427  muladd11r  11438  negeu  11462  addsubass  11482  subsub2  11501  subsub4  11506  pnncan  11514  addsub4  11516  addsubsub23  11637  pnpncand  11650  addmulsub  11691  subaddmulsub  11692  mulsubaddmulsub  11693  divdir  11912  cju  12229  cnref1o  13025  xov1plusxeqvd  13541  modaddb  13960  expaddz  14160  binom3  14278  sqoddm1div8  14297  mulsubdivbinom2  14316  muldivbinom2  14317  spllen  14813  crre  15189  remullem  15203  imval2  15226  cjreim2  15236  sqreulem  15435  bhmafibid1cn  15541  bhmafibid2cn  15542  bhmafibid1  15543  bhmafibid2  15544  addcn2  15669  o1add  15689  rlimadd  15718  fsumadd  15814  isumadd  15841  binomlem  15906  binomfallfaclem2  16116  bpoly4  16135  fsumcube  16136  efaddlem  16169  ef4p  16191  cosf  16203  tanval2  16211  tanval3  16212  resin4p  16216  recos4p  16217  efival  16230  sinadd  16242  cosadd  16243  tanadd  16245  pwp1fsum  16471  sadadd2lem2  16530  sadadd2lem  16539  pythagtriplem1  16898  pythagtriplem12  16908  pythagtriplem17  16913  pcbc  16982  mul4sqlem  17035  4sqlem14  17040  vdwlem6  17068  vdwlem9  17071  mulgdirlem  19215  blcvx  25006  cphpyth  25426  tcphcphlem1  25445  cphipval2  25451  4cphipval2  25452  csbren  25609  ovollb2lem  25698  mbfadd  25871  itgcnlem  26000  itgaddlem2  26034  dvmptre  26179  dvsincos  26191  itgpowd  26260  taylthlem2  26588  ptolemy  26712  tanregt0  26755  eff1olem  26764  cosargd  26824  tanarg  26835  logf1o2  26866  efopn  26874  cxpsqrtlem  26918  cxpeq  26973  ang180lem1  27025  ang180lem2  27026  ang180lem3  27027  ang180lem4  27028  pythag  27033  ssscongptld  27038  chordthmlem  27048  chordthmlem2  27049  chordthmlem3  27050  chordthmlem4  27051  chordthmlem5  27052  heron  27054  quad2  27055  dcubic1lem  27059  dcubic2  27060  dcubic1  27061  dcubic  27062  mcubic  27063  cubic2  27064  cubic  27065  binom4  27066  dquartlem1  27067  dquartlem2  27068  dquart  27069  quart1cl  27070  quart1lem  27071  quart1  27072  quartlem1  27073  quartlem2  27074  quartlem3  27075  quartlem4  27076  quart  27077  asinlem3  27087  asinf  27088  asinneg  27102  efiasin  27104  asinsinlem  27107  asinsin  27108  asinbnd  27115  atanlogaddlem  27129  dmgmaddnn0  27242  dmgmdivn0  27243  lgamgulmlem2  27245  lgamgulmlem3  27246  lgamgulmlem4  27247  lgamgulmlem5  27248  lgamgulmlem6  27249  lgamgulm2  27251  lgambdd  27252  lgamucov  27253  lgamcvg2  27270  gamcvg  27271  gamcvg2lem  27274  ftalem7  27294  basellem3  27298  bposlem9  27507  lgsquad2lem1  27599  2lgslem3d1  27618  2sqmod  27651  dchrvmasumiflem2  27717  mulogsumlem  27746  mulog2sumlem1  27749  mulog2sumlem2  27750  mulog2sumlem3  27751  selberglem1  27760  selberg2  27766  selberg3lem1  27772  selbergr  27783  selberg3r  27784  pntrlog2bndlem1  27792  pntrlog2bndlem2  27793  pntrlog2bndlem5  27796  pntrlog2bndlem6  27798  pntrlog2bnd  27799  brbtwn2  29310  colinearalglem1  29311  colinearalglem2  29312  axeuclidlem  29367  axcontlem2  29370  axcontlem7  29375  axcontlem8  29376  finsumvtxdg2ssteplem4  29956  wwlksext2clwwlk  30475  4ipval2  31131  dipcj  31137  golem1  32694  submuladdd  33155  binom2subadd  33156  pythagreim  33160  quad3d  33164  lt2addrd  33165  cycpmco2lem3  33512  cycpmco2lem4  33513  cycpmco2lem5  33514  cycpmco2lem6  33515  cycpmco2  33517  archirngz  33573  archiabllem2c  33579  zringfrac  33908  ccfldextdgrr  34126  constrrtll  34185  constrrtlc1  34186  constrrtcclem  34188  constrrtcc  34189  constrfin  34200  nn0constr  34215  constraddcl  34216  constrrecl  34223  constrresqrtcl  34231  constrsqrtcl  34233  cos9thpiminplylem1  34236  cos9thpiminplylem2  34237  cos9thpiminplylem3  34238  cos9thpiminply  34242  cos9thpinconstrlem1  34243  cos9thpinconstrlem2  34244  cnre2csqima  34365  ballotlemsima  34971  hgt750lemb  35108  iprodgam  36271  dnizphlfeqhlf  37122  dnibndlem9  37132  knoppndvlem16  37173  qdiff  38028  itg2addnclem3  38381  itgaddnclem2  38387  itgaddnc  38388  ftc1anclem6  38406  ftc1anclem8  38408  dvasin  38412  areacirclem1  38416  areacirclem4  38419  areacirc  38421  lcmineqlem6  42859  lcmineqlem11  42864  lcmineqlem18  42871  aks4d1p1p2  42895  aks4d1p1p6  42898  aks4d1p1p7  42899  aks4d1p1p5  42900  posbezout  42925  2np3bcnp1  42969  2ap1caineq  42970  sticksstones12a  42982  bcle2d  43004  quadfac  43030  mvrrsubd  43093  lsubrotld  43096  oddnumth  43130  sumcubes  43132  cxp112d  43160  cxp111d  43161  sn-negex12  43236  sn-addrid  43240  sn-subeu  43246  sn-0tie0  43283  zaddcomlem  43295  zaddcom  43296  cnreeu  43322  dffltz  43424  cu3addd  43470  3cubeslem2  43474  3cubeslem3l  43475  3cubeslem3r  43476  3cubeslem4  43478  pellexlem2  43615  pellexlem6  43619  pell1234qrreccl  43639  pell1234qrmulcl  43640  pell14qrdich  43654  rmxyneg  43705  rmxyadd  43706  jm2.19lem4  43777  jm2.26lem3  43786  sqrtcval  44425  int-rightdistd  44964  binomcxplemnn0  45117  binomcxplemrat  45118  binomcxplemfrat  45119  binomcxplemdvbinom  45121  binomcxplemnotnn0  45124  sub2times  46050  clim1fr1  46375  limcperiod  46402  addlimc  46420  coseq0  46636  fprodaddrecnncnvlem  46681  dvxpaek  46712  dvnxpaek  46714  dvnmul  46715  itgiccshift  46752  itgperiod  46753  stoweidlem1  46773  stoweidlem11  46783  stoweidlem13  46785  wallispilem4  46840  wallispilem5  46841  wallispi  46842  wallispi2lem1  46843  wallispi2lem2  46844  wallispi2  46845  stirlinglem1  46846  stirlinglem3  46848  stirlinglem4  46849  stirlinglem5  46850  stirlinglem6  46851  stirlinglem7  46852  stirlinglem10  46855  stirlinglem11  46856  stirlinglem12  46857  stirlinglem13  46858  stirlinglem15  46860  dirkerper  46868  dirkertrigeqlem1  46870  dirkertrigeqlem2  46871  dirkertrigeqlem3  46872  dirkeritg  46874  dirkercncflem2  46876  dirkercncflem4  46878  fourierdlem18  46897  fourierdlem26  46905  fourierdlem30  46909  fourierdlem48  46926  fourierdlem49  46927  fourierdlem79  46957  fourierdlem83  46961  fourierdlem92  46970  fourierdlem93  46971  fourierdlem103  46981  fourierdlem104  46982  fourierdlem111  46989  fourierdlem112  46990  smfmullem1  47563  sigaraf  47625  sigaras  47627  sin5tlem1  47668  sin5tlem4  47671  sin5tlem5  47672  readdcnnred  48098  fldivmod  48139  fmtnorec4  48359  quad1  48443  requad01  48444  requad2  48446  gpgedgvtx1  48885  dignn0flhalflem1  49452  affinecomb2  49540  eenglngeehlnmlem1  49574  itschlc0yqe  49597  itsclc0yqsollem1  49599  itsclc0yqsol  49601  itscnhlc0xyqsol  49602  itsclc0xyqsolr  49606  2itscplem3  49617  itscnhlinecirc02plem1  49619  inlinecirc02plem  49623  sinhpcosh  50575  crossp3d  50706