Theorem readdcld 8356

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 8306	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  (class class class)co 6085  ℝcr 8179   + caddc 8183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addrcl 8277

This theorem is used by:  ltadd2  8749  leadd1  8760  le2add  8774  lt2add  8775  lesub2  8787  ltsub2  8789  lesub3d  8893  gt0add  8904  reapadd1  8927  apadd1  8939  mulext1  8943  recexaplem2  8983  recp1lt1  9232  cju  9294  peano5nni  9310  peano2nn  9319  div4p1lem1div2  9564  peano2z  9685  difgtsumgt  9719  eluzmn  9938  irraddap  10057  addlelt  10180  xaddf  10257  xaddval  10258  xleaddadd  10300  lincmble  10417  zltaddlt1le  10421  elincfzoext  10622  zssinfcl  10676  exbtwnzlemstep  10693  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnrelemcalc  10701  flqaddz  10746  btwnzge0  10749  2tnp1ge0ge0  10750  flhalf  10751  modqltm1p1mod  10827  expnbnd  11115  nn0opthlem2d  11174  ccatalpha  11396  remim  11640  remullem  11651  sq01  11675  caucvgrelemcau  11761  caucvgre  11762  cvg1nlemcxze  11763  cvg1nlemcau  11765  cvg1nlemres  11766  recvguniqlem  11775  resqrexlem1arp  11786  resqrexlemp1rp  11787  resqrexlemf1  11789  resqrexlemfp1  11790  resqrexlemover  11791  resqrexlemdec  11792  resqrexlemlo  11794  resqrexlemcalc1  11795  resqrexlemcalc2  11796  resqrexlemnm  11799  resqrexlemcvg  11800  resqrexlemoverl  11802  resqrexlemglsq  11803  resqrexlemga  11804  abs00ap  11843  absext  11844  absrele  11865  abstri  11886  abs3lem  11893  amgm2  11900  qdenre  11984  maxabsle  11986  maxabslemlub  11989  maxabslemval  11990  maxcl  11992  maxltsup  12000  bdtrilem  12023  bdtri  12024  xrbdtri  12060  mulcn2  12096  fsumabs  12250  cvgratnnlembern  12308  eirraplem  12562  ltoddhalfle  12678  divalglemnqt  12705  bitscmp  12743  4sqlem12  13203  4sqlem15  13206  4sqlem16  13207  2expltfac  13241  ballotfilemsgt1  13305  ballotfilemsel1i  13307  xblss2ps  15557  cnopnap  15764  maxcncf  15768  mincncf  15769  ivthinclemlopn  15789  ivthinclemuopn  15791  hoverb  15801  ivthdichlem  15804  limcimolemlt  15817  efltlemlt  15927  efap1p  15932  cosq23lt0  15987  cosordlem  16003  pellexlem2  16152  efnnfsumcl  16161  efchtqdvds  16187  chtublem  16217  chtqub  16218  lgsdirprm  16275  gausslemma2dlem1a  16299  2sqlem8  16364  qdencn  17194  repiecelem  17196  trilpolemeq1  17211