MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  9re Structured version   Visualization version   GIF version

Theorem 9re 11728
Description: The number 9 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
9re 9 ∈ ℝ

Proof of Theorem 9re
StepHypRef Expression
1 df-9 11699 . 2 9 = (8 + 1)
2 8re 11725 . . 3 8 ∈ ℝ
3 1re 10634 . . 3 1 ∈ ℝ
42, 3readdcli 10649 . 2 (8 + 1) ∈ ℝ
51, 4eqeltri 2889 1 9 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  (class class class)co 7139  cr 10529  1c1 10531   + caddc 10533  8c8 11690  9c9 11691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-i2m1 10598  ax-1ne0 10599  ax-rrecex 10602  ax-cnre 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ne 2991  df-ral 3114  df-rex 3115  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699
This theorem is referenced by:  7lt9  11829  6lt9  11830  5lt9  11831  4lt9  11832  3lt9  11833  2lt9  11834  1lt9  11835  10re  12109  9lt10  12221  8lt10  12222  0.999...  15232  cos2bnd  15536  sincos2sgn  15542  cnfldfun  20106  tuslem  22876  setsmsds  23086  tnglem  23249  tngds  23257  2logb9irr  25384  sqrt2cxp2logb9e3  25388  log2tlbnd  25534  bposlem4  25874  bposlem5  25875  bposlem7  25877  bposlem8  25878  bposlem9  25879  ex-fv  28231  dp2lt10  30589  hgt750lem  32030  hgt750lem2  32031  hgt750leme  32037  problem5  33020  60gcd7e1  39286  lcmineqlem23  39332  3lexlogpow5ineq1  39334  31prm  44101  2exp340mod341  44238  341fppr2  44239  9fppr8  44242  nfermltl8rev  44247  nfermltl2rev  44248  wtgoldbnnsum4prm  44307  bgoldbnnsum3prm  44309  bgoldbtbndlem1  44310  ackval42  45097
  Copyright terms: Public domain W3C validator