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

Theorem 5re 8657
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 8640 . 2  |-  5  =  ( 4  +  1 )
2 4re 8655 . . 3  |-  4  e.  RR
3 1re 7637 . . 3  |-  1  e.  RR
42, 3readdcli 7651 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2172 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1448  (class class class)co 5706   RRcr 7499   1c1 7501    + caddc 7503   4c4 8631   5c5 8632
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082  ax-1re 7589  ax-addrcl 7592
This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096  df-2 8637  df-3 8638  df-4 8639  df-5 8640
This theorem is referenced by:  5cn  8658  6re  8659  6pos  8679  3lt5  8748  2lt5  8749  1lt5  8750  5lt6  8751  4lt6  8752  5lt7  8757  4lt7  8758  5lt8  8764  4lt8  8765  5lt9  8772  4lt9  8773  5lt10  9168  4lt10  9169  ef01bndlem  11261
  Copyright terms: Public domain W3C validator