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

Theorem 8re 8773
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 8753 . 2 8 = (7 + 1)
2 7re 8771 . . 3 7 ∈ ℝ
3 1re 7733 . . 3 1 ∈ ℝ
42, 3readdcli 7747 . 2 (7 + 1) ∈ ℝ
51, 4eqeltri 2190 1 8 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1465  (class class class)co 5742  cr 7587  1c1 7589   + caddc 7591  7c7 8744  8c8 8745
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099  ax-1re 7682  ax-addrcl 7685
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113  df-2 8747  df-3 8748  df-4 8749  df-5 8750  df-6 8751  df-7 8752  df-8 8753
This theorem is referenced by:  8cn  8774  9re  8775  9pos  8792  6lt8  8879  5lt8  8880  4lt8  8881  3lt8  8882  2lt8  8883  1lt8  8884  8lt9  8885  7lt9  8886  8th4div3  8907  8lt10  9281  7lt10  9282  ef01bndlem  11390  cos2bnd  11394
  Copyright terms: Public domain W3C validator