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

Theorem 7re 9001
Description: The number 7 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
7re 7 ∈ ℝ

Proof of Theorem 7re
StepHypRef Expression
1 df-7 8982 . 2 7 = (6 + 1)
2 6re 8999 . . 3 6 ∈ ℝ
3 1re 7955 . . 3 1 ∈ ℝ
42, 3readdcli 7969 . 2 (6 + 1) ∈ ℝ
51, 4eqeltri 2250 1 7 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 2148  (class class class)co 5874  cr 7809  1c1 7811   + caddc 7813  6c6 8973  7c7 8974
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 7904  ax-addrcl 7907
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8977  df-3 8978  df-4 8979  df-5 8980  df-6 8981  df-7 8982
This theorem is referenced by:  7cn  9002  8re  9003  8pos  9021  5lt7  9103  4lt7  9104  3lt7  9105  2lt7  9106  1lt7  9107  7lt8  9108  6lt8  9109  7lt9  9116  6lt9  9117  7lt10  9515  6lt10  9516  lgsdir2lem1  14399
  Copyright terms: Public domain W3C validator