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

Theorem 5re 9012
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 8995 . 2  |-  5  =  ( 4  +  1 )
2 4re 9010 . . 3  |-  4  e.  RR
3 1re 7970 . . 3  |-  1  e.  RR
42, 3readdcli 7984 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2260 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 2158  (class class class)co 5888   RRcr 7824   1c1 7826    + caddc 7828   4c4 8986   5c5 8987
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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169  ax-1re 7919  ax-addrcl 7922
This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183  df-2 8992  df-3 8993  df-4 8994  df-5 8995
This theorem is referenced by:  5cn  9013  6re  9014  6pos  9034  3lt5  9109  2lt5  9110  1lt5  9111  5lt6  9112  4lt6  9113  5lt7  9118  4lt7  9119  5lt8  9125  4lt8  9126  5lt9  9133  4lt9  9134  5lt10  9532  4lt10  9533  5recm6rec  9541  ef01bndlem  11778  vscandxnscandx  12635  slotsdifipndx  12648  slotstnscsi  12668  plendxnscandx  12681  slotsdnscsi  12692  lgsdir2lem1  14725
  Copyright terms: Public domain W3C validator