Theorem readdcli 11251

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 11210	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴 + 𝐵) ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℝcr 11126   + caddc 11130

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

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

This theorem is used by:  resubcli  11547  eqneg  11962  ledivp1i  12167  ltdivp1i  12168  nnne0  12297  2re  12342  3re  12348  4re  12352  5re  12355  6re  12358  7re  12361  8re  12364  9re  12367  10re  12762  numltc  12770  nn0opthlem2  14336  hashunlei  14493  hashge2el2dif  14548  abs3lemi  15501  ef01bndlem  16275  divalglem6  16491  log2ub  27189  mumullem2  27419  bposlem8  27530  dchrvmasumlem2  27737  ex-fl  30930  norm-ii-i  31621  norm3lem  31633  nmoptrii  32578  bdophsi  32580  unierri  32588  staddi  32730  stadd3i  32732  dp2ltc  33335  dpmul4  33362  ballotlem2  35003  hgt750lem  35162  poimirlem16  38388  itg2addnclem3  38425  fdc  38498  remul02  43283  sn-0tie0  43342  pellqrex  43723  stirlinglem11  46915  fouriersw  47062  goldratmolem4  47756  zm1nn  48193  evengpoap3  48718