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

Theorem readdcld 7974
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 7925 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3syl2anc 411 1 (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2148  (class class class)co 5869  cr 7798   + caddc 7802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addrcl 7896
This theorem is referenced by:  ltadd2  8363  leadd1  8374  le2add  8388  lt2add  8389  lesub2  8401  ltsub2  8403  gt0add  8517  reapadd1  8540  apadd1  8552  mulext1  8556  recexaplem2  8595  recp1lt1  8842  cju  8904  peano5nni  8908  peano2nn  8917  div4p1lem1div2  9158  peano2z  9275  difgtsumgt  9308  addlelt  9752  xaddf  9828  xaddval  9829  xleaddadd  9871  zltaddlt1le  9991  exbtwnzlemstep  10231  exbtwnz  10234  rebtwn2zlemstep  10236  rebtwn2z  10238  qbtwnrelemcalc  10239  flqaddz  10280  btwnzge0  10283  2tnp1ge0ge0  10284  flhalf  10285  modqltm1p1mod  10359  expnbnd  10626  nn0opthlem2d  10682  remim  10850  remullem  10861  caucvgrelemcau  10970  caucvgre  10971  cvg1nlemcxze  10972  cvg1nlemcau  10974  cvg1nlemres  10975  recvguniqlem  10984  resqrexlem1arp  10995  resqrexlemp1rp  10996  resqrexlemf1  10998  resqrexlemfp1  10999  resqrexlemover  11000  resqrexlemdec  11001  resqrexlemlo  11003  resqrexlemcalc1  11004  resqrexlemcalc2  11005  resqrexlemnm  11008  resqrexlemcvg  11009  resqrexlemoverl  11011  resqrexlemglsq  11012  resqrexlemga  11013  abs00ap  11052  absext  11053  absrele  11073  abstri  11094  abs3lem  11101  amgm2  11108  qdenre  11192  maxabsle  11194  maxabslemlub  11197  maxabslemval  11198  maxcl  11200  maxltsup  11208  bdtrilem  11228  bdtri  11229  xrbdtri  11265  mulcn2  11301  fsumabs  11454  cvgratnnlembern  11512  eirraplem  11765  ltoddhalfle  11878  divalglemnqt  11905  zssinfcl  11929  xblss2ps  13564  cnopnap  13754  ivthinclemlopn  13774  ivthinclemuopn  13776  limcimolemlt  13793  efltlemlt  13855  cosq23lt0  13914  cosordlem  13930  lgsdirprm  14095  2sqlem8  14119  qdencn  14424  trilpolemeq1  14437
  Copyright terms: Public domain W3C validator