Theorem 9re 9230

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 9209	. 2 |- 9 = ( 8 + 1 )
2		8re 9228	. . 3 |- 8 e. RR
3		1re 8178	. . 3 |- 1 e. RR
4	2, 3	readdcli 8192	. 2 |- ( 8 + 1 ) e. RR
5	1, 4	eqeltri 2304	1 |- 9 e. RR

Syntax hints:   e. wcel 2202  (class class class)co 6018   RRcr 8031   1c1 8033   + caddc 8035   8c8 9200   9c9 9201

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 8126  ax-addrcl 8129

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

This theorem is referenced by:  9cn  9231  7lt9  9342  6lt9  9343  5lt9  9344  4lt9  9345  3lt9  9346  2lt9  9347  1lt9  9348  9lt10  9741  8lt10  9742  0.999...  12100  cos2bnd  12339  sincos2sgn  12345  slotsdifplendx  13311  dsndxntsetndx  13325  unifndxntsetndx  13332  setsmsdsg  15223  2logb9irr  15714  2logb9irrap  15720