Theorem 9re 12442

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 12412	. 2 ⊢ 9 = (8 + 1)
2		8re 12439	. . 3 ⊢ 8 ∈ ℝ
3		1re 11308	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11324	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2857	1 ⊢ 9 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℝcr 11199  1c1 11201   + caddc 11203  8c8 12403  9c9 12404

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 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rrecex 11272  ax-cnre 11273

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409  df-7 12410  df-8 12411  df-9 12412

This theorem is used by:  7lt9  12545  6lt9  12546  5lt9  12547  4lt9  12548  3lt9  12549  2lt9  12550  1lt9  12551  10re  12837  9lt10  12951  8lt10  12952  7lt10  12953  6lt10  12954  5lt10  12955  4lt10  12956  3lt10  12957  2lt10  12958  1lt10  12959  0.999...  16050  cos2bnd  16356  sincos2sgn  16362  slotsdifplendx  17546  dsndxntsetndx  17564  unifndxntsetndx  17571  2logb9irr  27123  sqrt2cxp2logb9e3  27127  log2tlbnd  27273  bposlem4  27614  bposlem5  27615  bposlem7  27617  bposlem8  27618  bposlem9  27619  ex-fv  31044  dp2lt10  33450  hgt750lem  35280  hgt750lem2  35281  hgt750leme  35287  problem5  36434  60gcd7e1  43055  lcmineqlem23  43101  3lexlogpow5ineq1  43104  3lexlogpow5ineq2  43105  3lexlogpow5ineq4  43106  3lexlogpow5ineq3  43107  3lexlogpow2ineq2  43109  3lexlogpow5ineq5  43110  aks4d1lem1  43112  aks4d1p1  43126  aks4d1p6  43131  aks4d1p7d1  43132  aks4d1p7  43133  aks4d1p8  43137  9rp  43361  31prm  48681  2exp340mod341  48830  341fppr2  48831  9fppr8  48834  nfermltl8rev  48839  nfermltl2rev  48840  wtgoldbnnsum4prm  48899  bgoldbnnsum3prm  48901  bgoldbtbndlem1  48902  ackval42  49807