Theorem 9re 11894

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 11865	. 2 ⊢ 9 = (8 + 1)
2		8re 11891	. . 3 ⊢ 8 ∈ ℝ
3		1re 10798	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10813	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2827	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2112  (class class class)co 7191  ℝcr 10693  1c1 10695   + caddc 10697  8c8 11856  9c9 11857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-i2m1 10762  ax-1ne0 10763  ax-rrecex 10766  ax-cnre 10767

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194  df-2 11858  df-3 11859  df-4 11860  df-5 11861  df-6 11862  df-7 11863  df-8 11864  df-9 11865

This theorem is referenced by:  7lt9  11995  6lt9  11996  5lt9  11997  4lt9  11998  3lt9  11999  2lt9  12000  1lt9  12001  10re  12277  9lt10  12389  8lt10  12390  0.999...  15408  cos2bnd  15712  sincos2sgn  15718  cnfldfun  20329  tuslem  23118  setsmsds  23328  tnglem  23492  tngds  23500  2logb9irr  25632  sqrt2cxp2logb9e3  25636  log2tlbnd  25782  bposlem4  26122  bposlem5  26123  bposlem7  26125  bposlem8  26126  bposlem9  26127  ex-fv  28480  dp2lt10  30832  hgt750lem  32297  hgt750lem2  32298  hgt750leme  32304  problem5  33294  60gcd7e1  39696  lcmineqlem23  39742  3lexlogpow5ineq1  39745  3lexlogpow5ineq2  39746  3lexlogpow5ineq4  39747  3lexlogpow5ineq3  39748  3lexlogpow2ineq2  39750  3lexlogpow5ineq5  39751  aks4d1p1  39766  31prm  44665  2exp340mod341  44801  341fppr2  44802  9fppr8  44805  nfermltl8rev  44810  nfermltl2rev  44811  wtgoldbnnsum4prm  44870  bgoldbnnsum3prm  44872  bgoldbtbndlem1  44873  ackval42  45658