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  10747  btwnzge0  10750  2tnp1ge0ge0  10751  flhalf  10752  modqltm1p1mod  10828  expnbnd  11116  nn0opthlem2d  11175  ccatalpha  11397  remim  11641  remullem  11652  sq01  11676  caucvgrelemcau  11762  caucvgre  11763  cvg1nlemcxze  11764  cvg1nlemcau  11766  cvg1nlemres  11767  recvguniqlem  11776  resqrexlem1arp  11787  resqrexlemp1rp  11788  resqrexlemf1  11790  resqrexlemfp1  11791  resqrexlemover  11792  resqrexlemdec  11793  resqrexlemlo  11795  resqrexlemcalc1  11796  resqrexlemcalc2  11797  resqrexlemnm  11800  resqrexlemcvg  11801  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemga  11805  abs00ap  11844  absext  11845  absrele  11866  abstri  11887  abs3lem  11894  amgm2  11901  qdenre  11985  maxabsle  11987  maxabslemlub  11990  maxabslemval  11991  maxcl  11993  maxltsup  12001  bdtrilem  12024  bdtri  12025  xrbdtri  12061  mulcn2  12097  fsumabs  12251  cvgratnnlembern  12309  eirraplem  12563  ltoddhalfle  12679  divalglemnqt  12706  bitscmp  12744  4sqlem12  13204  4sqlem15  13207  4sqlem16  13208  2expltfac  13242  ballotfilemsgt1  13306  ballotfilemsel1i  13308  xblss2ps  15604  cnopnap  15811  maxcncf  15815  mincncf  15816  ivthinclemlopn  15836  ivthinclemuopn  15838  hoverb  15848  ivthdichlem  15851  limcimolemlt  15864  efltlemlt  15974  efap1p  15979  cosq23lt0  16034  cosordlem  16051  pellexlem2  16204  efnnfsumcl  16213  efchtqdvds  16239  chtublem  16269  chtqub  16270  bposlem7  16291  bposlem9  16293  lgsdirprm  16332  gausslemma2dlem1a  16356  2sqlem8  16421  qdencn  17251  repiecelem  17253  trilpolemeq1  17269