Theorem readdcld 8362

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  (class class class)co 6088  ℝcr 8185   + caddc 8189

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

This theorem is used by:  ltadd2  8755  leadd1  8766  le2add  8780  lt2add  8781  lesub2  8793  ltsub2  8795  lesub3d  8899  gt0add  8910  reapadd1  8933  apadd1  8945  mulext1  8949  recexaplem2  8989  recp1lt1  9238  cju  9300  peano5nni  9317  peano2nn  9326  div4p1lem1div2  9571  peano2z  9690  difgtsumgt  9724  eluzmn  9944  irraddap  10063  addlelt  10186  xaddf  10263  xaddval  10264  xleaddadd  10306  lincmble  10423  zltaddlt1le  10427  elincfzoext  10628  zssinfcl  10682  exbtwnzlemstep  10699  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2z  10706  qbtwnrelemcalc  10707  flqaddz  10753  btwnzge0  10756  2tnp1ge0ge0  10757  flhalf  10758  modqltm1p1mod  10834  expnbnd  11122  nn0opthlem2d  11181  ccatalpha  11403  remim  11647  remullem  11658  sq01  11682  caucvgrelemcau  11768  caucvgre  11769  cvg1nlemcxze  11770  cvg1nlemcau  11772  cvg1nlemres  11773  recvguniqlem  11782  resqrexlem1arp  11793  resqrexlemp1rp  11794  resqrexlemf1  11796  resqrexlemfp1  11797  resqrexlemover  11798  resqrexlemdec  11799  resqrexlemlo  11801  resqrexlemcalc1  11802  resqrexlemcalc2  11803  resqrexlemnm  11806  resqrexlemcvg  11807  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemga  11811  abs00ap  11850  absext  11851  absrele  11872  abstri  11893  abs3lem  11900  amgm2  11907  qdenre  11991  maxabsle  11993  maxabslemlub  11996  maxabslemval  11997  maxcl  11999  maxltsup  12007  bdtrilem  12030  bdtri  12031  xrbdtri  12067  mulcn2  12103  fsumabs  12257  cvgratnnlembern  12315  eirraplem  12569  ltoddhalfle  12685  divalglemnqt  12712  bitscmp  12750  4sqlem12  13210  4sqlem15  13213  4sqlem16  13214  2expltfac  13248  ballotfilemsgt1  13312  ballotfilemsel1i  13314  ofrle2add  15180  xblss2ps  15663  cnopnap  15870  maxcncf  15874  mincncf  15875  ivthinclemlopn  15895  ivthinclemuopn  15897  hoverb  15907  ivthdichlem  15910  limcimolemlt  15923  efltlemlt  16033  efap1p  16038  cosq23lt0  16093  cosordlem  16110  pellexlem2  16263  efnnfsumcl  16272  efchtqdvds  16298  chtublem  16328  chtqub  16329  bposlem7  16350  bposlem9  16352  lgsdirprm  16391  gausslemma2dlem1a  16415  2sqlem8  16480  qdencn  17311  repiecelem  17313  trilpolemeq1  17329