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

Theorem 7re 9002
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 8983 . 2 7 = (6 + 1)
2 6re 9000 . . 3 6 ∈ ℝ
3 1re 7956 . . 3 1 ∈ ℝ
42, 3readdcli 7970 . 2 (6 + 1) ∈ ℝ
51, 4eqeltri 2250 1 7 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 2148  (class class class)co 5875  cr 7810  1c1 7812   + caddc 7814  6c6 8974  7c7 8975
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 7905  ax-addrcl 7908
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8978  df-3 8979  df-4 8980  df-5 8981  df-6 8982  df-7 8983
This theorem is referenced by:  7cn  9003  8re  9004  8pos  9022  5lt7  9104  4lt7  9105  3lt7  9106  2lt7  9107  1lt7  9108  7lt8  9109  6lt8  9110  7lt9  9117  6lt9  9118  7lt10  9516  6lt10  9517  lgsdir2lem1  14432
  Copyright terms: Public domain W3C validator