Theorem readdcli 11363

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

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7451  ℝcr 11238   + caddc 11242

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

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

This theorem is used by:  resubcli  11659  eqneg  12077  ledivp1i  12282  ltdivp1i  12283  nnne0  12412  2re  12457  3re  12463  4re  12467  5re  12470  6re  12473  7re  12476  8re  12479  9re  12482  10re  12877  numltc  12885  nn0opthlem2  14454  hashunlei  14611  hashge2el2dif  14666  abs3lemi  15622  ef01bndlem  16396  divalglem6  16612  log2ub  27334  mumullem2  27564  bposlem8  27675  dchrvmasumlem2  27882  ex-fl  31105  norm-ii-i  31796  norm3lem  31808  nmoptrii  32753  bdophsi  32755  unierri  32763  staddi  32905  stadd3i  32907  dp2ltc  33549  dpmul4  33576  ballotlem2  35232  hgt750lem  35391  poimirlem16  38822  itg2addnclem3  38859  fdc  38945  remul02  43722  sn-0tie0  43781  pellqrex  44152  stirlinglem11  47367  fouriersw  47514  goldratmolem4  48208  zm1nn  48645  evengpoap3  49170