Theorem 8re 8798

Description: The number 8 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
8re	⊢ 8 ∈ ℝ

Proof of Theorem 8re

Step	Hyp	Ref	Expression
1		df-8 8778	. 2 ⊢ 8 = (7 + 1)
2		7re 8796	. . 3 ⊢ 7 ∈ ℝ
3		1re 7758	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7772	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2210	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 1480  (class class class)co 5767  ℝcr 7612  1c1 7614   + caddc 7616  7c7 8769  8c8 8770

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119  ax-1re 7707  ax-addrcl 7710

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133  df-2 8772  df-3 8773  df-4 8774  df-5 8775  df-6 8776  df-7 8777  df-8 8778

This theorem is referenced by:  8cn  8799  9re  8800  9pos  8817  6lt8  8904  5lt8  8905  4lt8  8906  3lt8  8907  2lt8  8908  1lt8  8909  8lt9  8910  7lt9  8911  8th4div3  8932  8lt10  9306  7lt10  9307  ef01bndlem  11452  cos2bnd  11456