Theorem 9re 12002

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 11973	. 2 ⊢ 9 = (8 + 1)
2		8re 11999	. . 3 ⊢ 8 ∈ ℝ
3		1re 10906	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10921	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2835	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7255  ℝcr 10801  1c1 10803   + caddc 10805  8c8 11964  9c9 11965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-2 11966  df-3 11967  df-4 11968  df-5 11969  df-6 11970  df-7 11971  df-8 11972  df-9 11973

This theorem is referenced by:  7lt9  12103  6lt9  12104  5lt9  12105  4lt9  12106  3lt9  12107  2lt9  12108  1lt9  12109  10re  12385  9lt10  12497  8lt10  12498  0.999...  15521  cos2bnd  15825  sincos2sgn  15831  dsndxntsetndx  17024  unifndxntsetndx  17030  cnfldfun  20522  tuslemOLD  23327  setsmsds  23537  tnglemOLD  23703  tngdsOLD  23718  2logb9irr  25850  sqrt2cxp2logb9e3  25854  log2tlbnd  26000  bposlem4  26340  bposlem5  26341  bposlem7  26343  bposlem8  26344  bposlem9  26345  ex-fv  28708  dp2lt10  31060  hgt750lem  32531  hgt750lem2  32532  hgt750leme  32538  problem5  33527  60gcd7e1  39941  lcmineqlem23  39987  3lexlogpow5ineq1  39990  3lexlogpow5ineq2  39991  3lexlogpow5ineq4  39992  3lexlogpow5ineq3  39993  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1lem1  39998  aks4d1p1  40012  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  31prm  44937  2exp340mod341  45073  341fppr2  45074  9fppr8  45077  nfermltl8rev  45082  nfermltl2rev  45083  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  bgoldbtbndlem1  45145  ackval42  45930