Theorem 9re 9208

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 9187	. 2 |- 9 = ( 8 + 1 )
2		8re 9206	. . 3 |- 8 e. RR
3		1re 8156	. . 3 |- 1 e. RR
4	2, 3	readdcli 8170	. 2 |- ( 8 + 1 ) e. RR
5	1, 4	eqeltri 2302	1 |- 9 e. RR

Syntax hints:   e. wcel 2200  (class class class)co 6007   RRcr 8009   1c1 8011   + caddc 8013   8c8 9178   9c9 9179

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1re 8104  ax-addrcl 8107

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-2 9180  df-3 9181  df-4 9182  df-5 9183  df-6 9184  df-7 9185  df-8 9186  df-9 9187

This theorem is referenced by:  9cn  9209  7lt9  9320  6lt9  9321  5lt9  9322  4lt9  9323  3lt9  9324  2lt9  9325  1lt9  9326  9lt10  9719  8lt10  9720  0.999...  12048  cos2bnd  12287  sincos2sgn  12293  slotsdifplendx  13259  dsndxntsetndx  13273  unifndxntsetndx  13280  setsmsdsg  15170  2logb9irr  15661  2logb9irrap  15667