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

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 8775 . 2 5 = (4 + 1)
2 4re 8790 . . 3 4 ∈ ℝ
3 1re 7758 . . 3 1 ∈ ℝ
42, 3readdcli 7772 . 2 (4 + 1) ∈ ℝ
51, 4eqeltri 2210 1 5 ∈ ℝ
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1480  (class class class)co 5767  ℝcr 7612  1c1 7614   + caddc 7616  4c4 8766  5c5 8767 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119  ax-1re 7707  ax-addrcl 7710 This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133  df-2 8772  df-3 8773  df-4 8774  df-5 8775 This theorem is referenced by:  5cn  8793  6re  8794  6pos  8814  3lt5  8889  2lt5  8890  1lt5  8891  5lt6  8892  4lt6  8893  5lt7  8898  4lt7  8899  5lt8  8905  4lt8  8906  5lt9  8913  4lt9  8914  5lt10  9309  4lt10  9310  5recm6rec  9318  ef01bndlem  11452
 Copyright terms: Public domain W3C validator