Theorem 9re 12362

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 12333	. 2 ⊢ 9 = (8 + 1)
2		8re 12359	. . 3 ⊢ 8 ∈ ℝ
3		1re 11258	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11273	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2834	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2105  (class class class)co 7430  ℝcr 11151  1c1 11153   + caddc 11155  8c8 12324  9c9 12325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333

This theorem is referenced by:  7lt9  12463  6lt9  12464  5lt9  12465  4lt9  12466  3lt9  12467  2lt9  12468  1lt9  12469  10re  12749  9lt10  12861  8lt10  12862  0.999...  15913  cos2bnd  16220  sincos2sgn  16226  slotsdifplendx  17420  dsndxntsetndx  17438  unifndxntsetndx  17445  cnfldfunALTOLDOLD  21410  tuslemOLD  24291  setsmsdsOLD  24503  tnglemOLD  24669  tngdsOLD  24684  2logb9irr  26852  sqrt2cxp2logb9e3  26856  log2tlbnd  27002  bposlem4  27345  bposlem5  27346  bposlem7  27348  bposlem8  27349  bposlem9  27350  ex-fv  30471  dp2lt10  32850  hgt750lem  34644  hgt750lem2  34645  hgt750leme  34651  problem5  35653  60gcd7e1  41986  lcmineqlem23  42032  3lexlogpow5ineq1  42035  3lexlogpow5ineq2  42036  3lexlogpow5ineq4  42037  3lexlogpow5ineq3  42038  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1lem1  42043  aks4d1p1  42057  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  9rp  42316  31prm  47521  2exp340mod341  47657  341fppr2  47658  9fppr8  47661  nfermltl8rev  47666  nfermltl2rev  47667  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  bgoldbtbndlem1  47729  ackval42  48545