Theorem 9re 8921

Description: The number 9 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
9re	⊢ 9 ∈ ℝ

Proof of Theorem 9re

Step	Hyp	Ref	Expression
1		df-9 8900	. 2 ⊢ 9 = (8 + 1)
2		8re 8919	. . 3 ⊢ 8 ∈ ℝ
3		1re 7878	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7892	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2230	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2128  (class class class)co 5825  ℝcr 7732  1c1 7734   + caddc 7736  8c8 8891  9c9 8892

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139  ax-1re 7827  ax-addrcl 7830

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153  df-2 8893  df-3 8894  df-4 8895  df-5 8896  df-6 8897  df-7 8898  df-8 8899  df-9 8900

This theorem is referenced by:  9cn  8922  7lt9  9032  6lt9  9033  5lt9  9034  4lt9  9035  3lt9  9036  2lt9  9037  1lt9  9038  9lt10  9426  8lt10  9427  0.999...  11422  cos2bnd  11661  sincos2sgn  11666  setsmsdsg  12922  2logb9irr  13330  2logb9irrap  13336