Theorem 9re 12292

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 12263	. 2 ⊢ 9 = (8 + 1)
2		8re 12289	. . 3 ⊢ 8 ∈ ℝ
3		1re 11181	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11196	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2825	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℝcr 11074  1c1 11076   + caddc 11078  8c8 12254  9c9 12255

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 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262  df-9 12263

This theorem is referenced by:  7lt9  12388  6lt9  12389  5lt9  12390  4lt9  12391  3lt9  12392  2lt9  12393  1lt9  12394  10re  12675  9lt10  12787  8lt10  12788  0.999...  15854  cos2bnd  16163  sincos2sgn  16169  slotsdifplendx  17345  dsndxntsetndx  17363  unifndxntsetndx  17370  2logb9irr  26712  sqrt2cxp2logb9e3  26716  log2tlbnd  26862  bposlem4  27205  bposlem5  27206  bposlem7  27208  bposlem8  27209  bposlem9  27210  ex-fv  30379  dp2lt10  32811  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  problem5  35663  60gcd7e1  42000  lcmineqlem23  42046  3lexlogpow5ineq1  42049  3lexlogpow5ineq2  42050  3lexlogpow5ineq4  42051  3lexlogpow5ineq3  42052  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1lem1  42057  aks4d1p1  42071  aks4d1p6  42076  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8  42082  9rp  42299  31prm  47602  2exp340mod341  47738  341fppr2  47739  9fppr8  47742  nfermltl8rev  47747  nfermltl2rev  47748  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  bgoldbtbndlem1  47810  ackval42  48689