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

 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 7007 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3syl2anc 391 1 (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1393  (class class class)co 5512  ℝcr 6888   + caddc 6892 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addrcl 6981 This theorem is referenced by:  ltadd2  7416  leadd1  7425  le2add  7439  lt2add  7440  lesub2  7452  ltsub2  7454  gt0add  7564  reapadd1  7587  apadd1  7599  mulext1  7603  recexaplem2  7633  recp1lt1  7865  cju  7913  peano5nni  7917  peano2nn  7926  div4p1lem1div2  8177  peano2z  8281  qbtwnzlemstep  9103  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2z  9109  qbtwnrelemcalc  9110  flqaddz  9139  btwnzge0  9142  2tnp1ge0ge0  9143  flhalf  9144  expnbnd  9372  remim  9460  remullem  9471  caucvgrelemcau  9579  caucvgre  9580  cvg1nlemcxze  9581  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniqlem  9592  resqrexlem1arp  9603  resqrexlemp1rp  9604  resqrexlemf1  9606  resqrexlemfp1  9607  resqrexlemover  9608  resqrexlemdec  9609  resqrexlemlo  9611  resqrexlemcalc1  9612  resqrexlemcalc2  9613  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemga  9621  abs00ap  9660  absext  9661  absrele  9679  abstri  9700  abs3lem  9707  amgm2  9714  qdenre  9798  mulcn2  9833  qdencn  10124
 Copyright terms: Public domain W3C validator