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

Theorem 8re 8505
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 8485 . 2 8 = (7 + 1)
2 7re 8503 . . 3 7 ∈ ℝ
3 1re 7485 . . 3 1 ∈ ℝ
42, 3readdcli 7499 . 2 (7 + 1) ∈ ℝ
51, 4eqeltri 2160 1 8 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1438  (class class class)co 5652  cr 7347  1c1 7349   + caddc 7351  7c7 8476  8c8 8477
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1re 7437  ax-addrcl 7440
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084  df-2 8479  df-3 8480  df-4 8481  df-5 8482  df-6 8483  df-7 8484  df-8 8485
This theorem is referenced by:  8cn  8506  9re  8507  9pos  8524  6lt8  8605  5lt8  8606  4lt8  8607  3lt8  8608  2lt8  8609  1lt8  8610  8lt9  8611  7lt9  8612  8th4div3  8633  8lt10  9006  7lt10  9007  ef01bndlem  11043  cos2bnd  11047
  Copyright terms: Public domain W3C validator