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

Theorem 8re 8980
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 8960 . 2 8 = (7 + 1)
2 7re 8978 . . 3 7 ∈ ℝ
3 1re 7934 . . 3 1 ∈ ℝ
42, 3readdcli 7948 . 2 (7 + 1) ∈ ℝ
51, 4eqeltri 2250 1 8 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 2148  (class class class)co 5868  cr 7788  1c1 7790   + caddc 7792  7c7 8951  8c8 8952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7883  ax-addrcl 7886
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8954  df-3 8955  df-4 8956  df-5 8957  df-6 8958  df-7 8959  df-8 8960
This theorem is referenced by:  8cn  8981  9re  8982  9pos  8999  6lt8  9086  5lt8  9087  4lt8  9088  3lt8  9089  2lt8  9090  1lt8  9091  8lt9  9092  7lt9  9093  8th4div3  9114  8lt10  9491  7lt10  9492  ef01bndlem  11735  cos2bnd  11739  slotstnscsi  12604  slotsdnscsi  12620
  Copyright terms: Public domain W3C validator