Theorem 8re 8942

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 8922	. 2 ⊢ 8 = (7 + 1)
2		7re 8940	. . 3 ⊢ 7 ∈ ℝ
3		1re 7898	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7912	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2239	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2136  (class class class)co 5842  ℝcr 7752  1c1 7754   + caddc 7756  7c7 8913  8c8 8914

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1re 7847  ax-addrcl 7850

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161  df-2 8916  df-3 8917  df-4 8918  df-5 8919  df-6 8920  df-7 8921  df-8 8922

This theorem is referenced by:  8cn  8943  9re  8944  9pos  8961  6lt8  9048  5lt8  9049  4lt8  9050  3lt8  9051  2lt8  9052  1lt8  9053  8lt9  9054  7lt9  9055  8th4div3  9076  8lt10  9453  7lt10  9454  ef01bndlem  11697  cos2bnd  11701