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

Theorem 5re 8767
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 8750 . 2  |-  5  =  ( 4  +  1 )
2 4re 8765 . . 3  |-  4  e.  RR
3 1re 7733 . . 3  |-  1  e.  RR
42, 3readdcli 7747 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2190 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1465  (class class class)co 5742   RRcr 7587   1c1 7589    + caddc 7591   4c4 8741   5c5 8742
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099  ax-1re 7682  ax-addrcl 7685
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113  df-2 8747  df-3 8748  df-4 8749  df-5 8750
This theorem is referenced by:  5cn  8768  6re  8769  6pos  8789  3lt5  8864  2lt5  8865  1lt5  8866  5lt6  8867  4lt6  8868  5lt7  8873  4lt7  8874  5lt8  8880  4lt8  8881  5lt9  8888  4lt9  8889  5lt10  9284  4lt10  9285  5recm6rec  9293  ef01bndlem  11390
  Copyright terms: Public domain W3C validator