Theorem 9re 12246

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 12217	. 2 ⊢ 9 = (8 + 1)
2		8re 12243	. . 3 ⊢ 8 ∈ ℝ
3		1re 11134	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11149	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℝcr 11027  1c1 11029   + caddc 11031  8c8 12208  9c9 12209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-i2m1 11096  ax-1ne0 11097  ax-rrecex 11100  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216  df-9 12217

This theorem is referenced by:  7lt9  12342  6lt9  12343  5lt9  12344  4lt9  12345  3lt9  12346  2lt9  12347  1lt9  12348  10re  12628  9lt10  12740  8lt10  12741  0.999...  15806  cos2bnd  16115  sincos2sgn  16121  slotsdifplendx  17297  dsndxntsetndx  17315  unifndxntsetndx  17322  2logb9irr  26763  sqrt2cxp2logb9e3  26767  log2tlbnd  26913  bposlem4  27256  bposlem5  27257  bposlem7  27259  bposlem8  27260  bposlem9  27261  ex-fv  30520  dp2lt10  32967  hgt750lem  34810  hgt750lem2  34811  hgt750leme  34817  problem5  35865  60gcd7e1  42281  lcmineqlem23  42327  3lexlogpow5ineq1  42330  3lexlogpow5ineq2  42331  3lexlogpow5ineq4  42332  3lexlogpow5ineq3  42333  3lexlogpow2ineq2  42335  3lexlogpow5ineq5  42336  aks4d1lem1  42338  aks4d1p1  42352  aks4d1p6  42357  aks4d1p7d1  42358  aks4d1p7  42359  aks4d1p8  42363  9rp  42580  31prm  47864  2exp340mod341  48000  341fppr2  48001  9fppr8  48004  nfermltl8rev  48009  nfermltl2rev  48010  wtgoldbnnsum4prm  48069  bgoldbnnsum3prm  48071  bgoldbtbndlem1  48072  ackval42  48963