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

Theorem 5re 8811
Description: The number 5 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
5re  |-  5  e.  RR

Proof of Theorem 5re
StepHypRef Expression
1 df-5 8794 . 2  |-  5  =  ( 4  +  1 )
2 4re 8809 . . 3  |-  4  e.  RR
3 1re 7777 . . 3  |-  1  e.  RR
42, 3readdcli 7791 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2212 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1480  (class class class)co 5774   RRcr 7631   1c1 7633    + caddc 7635   4c4 8785   5c5 8786
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 2121  ax-1re 7726  ax-addrcl 7729
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135  df-2 8791  df-3 8792  df-4 8793  df-5 8794
This theorem is referenced by:  5cn  8812  6re  8813  6pos  8833  3lt5  8908  2lt5  8909  1lt5  8910  5lt6  8911  4lt6  8912  5lt7  8917  4lt7  8918  5lt8  8924  4lt8  8925  5lt9  8932  4lt9  8933  5lt10  9328  4lt10  9329  5recm6rec  9337  ef01bndlem  11474
  Copyright terms: Public domain W3C validator