Theorem 9re 12340

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 12310	. 2 ⊢ 9 = (8 + 1)
2		8re 12337	. . 3 ⊢ 8 ∈ ℝ
3		1re 11208	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11224	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2865	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℝcr 11099  1c1 11101   + caddc 11103  8c8 12301  9c9 12302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-i2m1 11168  ax-1ne0 11169  ax-rrecex 11172  ax-cnre 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308  df-8 12309  df-9 12310

This theorem is referenced by:  7lt9  12443  6lt9  12444  5lt9  12445  4lt9  12446  3lt9  12447  2lt9  12448  1lt9  12449  10re  12734  9lt10  12848  8lt10  12849  7lt10  12850  6lt10  12851  5lt10  12852  4lt10  12853  3lt10  12854  2lt10  12855  1lt10  12856  0.999...  15935  cos2bnd  16244  sincos2sgn  16250  slotsdifplendx  17428  dsndxntsetndx  17446  unifndxntsetndx  17453  2logb9irr  26926  sqrt2cxp2logb9e3  26930  log2tlbnd  27076  bposlem4  27417  bposlem5  27418  bposlem7  27420  bposlem8  27421  bposlem9  27422  ex-fv  30735  dp2lt10  33144  hgt750lem  34983  hgt750lem2  34984  hgt750leme  34990  problem5  36094  60gcd7e1  42696  lcmineqlem23  42742  3lexlogpow5ineq1  42745  3lexlogpow5ineq2  42746  3lexlogpow5ineq4  42747  3lexlogpow5ineq3  42748  3lexlogpow2ineq2  42750  3lexlogpow5ineq5  42751  aks4d1lem1  42753  aks4d1p1  42767  aks4d1p6  42772  aks4d1p7d1  42773  aks4d1p7  42774  aks4d1p8  42778  9rp  42989  31prm  48272  2exp340mod341  48421  341fppr2  48422  9fppr8  48425  nfermltl8rev  48430  nfermltl2rev  48431  wtgoldbnnsum4prm  48490  bgoldbnnsum3prm  48492  bgoldbtbndlem1  48493  ackval42  49395