Theorem 8re 9270

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 9250	. 2 ⊢ 8 = (7 + 1)
2		7re 9268	. . 3 ⊢ 7 ∈ ℝ
3		1re 8221	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8235	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2304	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6028  ℝcr 8074  1c1 8076   + caddc 8078  7c7 9241  8c8 9242

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9244  df-3 9245  df-4 9246  df-5 9247  df-6 9248  df-7 9249  df-8 9250

This theorem is referenced by:  8cn  9271  9re  9272  9pos  9289  6lt8  9377  5lt8  9378  4lt8  9379  3lt8  9380  2lt8  9381  1lt8  9382  8lt9  9383  7lt9  9384  8th4div3  9405  8lt10  9786  7lt10  9787  ef01bndlem  12380  cos2bnd  12384  slotstnscsi  13341  slotsdnscsi  13369  2lgsoddprmlem1  15907  2lgsoddprmlem2  15908  2lgsoddprmlem3a  15909  2lgsoddprmlem3b  15910  2lgsoddprmlem3c  15911  2lgsoddprmlem3d  15912