Theorem 8re 9035

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 9015	. 2 ⊢ 8 = (7 + 1)
2		7re 9033	. . 3 ⊢ 7 ∈ ℝ
3		1re 7987	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8001	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2262	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2160  (class class class)co 5897  ℝcr 7841  1c1 7843   + caddc 7845  7c7 9006  8c8 9007

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 2171  ax-1re 7936  ax-addrcl 7939

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185  df-2 9009  df-3 9010  df-4 9011  df-5 9012  df-6 9013  df-7 9014  df-8 9015

This theorem is referenced by:  8cn  9036  9re  9037  9pos  9054  6lt8  9141  5lt8  9142  4lt8  9143  3lt8  9144  2lt8  9145  1lt8  9146  8lt9  9147  7lt9  9148  8th4div3  9169  8lt10  9546  7lt10  9547  ef01bndlem  11799  cos2bnd  11803  slotstnscsi  12709  slotsdnscsi  12733  2lgsoddprmlem1  14931  2lgsoddprmlem2  14932  2lgsoddprmlem3a  14933  2lgsoddprmlem3b  14934  2lgsoddprmlem3c  14935  2lgsoddprmlem3d  14936