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

Theorem readdcld 7280
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 7231 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 403 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434  (class class class)co 5564   RRcr 7112    + caddc 7116
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-addrcl 7205
This theorem is referenced by:  ltadd2  7660  leadd1  7671  le2add  7685  lt2add  7686  lesub2  7698  ltsub2  7700  gt0add  7810  reapadd1  7833  apadd1  7845  mulext1  7849  recexaplem2  7879  recp1lt1  8114  cju  8175  peano5nni  8179  peano2nn  8188  div4p1lem1div2  8421  peano2z  8538  addlelt  8990  zltaddlt1le  9174  exbtwnzlemstep  9404  exbtwnz  9407  rebtwn2zlemstep  9409  rebtwn2z  9411  qbtwnrelemcalc  9412  flqaddz  9449  btwnzge0  9452  2tnp1ge0ge0  9453  flhalf  9454  modqltm1p1mod  9528  expnbnd  9763  nn0opthlem2d  9815  remim  9966  remullem  9977  caucvgrelemcau  10085  caucvgre  10086  cvg1nlemcxze  10087  cvg1nlemcau  10089  cvg1nlemres  10090  recvguniqlem  10099  resqrexlem1arp  10110  resqrexlemp1rp  10111  resqrexlemf1  10113  resqrexlemfp1  10114  resqrexlemover  10115  resqrexlemdec  10116  resqrexlemlo  10118  resqrexlemcalc1  10119  resqrexlemcalc2  10120  resqrexlemnm  10123  resqrexlemcvg  10124  resqrexlemoverl  10126  resqrexlemglsq  10127  resqrexlemga  10128  abs00ap  10167  absext  10168  absrele  10188  abstri  10209  abs3lem  10216  amgm2  10223  qdenre  10307  maxabsle  10309  maxabslemlub  10312  maxabslemval  10313  maxcl  10315  maxltsup  10323  mulcn2  10370  ltoddhalfle  10518  divalglemnqt  10545  zssinfcl  10569  qdencn  11070
  Copyright terms: Public domain W3C validator