ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  readdcld GIF version

Theorem readdcld 7759
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
StepHypRef Expression
1 recnd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 readdcld.2 . 2 (𝜑𝐵 ∈ ℝ)
3 readdcl 7710 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3syl2anc 406 1 (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1463  (class class class)co 5740  cr 7583   + caddc 7587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-addrcl 7681
This theorem is referenced by:  ltadd2  8145  leadd1  8156  le2add  8170  lt2add  8171  lesub2  8183  ltsub2  8185  gt0add  8298  reapadd1  8321  apadd1  8333  mulext1  8337  recexaplem2  8376  recp1lt1  8617  cju  8679  peano5nni  8683  peano2nn  8692  div4p1lem1div2  8927  peano2z  9044  addlelt  9506  xaddf  9578  xaddval  9579  xleaddadd  9621  zltaddlt1le  9740  exbtwnzlemstep  9976  exbtwnz  9979  rebtwn2zlemstep  9981  rebtwn2z  9983  qbtwnrelemcalc  9984  flqaddz  10021  btwnzge0  10024  2tnp1ge0ge0  10025  flhalf  10026  modqltm1p1mod  10100  expnbnd  10366  nn0opthlem2d  10418  remim  10583  remullem  10594  caucvgrelemcau  10703  caucvgre  10704  cvg1nlemcxze  10705  cvg1nlemcau  10707  cvg1nlemres  10708  recvguniqlem  10717  resqrexlem1arp  10728  resqrexlemp1rp  10729  resqrexlemf1  10731  resqrexlemfp1  10732  resqrexlemover  10733  resqrexlemdec  10734  resqrexlemlo  10736  resqrexlemcalc1  10737  resqrexlemcalc2  10738  resqrexlemnm  10741  resqrexlemcvg  10742  resqrexlemoverl  10744  resqrexlemglsq  10745  resqrexlemga  10746  abs00ap  10785  absext  10786  absrele  10806  abstri  10827  abs3lem  10834  amgm2  10841  qdenre  10925  maxabsle  10927  maxabslemlub  10930  maxabslemval  10931  maxcl  10933  maxltsup  10941  bdtrilem  10961  bdtri  10962  xrbdtri  10996  mulcn2  11032  fsumabs  11185  cvgratnnlembern  11243  eirraplem  11390  ltoddhalfle  11497  divalglemnqt  11524  zssinfcl  11548  xblss2ps  12479  cnopnap  12669  ivthinclemlopn  12689  ivthinclemuopn  12691  limcimolemlt  12708  qdencn  13056  trilpolemeq1  13067
  Copyright terms: Public domain W3C validator