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

Theorem 4re 8066
Description: The number 4 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
4re 4 ∈ ℝ

Proof of Theorem 4re
StepHypRef Expression
1 df-4 8050 . 2 4 = (3 + 1)
2 3re 8063 . . 3 3 ∈ ℝ
3 1re 7083 . . 3 1 ∈ ℝ
42, 3readdcli 7097 . 2 (3 + 1) ∈ ℝ
51, 4eqeltri 2126 1 4 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1409  (class class class)co 5539  cr 6945  1c1 6947   + caddc 6949  3c3 8040  4c4 8041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038  ax-1re 7035  ax-addrcl 7038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052  df-2 8048  df-3 8049  df-4 8050
This theorem is referenced by:  4cn  8067  5re  8068  4ne0  8087  4ap0  8088  5pos  8089  2lt4  8155  1lt4  8156  4lt5  8157  3lt5  8158  2lt5  8159  1lt5  8160  4lt6  8162  3lt6  8163  4lt7  8168  3lt7  8169  4lt8  8175  3lt8  8176  4lt9  8183  3lt9  8184  8th4div3  8200  div4p1lem1div2  8234  4lt10  8561  3lt10  8562  fzo0to42pr  9177  fldiv4p1lem1div2  9254  faclbnd2  9609  4bc2eq6  9641  resqrexlemover  9836  resqrexlemcalc1  9840  resqrexlemcalc2  9841  resqrexlemcalc3  9842  resqrexlemnm  9844  resqrexlemga  9849  sqrt2gt1lt2  9875  amgm2  9944
  Copyright terms: Public domain W3C validator