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

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

Proof of Theorem 3re
StepHypRef Expression
1 df-3 8020 . 2 3 = (2 + 1)
2 2re 8030 . . 3 2 ∈ ℝ
3 1re 7054 . . 3 1 ∈ ℝ
42, 3readdcli 7068 . 2 (2 + 1) ∈ ℝ
51, 4eqeltri 2124 1 3 ∈ ℝ
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1407  (class class class)co 5537  ℝcr 6916  1c1 6918   + caddc 6920  2c2 8010  3c3 8011 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 1350  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-4 1414  ax-17 1433  ax-ial 1441  ax-ext 2036  ax-1re 7006  ax-addrcl 7009 This theorem depends on definitions:  df-bi 114  df-cleq 2047  df-clel 2050  df-2 8019  df-3 8020 This theorem is referenced by:  3cn  8035  4re  8037  3ne0  8055  3ap0  8056  4pos  8057  1lt3  8124  3lt4  8125  2lt4  8126  3lt5  8129  3lt6  8134  2lt6  8135  3lt7  8140  2lt7  8141  3lt8  8147  2lt8  8148  3lt9  8155  2lt9  8156  1le3  8163  8th4div3  8171  halfpm6th  8172  3halfnz  8365  3lt10  8533  2lt10  8534  uzuzle23  8579  uz3m2nn  8581  nn01to3  8619  expnass  9488  sqrt9  9838  ex-fl  10222
 Copyright terms: Public domain W3C validator