Theorem 9re 12311

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 12282	. 2 ⊢ 9 = (8 + 1)
2		8re 12308	. . 3 ⊢ 8 ∈ ℝ
3		1re 11214	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11229	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2830	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  ℝcr 11109  1c1 11111   + caddc 11113  8c8 12273  9c9 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rrecex 11182  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282

This theorem is referenced by:  7lt9  12412  6lt9  12413  5lt9  12414  4lt9  12415  3lt9  12416  2lt9  12417  1lt9  12418  10re  12696  9lt10  12808  8lt10  12809  0.999...  15827  cos2bnd  16131  sincos2sgn  16137  slotsdifplendx  17320  dsndxntsetndx  17338  unifndxntsetndx  17345  cnfldfunALTOLD  20958  tuslemOLD  23772  setsmsdsOLD  23984  tnglemOLD  24150  tngdsOLD  24165  2logb9irr  26300  sqrt2cxp2logb9e3  26304  log2tlbnd  26450  bposlem4  26790  bposlem5  26791  bposlem7  26793  bposlem8  26794  bposlem9  26795  ex-fv  29696  dp2lt10  32050  hgt750lem  33663  hgt750lem2  33664  hgt750leme  33670  problem5  34654  60gcd7e1  40870  lcmineqlem23  40916  3lexlogpow5ineq1  40919  3lexlogpow5ineq2  40920  3lexlogpow5ineq4  40921  3lexlogpow5ineq3  40922  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  aks4d1lem1  40927  aks4d1p1  40941  aks4d1p6  40946  aks4d1p7d1  40947  aks4d1p7  40948  aks4d1p8  40952  31prm  46265  2exp340mod341  46401  341fppr2  46402  9fppr8  46405  nfermltl8rev  46410  nfermltl2rev  46411  wtgoldbnnsum4prm  46470  bgoldbnnsum3prm  46472  bgoldbtbndlem1  46473  ackval42  47382