Theorem readdcli 11241

Description: Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)

Hypotheses

Ref	Expression
recni.1	⊢ 𝐴 ∈ ℝ
axri.2	⊢ 𝐵 ∈ ℝ

Assertion

Ref	Expression
readdcli	⊢ (𝐴 + 𝐵) ∈ ℝ

Proof of Theorem readdcli

Step	Hyp	Ref	Expression
1		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
2		axri.2	. 2 ⊢ 𝐵 ∈ ℝ
3		readdcl 11200	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴 + 𝐵) ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℝcr 11116   + caddc 11120

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

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

This theorem is used by:  resubcli  11537  eqneg  11952  ledivp1i  12157  ltdivp1i  12158  nnne0  12287  2re  12332  3re  12338  4re  12342  5re  12345  6re  12348  7re  12351  8re  12354  9re  12357  10re  12752  numltc  12760  nn0opthlem2  14325  hashunlei  14482  hashge2el2dif  14537  abs3lemi  15488  ef01bndlem  16264  divalglem6  16480  log2ub  27167  mumullem2  27397  bposlem8  27508  dchrvmasumlem2  27715  ex-fl  30871  norm-ii-i  31562  norm3lem  31574  nmoptrii  32519  bdophsi  32521  unierri  32529  staddi  32671  stadd3i  32673  dp2ltc  33278  dpmul4  33305  ballotlem2  34946  hgt750lem  35105  poimirlem16  38346  itg2addnclem3  38383  fdc  38456  remul02  43226  sn-0tie0  43285  pellqrex  43666  stirlinglem11  46858  fouriersw  47005  zm1nn  48099  evengpoap3  48624