Theorem 9re 12363

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 12334	. 2 ⊢ 9 = (8 + 1)
2		8re 12360	. . 3 ⊢ 8 ∈ ℝ
3		1re 11264	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11279	. 2 ⊢ (8 + 1) ∈ ℝ
5	1, 4	eqeltri 2822	1 ⊢ 9 ∈ ℝ

Syntax hints:   ∈ wcel 2099  (class class class)co 7424  ℝcr 11157  1c1 11159   + caddc 11161  8c8 12325  9c9 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-i2m1 11226  ax-1ne0 11227  ax-rrecex 11230  ax-cnre 11231

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-iota 6506  df-fv 6562  df-ov 7427  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334

This theorem is referenced by:  7lt9  12464  6lt9  12465  5lt9  12466  4lt9  12467  3lt9  12468  2lt9  12469  1lt9  12470  10re  12748  9lt10  12860  8lt10  12861  0.999...  15885  cos2bnd  16190  sincos2sgn  16196  slotsdifplendx  17389  dsndxntsetndx  17407  unifndxntsetndx  17414  cnfldfunALTOLDOLD  21372  tuslemOLD  24263  setsmsdsOLD  24475  tnglemOLD  24641  tngdsOLD  24656  2logb9irr  26823  sqrt2cxp2logb9e3  26827  log2tlbnd  26973  bposlem4  27316  bposlem5  27317  bposlem7  27319  bposlem8  27320  bposlem9  27321  ex-fv  30376  dp2lt10  32745  hgt750lem  34497  hgt750lem2  34498  hgt750leme  34504  problem5  35497  60gcd7e1  41704  lcmineqlem23  41750  3lexlogpow5ineq1  41753  3lexlogpow5ineq2  41754  3lexlogpow5ineq4  41755  3lexlogpow5ineq3  41756  3lexlogpow2ineq2  41758  3lexlogpow5ineq5  41759  aks4d1lem1  41761  aks4d1p1  41775  aks4d1p6  41780  aks4d1p7d1  41781  aks4d1p7  41782  aks4d1p8  41786  31prm  47169  2exp340mod341  47305  341fppr2  47306  9fppr8  47309  nfermltl8rev  47314  nfermltl2rev  47315  wtgoldbnnsum4prm  47374  bgoldbnnsum3prm  47376  bgoldbtbndlem1  47377  ackval42  48084