Theorem 9re 9273

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

Assertion

Ref	Expression
9re	|- 9 e. RR

Proof of Theorem 9re

Step	Hyp	Ref	Expression
1		df-9 9252	. 2 |- 9 = ( 8 + 1 )
2		8re 9271	. . 3 |- 8 e. RR
3		1re 8221	. . 3 |- 1 e. RR
4	2, 3	readdcli 8235	. 2 |- ( 8 + 1 ) e. RR
5	1, 4	eqeltri 2304	1 |- 9 e. RR

Syntax hints:   e. wcel 2202  (class class class)co 6028   RRcr 8074   1c1 8076   + caddc 8078   8c8 9243   9c9 9244

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 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9245  df-3 9246  df-4 9247  df-5 9248  df-6 9249  df-7 9250  df-8 9251  df-9 9252

This theorem is referenced by:  9cn  9274  7lt9  9385  6lt9  9386  5lt9  9387  4lt9  9388  3lt9  9389  2lt9  9390  1lt9  9391  9lt10  9786  8lt10  9787  0.999...  12145  cos2bnd  12384  sincos2sgn  12390  slotsdifplendx  13356  dsndxntsetndx  13370  unifndxntsetndx  13377  setsmsdsg  15274  2logb9irr  15765  2logb9irrap  15771