Theorem 9re 12285

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 12256	. 2 ⊢ 9 = (8 + 1)
2		8re 12282	. . 3 ⊢ 8 ∈ ℝ
3		1re 11174	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11189	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067  1c1 11069   + caddc 11071  8c8 12247  9c9 12248

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255  df-9 12256

This theorem is referenced by:  7lt9  12381  6lt9  12382  5lt9  12383  4lt9  12384  3lt9  12385  2lt9  12386  1lt9  12387  10re  12668  9lt10  12780  8lt10  12781  0.999...  15847  cos2bnd  16156  sincos2sgn  16162  slotsdifplendx  17338  dsndxntsetndx  17356  unifndxntsetndx  17363  2logb9irr  26705  sqrt2cxp2logb9e3  26709  log2tlbnd  26855  bposlem4  27198  bposlem5  27199  bposlem7  27201  bposlem8  27202  bposlem9  27203  ex-fv  30372  dp2lt10  32804  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  problem5  35656  60gcd7e1  41993  lcmineqlem23  42039  3lexlogpow5ineq1  42042  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1lem1  42050  aks4d1p1  42064  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  9rp  42292  31prm  47598  2exp340mod341  47734  341fppr2  47735  9fppr8  47738  nfermltl8rev  47743  nfermltl2rev  47744  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem1  47806  ackval42  48685