Theorem readdcli 11230

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

This proof depends on syntax axioms:   ∈ wcel 2142  (class class class)co 7412  ℝcr 11105   + caddc 11109

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

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

This theorem is used by:  resubcli  11526  eqneg  11941  ledivp1i  12146  ltdivp1i  12147  nnne0  12276  2re  12321  3re  12327  4re  12331  5re  12334  6re  12337  7re  12340  8re  12343  9re  12346  10re  12740  numltc  12748  nn0opthlem2  14312  hashunlei  14469  hashge2el2dif  14524  abs3lemi  15469  ef01bndlem  16246  divalglem6  16462  log2ub  27125  mumullem2  27355  bposlem8  27466  dchrvmasumlem2  27673  ex-fl  30809  norm-ii-i  31500  norm3lem  31512  nmoptrii  32457  bdophsi  32459  unierri  32467  staddi  32609  stadd3i  32611  dp2ltc  33217  dpmul4  33244  ballotlem2  34888  hgt750lem  35047  poimirlem16  38315  itg2addnclem3  38352  fdc  38424  remul02  43194  sn-0tie0  43253  pellqrex  43634  stirlinglem11  46826  fouriersw  46973  zm1nn  48067  evengpoap3  48592  crossp3i  50676