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

Theorem 7re 8948
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 8929 . 2 7 = (6 + 1)
2 6re 8946 . . 3 6 ∈ ℝ
3 1re 7906 . . 3 1 ∈ ℝ
42, 3readdcli 7920 . 2 (6 + 1) ∈ ℝ
51, 4eqeltri 2243 1 7 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 2141  (class class class)co 5850  cr 7760  1c1 7762   + caddc 7764  6c6 8920  7c7 8921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1re 7855  ax-addrcl 7858
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166  df-2 8924  df-3 8925  df-4 8926  df-5 8927  df-6 8928  df-7 8929
This theorem is referenced by:  7cn  8949  8re  8950  8pos  8968  5lt7  9050  4lt7  9051  3lt7  9052  2lt7  9053  1lt7  9054  7lt8  9055  6lt8  9056  7lt9  9063  6lt9  9064  7lt10  9462  6lt10  9463  lgsdir2lem1  13682
  Copyright terms: Public domain W3C validator