Theorem 9re 12365

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 12336	. 2 ⊢ 9 = (8 + 1)
2		8re 12362	. . 3 ⊢ 8 ∈ ℝ
3		1re 11261	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11276	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2837	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  ℝcr 11154  1c1 11156   + caddc 11158  8c8 12327  9c9 12328

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336

This theorem is referenced by:  7lt9  12466  6lt9  12467  5lt9  12468  4lt9  12469  3lt9  12470  2lt9  12471  1lt9  12472  10re  12752  9lt10  12864  8lt10  12865  0.999...  15917  cos2bnd  16224  sincos2sgn  16230  slotsdifplendx  17419  dsndxntsetndx  17437  unifndxntsetndx  17444  cnfldfunALTOLDOLD  21393  tuslemOLD  24276  setsmsdsOLD  24488  tnglemOLD  24654  tngdsOLD  24669  2logb9irr  26838  sqrt2cxp2logb9e3  26842  log2tlbnd  26988  bposlem4  27331  bposlem5  27332  bposlem7  27334  bposlem8  27335  bposlem9  27336  ex-fv  30462  dp2lt10  32866  hgt750lem  34666  hgt750lem2  34667  hgt750leme  34673  problem5  35674  60gcd7e1  42006  lcmineqlem23  42052  3lexlogpow5ineq1  42055  3lexlogpow5ineq2  42056  3lexlogpow5ineq4  42057  3lexlogpow5ineq3  42058  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1lem1  42063  aks4d1p1  42077  aks4d1p6  42082  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8  42088  9rp  42338  31prm  47584  2exp340mod341  47720  341fppr2  47721  9fppr8  47724  nfermltl8rev  47729  nfermltl2rev  47730  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem1  47792  ackval42  48617