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

Theorem 8re 8849
 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 8829 . 2 8 = (7 + 1)
2 7re 8847 . . 3 7 ∈ ℝ
3 1re 7809 . . 3 1 ∈ ℝ
42, 3readdcli 7823 . 2 (7 + 1) ∈ ℝ
51, 4eqeltri 2213 1 8 ∈ ℝ
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1481  (class class class)co 5783  ℝcr 7663  1c1 7665   + caddc 7667  7c7 8820  8c8 8821 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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122  ax-1re 7758  ax-addrcl 7761 This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136  df-2 8823  df-3 8824  df-4 8825  df-5 8826  df-6 8827  df-7 8828  df-8 8829 This theorem is referenced by:  8cn  8850  9re  8851  9pos  8868  6lt8  8955  5lt8  8956  4lt8  8957  3lt8  8958  2lt8  8959  1lt8  8960  8lt9  8961  7lt9  8962  8th4div3  8983  8lt10  9357  7lt10  9358  ef01bndlem  11519  cos2bnd  11523
 Copyright terms: Public domain W3C validator