Theorem 9re 12452

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 12422	. 2 ⊢ 9 = (8 + 1)
2		8re 12449	. . 3 ⊢ 8 ∈ ℝ
3		1re 11318	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11334	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 9 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℝcr 11209  1c1 11211   + caddc 11213  8c8 12413  9c9 12414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-i2m1 11278  ax-1ne0 11279  ax-rrecex 11282  ax-cnre 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419  df-7 12420  df-8 12421  df-9 12422

This theorem is used by:  7lt9  12555  6lt9  12556  5lt9  12557  4lt9  12558  3lt9  12559  2lt9  12560  1lt9  12561  10re  12847  9lt10  12961  8lt10  12962  7lt10  12963  6lt10  12964  5lt10  12965  4lt10  12966  3lt10  12967  2lt10  12968  1lt10  12969  0.999...  16062  cos2bnd  16368  sincos2sgn  16374  slotsdifplendx  17558  dsndxntsetndx  17576  unifndxntsetndx  17583  2logb9irr  27135  sqrt2cxp2logb9e3  27139  log2tlbnd  27285  bposlem4  27626  bposlem5  27627  bposlem7  27629  bposlem8  27630  bposlem9  27631  ex-fv  31056  dp2lt10  33503  hgt750lem  35333  hgt750lem2  35334  hgt750leme  35340  problem5  36555  60gcd7e1  43195  lcmineqlem23  43241  3lexlogpow5ineq1  43244  3lexlogpow5ineq2  43245  3lexlogpow5ineq4  43246  3lexlogpow5ineq3  43247  3lexlogpow2ineq2  43249  3lexlogpow5ineq5  43250  aks4d1lem1  43252  aks4d1p1  43266  aks4d1p6  43271  aks4d1p7d1  43272  aks4d1p7  43273  aks4d1p8  43277  9rp  43501  31prm  48821  2exp340mod341  48970  341fppr2  48971  9fppr8  48974  nfermltl8rev  48979  nfermltl2rev  48980  wtgoldbnnsum4prm  49039  bgoldbnnsum3prm  49041  bgoldbtbndlem1  49042  ackval42  49947