Theorem 9re 9324

Description: The number 9 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
9re	⊢ 9 ∈ ℝ

Proof of Theorem 9re

Step	Hyp	Ref	Expression
1		df-9 9303	. 2 ⊢ 9 = (8 + 1)
2		8re 9322	. . 3 ⊢ 8 ∈ ℝ
3		1re 8273	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8287	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2305	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2203  (class class class)co 6050  ℝcr 8126  1c1 8128   + caddc 8130  8c8 9294  9c9 9295

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 2214  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228  df-2 9296  df-3 9297  df-4 9298  df-5 9299  df-6 9300  df-7 9301  df-8 9302  df-9 9303

This theorem is referenced by:  9cn  9325  7lt9  9436  6lt9  9437  5lt9  9438  4lt9  9439  3lt9  9440  2lt9  9441  1lt9  9442  9lt10  9839  8lt10  9840  0.999...  12207  cos2bnd  12446  sincos2sgn  12452  slotsdifplendx  13423  dsndxntsetndx  13437  unifndxntsetndx  13444  setsmsdsg  15345  2logb9irr  15836  2logb9irrap  15842