Theorem 9re 11584

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 11555	. 2 ⊢ 9 = (8 + 1)
2		8re 11581	. . 3 ⊢ 8 ∈ ℝ
3		1re 10487	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10502	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2879	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2081  (class class class)co 7016  ℝcr 10382  1c1 10384   + caddc 10386  8c8 11546  9c9 11547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-i2m1 10451  ax-1ne0 10452  ax-rrecex 10455  ax-cnre 10456

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-iota 6189  df-fv 6233  df-ov 7019  df-2 11548  df-3 11549  df-4 11550  df-5 11551  df-6 11552  df-7 11553  df-8 11554  df-9 11555

This theorem is referenced by:  7lt9  11685  6lt9  11686  5lt9  11687  4lt9  11688  3lt9  11689  2lt9  11690  1lt9  11691  10re  11966  9lt10  12079  8lt10  12080  0.999...  15070  cos2bnd  15374  sincos2sgn  15380  cnfldfun  20239  tuslem  22559  setsmsds  22769  tnglem  22932  tngds  22940  2logb9irr  25054  sqrt2cxp2logb9e3  25058  log2tlbnd  25205  bposlem4  25545  bposlem5  25546  bposlem7  25548  bposlem8  25549  bposlem9  25550  ex-fv  27914  dp2lt10  30244  hgt750lem  31539  hgt750lem2  31540  hgt750leme  31546  problem5  32520  31prm  43242  2exp340mod341  43380  341fppr2  43381  9fppr8  43384  nfermltl8rev  43389  nfermltl2rev  43390  wtgoldbnnsum4prm  43449  bgoldbnnsum3prm  43451  bgoldbtbndlem1  43452