Theorem 9re 8944

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 8923	. 2 |- 9 = ( 8 + 1 )
2		8re 8942	. . 3 |- 8 e. RR
3		1re 7898	. . 3 |- 1 e. RR
4	2, 3	readdcli 7912	. 2 |- ( 8 + 1 ) e. RR
5	1, 4	eqeltri 2239	1 |- 9 e. RR

Syntax hints:   e. wcel 2136  (class class class)co 5842   RRcr 7752   1c1 7754   + caddc 7756   8c8 8914   9c9 8915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1re 7847  ax-addrcl 7850

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161  df-2 8916  df-3 8917  df-4 8918  df-5 8919  df-6 8920  df-7 8921  df-8 8922  df-9 8923

This theorem is referenced by:  9cn  8945  7lt9  9055  6lt9  9056  5lt9  9057  4lt9  9058  3lt9  9059  2lt9  9060  1lt9  9061  9lt10  9452  8lt10  9453  0.999...  11462  cos2bnd  11701  sincos2sgn  11706  setsmsdsg  13130  2logb9irr  13539  2logb9irrap  13545