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

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

Proof of Theorem 7re
StepHypRef Expression
1 df-7 8997 . 2  |-  7  =  ( 6  +  1 )
2 6re 9014 . . 3  |-  6  e.  RR
3 1re 7970 . . 3  |-  1  e.  RR
42, 3readdcli 7984 . 2  |-  ( 6  +  1 )  e.  RR
51, 4eqeltri 2260 1  |-  7  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 2158  (class class class)co 5888   RRcr 7824   1c1 7826    + caddc 7828   6c6 8988   7c7 8989
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  df-6 8996  df-7 8997
This theorem is referenced by:  7cn  9017  8re  9018  8pos  9036  5lt7  9118  4lt7  9119  3lt7  9120  2lt7  9121  1lt7  9122  7lt8  9123  6lt8  9124  7lt9  9131  6lt9  9132  7lt10  9530  6lt10  9531  lgsdir2lem1  14725
  Copyright terms: Public domain W3C validator