Theorem 9re 8899

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 8878	. 2 |- 9 = ( 8 + 1 )
2		8re 8897	. . 3 |- 8 e. RR
3		1re 7856	. . 3 |- 1 e. RR
4	2, 3	readdcli 7870	. 2 |- ( 8 + 1 ) e. RR
5	1, 4	eqeltri 2227	1 |- 9 e. RR

Syntax hints:   e. wcel 2125  (class class class)co 5814   RRcr 7710   1c1 7712   + caddc 7714   8c8 8869   9c9 8870

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511  ax-ext 2136  ax-1re 7805  ax-addrcl 7808

This theorem depends on definitions:  df-bi 116  df-cleq 2147  df-clel 2150  df-2 8871  df-3 8872  df-4 8873  df-5 8874  df-6 8875  df-7 8876  df-8 8877  df-9 8878

This theorem is referenced by:  9cn  8900  7lt9  9010  6lt9  9011  5lt9  9012  4lt9  9013  3lt9  9014  2lt9  9015  1lt9  9016  9lt10  9404  8lt10  9405  0.999...  11395  cos2bnd  11634  sincos2sgn  11639  setsmsdsg  12827  2logb9irr  13235  2logb9irrap  13241