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

Theorem 5re 8984
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 8967 . 2  |-  5  =  ( 4  +  1 )
2 4re 8982 . . 3  |-  4  e.  RR
3 1re 7944 . . 3  |-  1  e.  RR
42, 3readdcli 7958 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2250 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 2148  (class class class)co 5869   RRcr 7798   1c1 7800    + caddc 7802   4c4 8958   5c5 8959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7893  ax-addrcl 7896
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8964  df-3 8965  df-4 8966  df-5 8967
This theorem is referenced by:  5cn  8985  6re  8986  6pos  9006  3lt5  9081  2lt5  9082  1lt5  9083  5lt6  9084  4lt6  9085  5lt7  9090  4lt7  9091  5lt8  9097  4lt8  9098  5lt9  9105  4lt9  9106  5lt10  9504  4lt10  9505  5recm6rec  9513  ef01bndlem  11745  slotstnscsi  12614  slotsdnscsi  12630  lgsdir2lem1  14089
  Copyright terms: Public domain W3C validator