Theorem 9re 9289

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

Syntax hints:   ∈ wcel 2202  (class class class)co 6028  ℝcr 8091  1c1 8093   + caddc 8095  8c8 9259  9c9 9260

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 8186  ax-addrcl 8189

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9261  df-3 9262  df-4 9263  df-5 9264  df-6 9265  df-7 9266  df-8 9267  df-9 9268

This theorem is referenced by:  9cn  9290  7lt9  9401  6lt9  9402  5lt9  9403  4lt9  9404  3lt9  9405  2lt9  9406  1lt9  9407  9lt10  9802  8lt10  9803  0.999...  12162  cos2bnd  12401  sincos2sgn  12407  slotsdifplendx  13373  dsndxntsetndx  13387  unifndxntsetndx  13394  setsmsdsg  15291  2logb9irr  15782  2logb9irrap  15788