Theorem 9re 12274

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 12245	. 2 ⊢ 9 = (8 + 1)
2		8re 12271	. . 3 ⊢ 8 ∈ ℝ
3		1re 11138	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11154	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031  1c1 11033   + caddc 11035  8c8 12236  9c9 12237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242  df-7 12243  df-8 12244  df-9 12245

This theorem is referenced by:  7lt9  12370  6lt9  12371  5lt9  12372  4lt9  12373  3lt9  12374  2lt9  12375  1lt9  12376  10re  12657  9lt10  12769  8lt10  12770  0.999...  15840  cos2bnd  16149  sincos2sgn  16155  slotsdifplendx  17332  dsndxntsetndx  17350  unifndxntsetndx  17357  2logb9irr  26775  sqrt2cxp2logb9e3  26779  log2tlbnd  26925  bposlem4  27267  bposlem5  27268  bposlem7  27270  bposlem8  27271  bposlem9  27272  ex-fv  30531  dp2lt10  32961  hgt750lem  34814  hgt750lem2  34815  hgt750leme  34821  problem5  35870  60gcd7e1  42461  lcmineqlem23  42507  3lexlogpow5ineq1  42510  3lexlogpow5ineq2  42511  3lexlogpow5ineq4  42512  3lexlogpow5ineq3  42513  3lexlogpow2ineq2  42515  3lexlogpow5ineq5  42516  aks4d1lem1  42518  aks4d1p1  42532  aks4d1p6  42537  aks4d1p7d1  42538  aks4d1p7  42539  aks4d1p8  42543  9rp  42753  31prm  48075  2exp340mod341  48224  341fppr2  48225  9fppr8  48228  nfermltl8rev  48233  nfermltl2rev  48234  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem1  48296  ackval42  49187