Theorem 9re 12275

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 12246	. 2 ⊢ 9 = (8 + 1)
2		8re 12272	. . 3 ⊢ 8 ∈ ℝ
3		1re 11140	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11156	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2837	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2121  (class class class)co 7359  ℝcr 11033  1c1 11035   + caddc 11037  8c8 12237  9c9 12238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-1cn 11092  ax-icn 11093  ax-addcl 11094  ax-addrcl 11095  ax-mulcl 11096  ax-mulrcl 11097  ax-i2m1 11102  ax-1ne0 11103  ax-rrecex 11106  ax-cnre 11107

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6444  df-fv 6496  df-ov 7362  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243  df-7 12244  df-8 12245  df-9 12246

This theorem is referenced by:  7lt9  12371  6lt9  12372  5lt9  12373  4lt9  12374  3lt9  12375  2lt9  12376  1lt9  12377  10re  12658  9lt10  12770  8lt10  12771  0.999...  15841  cos2bnd  16150  sincos2sgn  16156  slotsdifplendx  17333  dsndxntsetndx  17351  unifndxntsetndx  17358  2logb9irr  26780  sqrt2cxp2logb9e3  26784  log2tlbnd  26930  bposlem4  27271  bposlem5  27272  bposlem7  27274  bposlem8  27275  bposlem9  27276  ex-fv  30533  dp2lt10  32964  hgt750lem  34845  hgt750lem2  34846  hgt750leme  34852  problem5  35910  60gcd7e1  42503  lcmineqlem23  42549  3lexlogpow5ineq1  42552  3lexlogpow5ineq2  42553  3lexlogpow5ineq4  42554  3lexlogpow5ineq3  42555  3lexlogpow2ineq2  42557  3lexlogpow5ineq5  42558  aks4d1lem1  42560  aks4d1p1  42574  aks4d1p6  42579  aks4d1p7d1  42580  aks4d1p7  42581  aks4d1p8  42585  9rp  42794  31prm  48087  2exp340mod341  48236  341fppr2  48237  9fppr8  48240  nfermltl8rev  48245  nfermltl2rev  48246  wtgoldbnnsum4prm  48305  bgoldbnnsum3prm  48307  bgoldbtbndlem1  48308  ackval42  49199