Theorem 8re 9218

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 9198	. 2 ⊢ 8 = (7 + 1)
2		7re 9216	. . 3 ⊢ 7 ∈ ℝ
3		1re 8168	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8182	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2302	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2200  (class class class)co 6013  ℝcr 8021  1c1 8023   + caddc 8025  7c7 9189  8c8 9190

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1re 8116  ax-addrcl 8119

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-2 9192  df-3 9193  df-4 9194  df-5 9195  df-6 9196  df-7 9197  df-8 9198

This theorem is referenced by:  8cn  9219  9re  9220  9pos  9237  6lt8  9325  5lt8  9326  4lt8  9327  3lt8  9328  2lt8  9329  1lt8  9330  8lt9  9331  7lt9  9332  8th4div3  9353  8lt10  9732  7lt10  9733  ef01bndlem  12307  cos2bnd  12311  slotstnscsi  13268  slotsdnscsi  13296  2lgsoddprmlem1  15824  2lgsoddprmlem2  15825  2lgsoddprmlem3a  15826  2lgsoddprmlem3b  15827  2lgsoddprmlem3c  15828  2lgsoddprmlem3d  15829