Theorem 9re 12337

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 12308	. 2 ⊢ 9 = (8 + 1)
2		8re 12334	. . 3 ⊢ 8 ∈ ℝ
3		1re 11233	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11248	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2830	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7403  ℝcr 11126  1c1 11128   + caddc 11130  8c8 12299  9c9 12300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305  df-7 12306  df-8 12307  df-9 12308

This theorem is referenced by:  7lt9  12438  6lt9  12439  5lt9  12440  4lt9  12441  3lt9  12442  2lt9  12443  1lt9  12444  10re  12725  9lt10  12837  8lt10  12838  0.999...  15895  cos2bnd  16204  sincos2sgn  16210  slotsdifplendx  17387  dsndxntsetndx  17405  unifndxntsetndx  17412  2logb9irr  26755  sqrt2cxp2logb9e3  26759  log2tlbnd  26905  bposlem4  27248  bposlem5  27249  bposlem7  27251  bposlem8  27252  bposlem9  27253  ex-fv  30370  dp2lt10  32804  hgt750lem  34629  hgt750lem2  34630  hgt750leme  34636  problem5  35637  60gcd7e1  41964  lcmineqlem23  42010  3lexlogpow5ineq1  42013  3lexlogpow5ineq2  42014  3lexlogpow5ineq4  42015  3lexlogpow5ineq3  42016  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1lem1  42021  aks4d1p1  42035  aks4d1p6  42040  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8  42046  9rp  42300  31prm  47559  2exp340mod341  47695  341fppr2  47696  9fppr8  47699  nfermltl8rev  47704  nfermltl2rev  47705  wtgoldbnnsum4prm  47764  bgoldbnnsum3prm  47766  bgoldbtbndlem1  47767  ackval42  48624