Theorem 9re 12242

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 12213	. 2 ⊢ 9 = (8 + 1)
2		8re 12239	. . 3 ⊢ 8 ∈ ℝ
3		1re 11130	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11145	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2830	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℝcr 11023  1c1 11025   + caddc 11027  8c8 12204  9c9 12205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-i2m1 11092  ax-1ne0 11093  ax-rrecex 11096  ax-cnre 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-2 12206  df-3 12207  df-4 12208  df-5 12209  df-6 12210  df-7 12211  df-8 12212  df-9 12213

This theorem is referenced by:  7lt9  12338  6lt9  12339  5lt9  12340  4lt9  12341  3lt9  12342  2lt9  12343  1lt9  12344  10re  12624  9lt10  12736  8lt10  12737  0.999...  15802  cos2bnd  16111  sincos2sgn  16117  slotsdifplendx  17293  dsndxntsetndx  17311  unifndxntsetndx  17318  2logb9irr  26759  sqrt2cxp2logb9e3  26763  log2tlbnd  26909  bposlem4  27252  bposlem5  27253  bposlem7  27255  bposlem8  27256  bposlem9  27257  ex-fv  30467  dp2lt10  32914  hgt750lem  34757  hgt750lem2  34758  hgt750leme  34764  problem5  35812  60gcd7e1  42198  lcmineqlem23  42244  3lexlogpow5ineq1  42247  3lexlogpow5ineq2  42248  3lexlogpow5ineq4  42249  3lexlogpow5ineq3  42250  3lexlogpow2ineq2  42252  3lexlogpow5ineq5  42253  aks4d1lem1  42255  aks4d1p1  42269  aks4d1p6  42274  aks4d1p7d1  42275  aks4d1p7  42276  aks4d1p8  42280  9rp  42501  31prm  47785  2exp340mod341  47921  341fppr2  47922  9fppr8  47925  nfermltl8rev  47930  nfermltl2rev  47931  wtgoldbnnsum4prm  47990  bgoldbnnsum3prm  47992  bgoldbtbndlem1  47993  ackval42  48884