Theorem addcld 11252

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7413  ℂcc 11122   + caddc 11127

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

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

This theorem is used by:  cnegex  11415  addcom  11420  addcomd  11436  muladd11r  11447  negeu  11471  addsubass  11491  subsub2  11510  subsub4  11515  pnncan  11523  addsub4  11525  addsubsub23  11646  pnpncand  11659  addmulsub  11700  subaddmulsub  11701  mulsubaddmulsub  11702  divdir  11921  cju  12238  cnref1o  13035  xov1plusxeqvd  13551  modaddb  13970  expaddz  14170  binom3  14288  sqoddm1div8  14307  mulsubdivbinom2  14326  muldivbinom2  14327  spllen  14823  crre  15201  remullem  15215  imval2  15238  cjreim2  15248  sqreulem  15447  bhmafibid1cn  15553  bhmafibid2cn  15554  bhmafibid1  15555  bhmafibid2  15556  addcn2  15681  o1add  15701  rlimadd  15730  fsumadd  15826  isumadd  15853  binomlem  15918  binomfallfaclem2  16126  bpoly4  16145  fsumcube  16146  efaddlem  16179  ef4p  16201  cosf  16213  tanval2  16221  tanval3  16222  resin4p  16226  recos4p  16227  efival  16240  sinadd  16252  cosadd  16253  tanadd  16255  pwp1fsum  16481  sadadd2lem2  16540  sadadd2lem  16549  pythagtriplem1  16908  pythagtriplem12  16918  pythagtriplem17  16923  pcbc  16992  mul4sqlem  17045  4sqlem14  17050  vdwlem6  17078  vdwlem9  17081  mulgdirlem  19228  blcvx  25024  cphpyth  25444  tcphcphlem1  25463  cphipval2  25469  4cphipval2  25470  csbren  25627  ovollb2lem  25716  mbfadd  25889  itgcnlem  26017  itgaddlem2  26051  dvmptre  26196  dvsincos  26208  itgpowd  26277  taylthlem2  26610  ptolemy  26734  tanregt0  26776  eff1olem  26785  cosargd  26845  tanarg  26856  logf1o2  26887  efopn  26895  cxpsqrtlem  26939  cxpeq  26994  ang180lem1  27046  ang180lem2  27047  ang180lem3  27048  ang180lem4  27049  pythag  27054  ssscongptld  27059  chordthmlem  27069  chordthmlem2  27070  chordthmlem3  27071  chordthmlem4  27072  chordthmlem5  27073  heron  27075  quad2  27076  dcubic1lem  27080  dcubic2  27081  dcubic1  27082  dcubic  27083  mcubic  27084  cubic2  27085  cubic  27086  binom4  27087  dquartlem1  27088  dquartlem2  27089  dquart  27090  quart1cl  27091  quart1lem  27092  quart1  27093  quartlem1  27094  quartlem2  27095  quartlem3  27096  quartlem4  27097  quart  27098  asinlem3  27108  asinf  27109  asinneg  27123  efiasin  27125  asinsinlem  27128  asinsin  27129  asinbnd  27136  atanlogaddlem  27150  dmgmaddnn0  27263  dmgmdivn0  27264  lgamgulmlem2  27266  lgamgulmlem3  27267  lgamgulmlem4  27268  lgamgulmlem5  27269  lgamgulmlem6  27270  lgamgulm2  27272  lgambdd  27273  lgamucov  27274  lgamcvg2  27291  gamcvg  27292  gamcvg2lem  27295  ftalem7  27315  basellem3  27319  bposlem9  27528  lgsquad2lem1  27620  2lgslem3d1  27639  2sqmod  27672  dchrvmasumiflem2  27738  mulogsumlem  27767  mulog2sumlem1  27770  mulog2sumlem2  27771  mulog2sumlem3  27772  selberglem1  27781  selberg2  27787  selberg3lem1  27793  selbergr  27804  selberg3r  27805  pntrlog2bndlem1  27813  pntrlog2bndlem2  27814  pntrlog2bndlem5  27817  pntrlog2bndlem6  27819  pntrlog2bnd  27820  brbtwn2  29362  colinearalglem1  29363  colinearalglem2  29364  axeuclidlem  29419  axcontlem2  29422  axcontlem7  29427  axcontlem8  29428  finsumvtxdg2ssteplem4  30008  wwlksext2clwwlk  30527  4ipval2  31189  dipcj  31195  golem1  32752  submuladdd  33211  binom2subadd  33212  pythagreim  33216  quad3d  33220  lt2addrd  33221  cycpmco2lem3  33568  cycpmco2lem4  33569  cycpmco2lem5  33570  cycpmco2lem6  33571  cycpmco2  33573  archirngz  33629  archiabllem2c  33635  zringfrac  33964  ccfldextdgrr  34182  constrrtll  34241  constrrtlc1  34242  constrrtcclem  34244  constrrtcc  34245  constrfin  34256  nn0constr  34271  constraddcl  34272  constrrecl  34279  constrresqrtcl  34287  constrsqrtcl  34289  cos9thpiminplylem1  34292  cos9thpiminplylem2  34293  cos9thpiminplylem3  34294  cos9thpiminply  34298  cos9thpinconstrlem1  34299  cos9thpinconstrlem2  34300  cnre2csqima  34421  ballotlemsima  35027  hgt750lemb  35164  iprodgam  36321  dnizphlfeqhlf  37173  dnibndlem9  37183  knoppndvlem16  37224  qdiff  38079  itg2addnclem3  38422  itgaddnclem2  38428  itgaddnc  38429  ftc1anclem6  38447  ftc1anclem8  38449  dvasin  38453  areacirclem1  38457  areacirclem4  38460  areacirc  38462  lcmineqlem6  42900  lcmineqlem11  42905  lcmineqlem18  42912  aks4d1p1p2  42936  aks4d1p1p6  42939  aks4d1p1p7  42940  aks4d1p1p5  42941  posbezout  42966  2np3bcnp1  43010  2ap1caineq  43011  sticksstones12a  43023  bcle2d  43045  quadfac  43071  mvrrsubd  43149  lsubrotld  43152  oddnumth  43186  sumcubes  43188  cxp112d  43216  cxp111d  43217  sn-negex12  43292  sn-addrid  43296  sn-subeu  43302  sn-0tie0  43339  zaddcomlem  43351  zaddcom  43352  cnreeu  43378  dffltz  43480  cu3addd  43526  3cubeslem2  43530  3cubeslem3l  43531  3cubeslem3r  43532  3cubeslem4  43534  pellexlem2  43671  pellexlem6  43675  pell1234qrreccl  43695  pell1234qrmulcl  43696  pell14qrdich  43710  rmxyneg  43761  rmxyadd  43762  jm2.19lem4  43833  jm2.26lem3  43842  sqrtcval  44481  int-rightdistd  45020  binomcxplemnn0  45173  binomcxplemrat  45174  binomcxplemfrat  45175  binomcxplemdvbinom  45177  binomcxplemnotnn0  45180  sub2times  46106  clim1fr1  46431  limcperiod  46458  addlimc  46476  coseq0  46692  fprodaddrecnncnvlem  46737  dvxpaek  46768  dvnxpaek  46770  dvnmul  46771  itgiccshift  46808  itgperiod  46809  stoweidlem1  46829  stoweidlem11  46839  stoweidlem13  46841  wallispilem4  46896  wallispilem5  46897  wallispi  46898  wallispi2lem1  46899  wallispi2lem2  46900  wallispi2  46901  stirlinglem1  46902  stirlinglem3  46904  stirlinglem4  46905  stirlinglem5  46906  stirlinglem6  46907  stirlinglem7  46908  stirlinglem10  46911  stirlinglem11  46912  stirlinglem12  46913  stirlinglem13  46914  stirlinglem15  46916  dirkerper  46924  dirkertrigeqlem1  46926  dirkertrigeqlem2  46927  dirkertrigeqlem3  46928  dirkeritg  46930  dirkercncflem2  46932  dirkercncflem4  46934  fourierdlem18  46953  fourierdlem26  46961  fourierdlem30  46965  fourierdlem48  46982  fourierdlem49  46983  fourierdlem79  47013  fourierdlem83  47017  fourierdlem92  47026  fourierdlem93  47027  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  fourierdlem112  47046  smfmullem1  47619  sigaraf  47681  sigaras  47683  sin5tlem1  47737  sin5tlem4  47740  sin5tlem5  47741  readdcnnred  48191  fldivmod  48232  fmtnorec4  48452  quad1  48536  requad01  48537  requad2  48539  gpgedgvtx1  48978  dignn0flhalflem1  49545  affinecomb2  49633  eenglngeehlnmlem1  49667  itschlc0yqe  49690  itsclc0yqsollem1  49692  itsclc0yqsol  49694  itscnhlc0xyqsol  49695  itsclc0xyqsolr  49699  2itscplem3  49710  itscnhlinecirc02plem1  49712  inlinecirc02plem  49716  sinhpcosh  50666  crossp3d  50800  veroquadgsumlem  50816