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

Theorem 3re 8467
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 8453 . 2 3 = (2 + 1)
2 2re 8463 . . 3 2 ∈ ℝ
3 1re 7466 . . 3 1 ∈ ℝ
42, 3readdcli 7480 . 2 (2 + 1) ∈ ℝ
51, 4eqeltri 2160 1 3 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1438  (class class class)co 5634  cr 7328  1c1 7330   + caddc 7332  2c2 8444  3c3 8445
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1re 7418  ax-addrcl 7421
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084  df-2 8452  df-3 8453
This theorem is referenced by:  3cn  8468  4re  8470  3ne0  8488  3ap0  8489  4pos  8490  1lt3  8557  3lt4  8558  2lt4  8559  3lt5  8562  3lt6  8567  2lt6  8568  3lt7  8573  2lt7  8574  3lt8  8580  2lt8  8581  3lt9  8588  2lt9  8589  1le3  8597  8th4div3  8605  halfpm6th  8606  3halfnz  8813  3lt10  8982  2lt10  8983  uzuzle23  9028  uz3m2nn  9030  nn01to3  9071  expnass  10024  sqrt9  10445  flodddiv4  11014  ex-fl  11296  ex-gcd  11302
  Copyright terms: Public domain W3C validator