Theorem 9re 12357

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 12327	. 2 ⊢ 9 = (8 + 1)
2		8re 12354	. . 3 ⊢ 8 ∈ ℝ
3		1re 11225	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11241	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2861	1 ⊢ 9 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℝcr 11116  1c1 11118   + caddc 11120  8c8 12318  9c9 12319

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-i2m1 11185  ax-1ne0 11186  ax-rrecex 11189  ax-cnre 11190

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324  df-7 12325  df-8 12326  df-9 12327

This theorem is used by:  7lt9  12460  6lt9  12461  5lt9  12462  4lt9  12463  3lt9  12464  2lt9  12465  1lt9  12466  10re  12752  9lt10  12866  8lt10  12867  7lt10  12868  6lt10  12869  5lt10  12870  4lt10  12871  3lt10  12872  2lt10  12873  1lt10  12874  0.999...  15960  cos2bnd  16268  sincos2sgn  16274  slotsdifplendx  17452  dsndxntsetndx  17470  unifndxntsetndx  17477  2logb9irr  27013  sqrt2cxp2logb9e3  27017  log2tlbnd  27163  bposlem4  27504  bposlem5  27505  bposlem7  27507  bposlem8  27508  bposlem9  27509  ex-fv  30867  dp2lt10  33275  hgt750lem  35105  hgt750lem2  35106  hgt750leme  35112  problem5  36200  60gcd7e1  42832  lcmineqlem23  42878  3lexlogpow5ineq1  42881  3lexlogpow5ineq2  42882  3lexlogpow5ineq4  42883  3lexlogpow5ineq3  42884  3lexlogpow2ineq2  42886  3lexlogpow5ineq5  42887  aks4d1lem1  42889  aks4d1p1  42903  aks4d1p6  42908  aks4d1p7d1  42909  aks4d1p7  42910  aks4d1p8  42914  9rp  43125  31prm  48409  2exp340mod341  48558  341fppr2  48559  9fppr8  48562  nfermltl8rev  48567  nfermltl2rev  48568  wtgoldbnnsum4prm  48627  bgoldbnnsum3prm  48629  bgoldbtbndlem1  48630  ackval42  49535