Theorem 9re 12280

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 12251	. 2 ⊢ 9 = (8 + 1)
2		8re 12277	. . 3 ⊢ 8 ∈ ℝ
3		1re 11144	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11160	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037  1c1 11039   + caddc 11041  8c8 12242  9c9 12243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251

This theorem is referenced by:  7lt9  12376  6lt9  12377  5lt9  12378  4lt9  12379  3lt9  12380  2lt9  12381  1lt9  12382  10re  12663  9lt10  12775  8lt10  12776  0.999...  15846  cos2bnd  16155  sincos2sgn  16161  slotsdifplendx  17338  dsndxntsetndx  17356  unifndxntsetndx  17363  2logb9irr  26759  sqrt2cxp2logb9e3  26763  log2tlbnd  26909  bposlem4  27250  bposlem5  27251  bposlem7  27253  bposlem8  27254  bposlem9  27255  ex-fv  30513  dp2lt10  32943  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  problem5  35851  60gcd7e1  42444  lcmineqlem23  42490  3lexlogpow5ineq1  42493  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow5ineq3  42496  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1lem1  42501  aks4d1p1  42515  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8  42526  9rp  42736  31prm  48060  2exp340mod341  48209  341fppr2  48210  9fppr8  48213  nfermltl8rev  48218  nfermltl2rev  48219  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem1  48281  ackval42  49172