Theorem 8re 9120

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 9100	. 2 ⊢ 8 = (7 + 1)
2		7re 9118	. . 3 ⊢ 7 ∈ ℝ
3		1re 8070	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8084	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2277	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2175  (class class class)co 5943  ℝcr 7923  1c1 7925   + caddc 7927  7c7 9091  8c8 9092

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200  df-2 9094  df-3 9095  df-4 9096  df-5 9097  df-6 9098  df-7 9099  df-8 9100

This theorem is referenced by:  8cn  9121  9re  9122  9pos  9139  6lt8  9227  5lt8  9228  4lt8  9229  3lt8  9230  2lt8  9231  1lt8  9232  8lt9  9233  7lt9  9234  8th4div3  9255  8lt10  9634  7lt10  9635  ef01bndlem  12038  cos2bnd  12042  slotstnscsi  12998  slotsdnscsi  13026  2lgsoddprmlem1  15553  2lgsoddprmlem2  15554  2lgsoddprmlem3a  15555  2lgsoddprmlem3b  15556  2lgsoddprmlem3c  15557  2lgsoddprmlem3d  15558