Theorem 9re 9229

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 9208	. 2 |- 9 = ( 8 + 1 )
2		8re 9227	. . 3 |- 8 e. RR
3		1re 8177	. . 3 |- 1 e. RR
4	2, 3	readdcli 8191	. 2 |- ( 8 + 1 ) e. RR
5	1, 4	eqeltri 2304	1 |- 9 e. RR

Syntax hints:   e. wcel 2202  (class class class)co 6017   RRcr 8030   1c1 8032   + caddc 8034   8c8 9199   9c9 9200

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1re 8125  ax-addrcl 8128

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9201  df-3 9202  df-4 9203  df-5 9204  df-6 9205  df-7 9206  df-8 9207  df-9 9208

This theorem is referenced by:  9cn  9230  7lt9  9341  6lt9  9342  5lt9  9343  4lt9  9344  3lt9  9345  2lt9  9346  1lt9  9347  9lt10  9740  8lt10  9741  0.999...  12081  cos2bnd  12320  sincos2sgn  12326  slotsdifplendx  13292  dsndxntsetndx  13306  unifndxntsetndx  13313  setsmsdsg  15203  2logb9irr  15694  2logb9irrap  15700