Theorem readdcld 8299

Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
recnd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
readdcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
readdcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcld

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		readdcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		readdcl 8249	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2203  (class class class)co 6049  ℝcr 8122   + caddc 8126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addrcl 8220

This theorem is referenced by:  ltadd2  8689  leadd1  8700  le2add  8714  lt2add  8715  lesub2  8727  ltsub2  8729  gt0add  8843  reapadd1  8866  apadd1  8878  mulext1  8882  recexaplem2  8922  recp1lt1  9169  cju  9231  peano5nni  9236  peano2nn  9245  div4p1lem1div2  9488  peano2z  9609  difgtsumgt  9643  eluzmn  9856  addlelt  10097  xaddf  10173  xaddval  10174  xleaddadd  10216  lincmble  10333  zltaddlt1le  10337  elincfzoext  10534  zssinfcl  10588  exbtwnzlemstep  10603  exbtwnz  10606  rebtwn2zlemstep  10608  rebtwn2z  10610  qbtwnrelemcalc  10611  flqaddz  10653  btwnzge0  10656  2tnp1ge0ge0  10657  flhalf  10658  modqltm1p1mod  10734  expnbnd  11021  nn0opthlem2d  11079  ccatalpha  11294  remim  11538  remullem  11549  caucvgrelemcau  11658  caucvgre  11659  cvg1nlemcxze  11660  cvg1nlemcau  11662  cvg1nlemres  11663  recvguniqlem  11672  resqrexlem1arp  11683  resqrexlemp1rp  11684  resqrexlemf1  11686  resqrexlemfp1  11687  resqrexlemover  11688  resqrexlemdec  11689  resqrexlemlo  11691  resqrexlemcalc1  11692  resqrexlemcalc2  11693  resqrexlemnm  11696  resqrexlemcvg  11697  resqrexlemoverl  11699  resqrexlemglsq  11700  resqrexlemga  11701  abs00ap  11740  absext  11741  absrele  11761  abstri  11782  abs3lem  11789  amgm2  11796  qdenre  11880  maxabsle  11882  maxabslemlub  11885  maxabslemval  11886  maxcl  11888  maxltsup  11896  bdtrilem  11917  bdtri  11918  xrbdtri  11954  mulcn2  11990  fsumabs  12144  cvgratnnlembern  12202  eirraplem  12456  ltoddhalfle  12572  divalglemnqt  12599  bitscmp  12637  4sqlem12  13093  4sqlem15  13096  4sqlem16  13097  2expltfac  13130  xblss2ps  15256  cnopnap  15463  maxcncf  15467  mincncf  15468  ivthinclemlopn  15488  ivthinclemuopn  15490  hoverb  15500  ivthdichlem  15503  limcimolemlt  15516  efltlemlt  15626  cosq23lt0  15685  cosordlem  15701  pellexlem2  15833  lgsdirprm  15894  gausslemma2dlem1a  15918  2sqlem8  15983  qdencn  16794  repiecelem  16796  trilpolemeq1  16811