Theorem 9re 12227

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 12198	. 2 ⊢ 9 = (8 + 1)
2		8re 12224	. . 3 ⊢ 8 ∈ ℝ
3		1re 11115	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11130	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008  1c1 11010   + caddc 11012  8c8 12189  9c9 12190

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rrecex 11081  ax-cnre 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195  df-7 12196  df-8 12197  df-9 12198

This theorem is referenced by:  7lt9  12323  6lt9  12324  5lt9  12325  4lt9  12326  3lt9  12327  2lt9  12328  1lt9  12329  10re  12610  9lt10  12722  8lt10  12723  0.999...  15788  cos2bnd  16097  sincos2sgn  16103  slotsdifplendx  17279  dsndxntsetndx  17297  unifndxntsetndx  17304  2logb9irr  26703  sqrt2cxp2logb9e3  26707  log2tlbnd  26853  bposlem4  27196  bposlem5  27197  bposlem7  27199  bposlem8  27200  bposlem9  27201  ex-fv  30387  dp2lt10  32825  hgt750lem  34625  hgt750lem2  34626  hgt750leme  34632  problem5  35652  60gcd7e1  41988  lcmineqlem23  42034  3lexlogpow5ineq1  42037  3lexlogpow5ineq2  42038  3lexlogpow5ineq4  42039  3lexlogpow5ineq3  42040  3lexlogpow2ineq2  42042  3lexlogpow5ineq5  42043  aks4d1lem1  42045  aks4d1p1  42059  aks4d1p6  42064  aks4d1p7d1  42065  aks4d1p7  42066  aks4d1p8  42070  9rp  42287  31prm  47591  2exp340mod341  47727  341fppr2  47728  9fppr8  47731  nfermltl8rev  47736  nfermltl2rev  47737  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  bgoldbtbndlem1  47799  ackval42  48691