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

Theorem 4re 7992
 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 7975 . 2 4 = (3 + 1)
2 3re 7989 . . 3 3 ∈ ℝ
3 1re 7026 . . 3 1 ∈ ℝ
42, 3readdcli 7040 . 2 (3 + 1) ∈ ℝ
51, 4eqeltri 2110 1 4 ∈ ℝ
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1393  (class class class)co 5512  ℝcr 6888  1c1 6890   + caddc 6892  3c3 7965  4c4 7966 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022  ax-1re 6978  ax-addrcl 6981 This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-2 7973  df-3 7974  df-4 7975 This theorem is referenced by:  4cn  7993  5re  7994  4ne0  8014  4ap0  8015  5pos  8016  2lt4  8090  1lt4  8091  4lt5  8092  3lt5  8093  2lt5  8094  1lt5  8095  4lt6  8097  3lt6  8098  4lt7  8103  3lt7  8104  4lt8  8110  3lt8  8111  4lt9  8118  3lt9  8119  4lt10  8127  3lt10  8128  8th4div3  8144  div4p1lem1div2  8177  fzo0to42pr  9076  fldiv4p1lem1div2  9147  resqrexlemover  9608  resqrexlemcalc1  9612  resqrexlemcalc2  9613  resqrexlemcalc3  9614  resqrexlemnm  9616  resqrexlemga  9621  sqrt2gt1lt2  9647  amgm2  9714
 Copyright terms: Public domain W3C validator