Theorem 8re 9069

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 9049	. 2 ⊢ 8 = (7 + 1)
2		7re 9067	. . 3 ⊢ 7 ∈ ℝ
3		1re 8020	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8034	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2266	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2164  (class class class)co 5919  ℝcr 7873  1c1 7875   + caddc 7877  7c7 9040  8c8 9041

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1re 7968  ax-addrcl 7971

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189  df-2 9043  df-3 9044  df-4 9045  df-5 9046  df-6 9047  df-7 9048  df-8 9049

This theorem is referenced by:  8cn  9070  9re  9071  9pos  9088  6lt8  9176  5lt8  9177  4lt8  9178  3lt8  9179  2lt8  9180  1lt8  9181  8lt9  9182  7lt9  9183  8th4div3  9204  8lt10  9582  7lt10  9583  ef01bndlem  11902  cos2bnd  11906  slotstnscsi  12815  slotsdnscsi  12839  2lgsoddprmlem1  15262  2lgsoddprmlem2  15263  2lgsoddprmlem3a  15264  2lgsoddprmlem3b  15265  2lgsoddprmlem3c  15266  2lgsoddprmlem3d  15267