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

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

Proof of Theorem 8re
StepHypRef Expression
1 df-8 8742 . 2 8 = (7 + 1)
2 7re 8760 . . 3 7 ∈ ℝ
3 1re 7729 . . 3 1 ∈ ℝ
42, 3readdcli 7743 . 2 (7 + 1) ∈ ℝ
51, 4eqeltri 2188 1 8 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1463  (class class class)co 5740  cr 7583  1c1 7585   + caddc 7587  7c7 8733  8c8 8734
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097  ax-1re 7678  ax-addrcl 7681
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111  df-2 8736  df-3 8737  df-4 8738  df-5 8739  df-6 8740  df-7 8741  df-8 8742
This theorem is referenced by:  8cn  8763  9re  8764  9pos  8781  6lt8  8862  5lt8  8863  4lt8  8864  3lt8  8865  2lt8  8866  1lt8  8867  8lt9  8868  7lt9  8869  8th4div3  8890  8lt10  9264  7lt10  9265  ef01bndlem  11362  cos2bnd  11366
  Copyright terms: Public domain W3C validator