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

Theorem readdcld 7114
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 7065 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3syl2anc 397 1 (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  (class class class)co 5540  cr 6946   + caddc 6950
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105  ax-addrcl 7039
This theorem is referenced by:  ltadd2  7488  leadd1  7499  le2add  7513  lt2add  7514  lesub2  7526  ltsub2  7528  gt0add  7638  reapadd1  7661  apadd1  7673  mulext1  7677  recexaplem2  7707  recp1lt1  7940  cju  7989  peano5nni  7993  peano2nn  8002  div4p1lem1div2  8235  peano2z  8338  addlelt  8786  zltaddlt1le  8975  qbtwnzlemstep  9205  qbtwnz  9208  rebtwn2zlemstep  9209  rebtwn2z  9211  qbtwnrelemcalc  9212  flqaddz  9247  btwnzge0  9250  2tnp1ge0ge0  9251  flhalf  9252  modqltm1p1mod  9326  expnbnd  9540  nn0opthlem2d  9589  remim  9688  remullem  9699  caucvgrelemcau  9807  caucvgre  9808  cvg1nlemcxze  9809  cvg1nlemcau  9811  cvg1nlemres  9812  recvguniqlem  9821  resqrexlem1arp  9832  resqrexlemp1rp  9833  resqrexlemf1  9835  resqrexlemfp1  9836  resqrexlemover  9837  resqrexlemdec  9838  resqrexlemlo  9840  resqrexlemcalc1  9841  resqrexlemcalc2  9842  resqrexlemnm  9845  resqrexlemcvg  9846  resqrexlemoverl  9848  resqrexlemglsq  9849  resqrexlemga  9850  abs00ap  9889  absext  9890  absrele  9910  abstri  9931  abs3lem  9938  amgm2  9945  qdenre  10029  mulcn2  10064  ltoddhalfle  10205  divalglemnqt  10232  qdencn  10511
  Copyright terms: Public domain W3C validator