Theorem 9re 12335

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 12305	. 2 ⊢ 9 = (8 + 1)
2		8re 12332	. . 3 ⊢ 8 ∈ ℝ
3		1re 11203	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11219	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094  1c1 11096   + caddc 11098  8c8 12296  9c9 12297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303  df-8 12304  df-9 12305

This theorem is referenced by:  7lt9  12438  6lt9  12439  5lt9  12440  4lt9  12441  3lt9  12442  2lt9  12443  1lt9  12444  10re  12729  9lt10  12843  8lt10  12844  7lt10  12845  6lt10  12846  5lt10  12847  4lt10  12848  3lt10  12849  2lt10  12850  1lt10  12851  0.999...  15931  cos2bnd  16239  sincos2sgn  16245  slotsdifplendx  17423  dsndxntsetndx  17441  unifndxntsetndx  17448  2logb9irr  26960  sqrt2cxp2logb9e3  26964  log2tlbnd  27110  bposlem4  27451  bposlem5  27452  bposlem7  27454  bposlem8  27455  bposlem9  27456  ex-fv  30794  dp2lt10  33203  hgt750lem  35038  hgt750lem2  35039  hgt750leme  35045  problem5  36161  60gcd7e1  42792  lcmineqlem23  42838  3lexlogpow5ineq1  42841  3lexlogpow5ineq2  42842  3lexlogpow5ineq4  42843  3lexlogpow5ineq3  42844  3lexlogpow2ineq2  42846  3lexlogpow5ineq5  42847  aks4d1lem1  42849  aks4d1p1  42863  aks4d1p6  42868  aks4d1p7d1  42869  aks4d1p7  42870  aks4d1p8  42874  9rp  43085  31prm  48369  2exp340mod341  48518  341fppr2  48519  9fppr8  48522  nfermltl8rev  48527  nfermltl2rev  48528  wtgoldbnnsum4prm  48587  bgoldbnnsum3prm  48589  bgoldbtbndlem1  48590  ackval42  49496