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

Theorem readdcld 7759
Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1  |-  ( ph  ->  A  e.  RR )
readdcld.2  |-  ( ph  ->  B  e.  RR )
Assertion
Ref Expression
readdcld  |-  ( ph  ->  ( A  +  B
)  e.  RR )

Proof of Theorem readdcld
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 readdcld.2 . 2  |-  ( ph  ->  B  e.  RR )
3 readdcl 7710 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 406 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1463  (class class class)co 5740   RRcr 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  8373  recp1lt1  8614  cju  8676  peano5nni  8680  peano2nn  8689  div4p1lem1div2  8924  peano2z  9041  addlelt  9495  xaddf  9567  xaddval  9568  xleaddadd  9610  zltaddlt1le  9729  exbtwnzlemstep  9965  exbtwnz  9968  rebtwn2zlemstep  9970  rebtwn2z  9972  qbtwnrelemcalc  9973  flqaddz  10010  btwnzge0  10013  2tnp1ge0ge0  10014  flhalf  10015  modqltm1p1mod  10089  expnbnd  10355  nn0opthlem2d  10407  remim  10572  remullem  10583  caucvgrelemcau  10692  caucvgre  10693  cvg1nlemcxze  10694  cvg1nlemcau  10696  cvg1nlemres  10697  recvguniqlem  10706  resqrexlem1arp  10717  resqrexlemp1rp  10718  resqrexlemf1  10720  resqrexlemfp1  10721  resqrexlemover  10722  resqrexlemdec  10723  resqrexlemlo  10725  resqrexlemcalc1  10726  resqrexlemcalc2  10727  resqrexlemnm  10730  resqrexlemcvg  10731  resqrexlemoverl  10733  resqrexlemglsq  10734  resqrexlemga  10735  abs00ap  10774  absext  10775  absrele  10795  abstri  10816  abs3lem  10823  amgm2  10830  qdenre  10914  maxabsle  10916  maxabslemlub  10919  maxabslemval  10920  maxcl  10922  maxltsup  10930  bdtrilem  10950  bdtri  10951  xrbdtri  10985  mulcn2  11021  fsumabs  11174  cvgratnnlembern  11232  eirraplem  11379  ltoddhalfle  11486  divalglemnqt  11513  zssinfcl  11537  xblss2ps  12468  cnopnap  12658  limcimolemlt  12676  qdencn  13024  trilpolemeq1  13035
  Copyright terms: Public domain W3C validator