Theorem 9re 9009

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 8988	. 2 ⊢ 9 = (8 + 1)
2		8re 9007	. . 3 ⊢ 8 ∈ ℝ
3		1re 7959	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7973	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2250	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2148  (class class class)co 5878  ℝcr 7813  1c1 7815   + caddc 7817  8c8 8979  9c9 8980

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7908  ax-addrcl 7911

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8981  df-3 8982  df-4 8983  df-5 8984  df-6 8985  df-7 8986  df-8 8987  df-9 8988

This theorem is referenced by:  9cn  9010  7lt9  9120  6lt9  9121  5lt9  9122  4lt9  9123  3lt9  9124  2lt9  9125  1lt9  9126  9lt10  9517  8lt10  9518  0.999...  11532  cos2bnd  11771  sincos2sgn  11776  slotsdifplendx  12671  dsndxntsetndx  12681  unifndxntsetndx  12688  cnfldstr  13631  setsmsdsg  14168  2logb9irr  14577  2logb9irrap  14583