Theorem 9re 9125

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 9104	. 2 |- 9 = ( 8 + 1 )
2		8re 9123	. . 3 |- 8 e. RR
3		1re 8073	. . 3 |- 1 e. RR
4	2, 3	readdcli 8087	. 2 |- ( 8 + 1 ) e. RR
5	1, 4	eqeltri 2278	1 |- 9 e. RR

Syntax hints:   e. wcel 2176  (class class class)co 5946   RRcr 7926   1c1 7928   + caddc 7930   8c8 9095   9c9 9096

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187  ax-1re 8021  ax-addrcl 8024

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201  df-2 9097  df-3 9098  df-4 9099  df-5 9100  df-6 9101  df-7 9102  df-8 9103  df-9 9104

This theorem is referenced by:  9cn  9126  7lt9  9237  6lt9  9238  5lt9  9239  4lt9  9240  3lt9  9241  2lt9  9242  1lt9  9243  9lt10  9636  8lt10  9637  0.999...  11865  cos2bnd  12104  sincos2sgn  12110  slotsdifplendx  13075  dsndxntsetndx  13089  unifndxntsetndx  13096  setsmsdsg  14985  2logb9irr  15476  2logb9irrap  15482