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

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

Proof of Theorem 6re
StepHypRef Expression
1 df-6 8169 . 2  |-  6  =  ( 5  +  1 )
2 5re 8185 . . 3  |-  5  e.  RR
3 1re 7180 . . 3  |-  1  e.  RR
42, 3readdcli 7194 . 2  |-  ( 5  +  1 )  e.  RR
51, 4eqeltri 2152 1  |-  6  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1434  (class class class)co 5543   RRcr 7042   1c1 7044    + caddc 7046   5c5 8159   6c6 8160
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064  ax-1re 7132  ax-addrcl 7135
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078  df-2 8165  df-3 8166  df-4 8167  df-5 8168  df-6 8169
This theorem is referenced by:  6cn  8188  7re  8189  7pos  8208  4lt6  8279  3lt6  8280  2lt6  8281  1lt6  8282  6lt7  8283  5lt7  8284  6lt8  8290  5lt8  8291  6lt9  8298  5lt9  8299  8th4div3  8317  halfpm6th  8318  div4p1lem1div2  8351  6lt10  8691  5lt10  8692
  Copyright terms: Public domain W3C validator