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

Theorem 9re 12251
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 12222 . 2 9 = (8 + 1)
2 8re 12248 . . 3 8 ∈ ℝ
3 1re 11154 . . 3 1 ∈ ℝ
42, 3readdcli 11169 . 2 (8 + 1) ∈ ℝ
51, 4eqeltri 2834 1 9 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  (class class class)co 7356  cr 11049  1c1 11051   + caddc 11053  8c8 12213  9c9 12214
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-1cn 11108  ax-icn 11109  ax-addcl 11110  ax-addrcl 11111  ax-mulcl 11112  ax-mulrcl 11113  ax-i2m1 11118  ax-1ne0 11119  ax-rrecex 11122  ax-cnre 11123
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7359  df-2 12215  df-3 12216  df-4 12217  df-5 12218  df-6 12219  df-7 12220  df-8 12221  df-9 12222
This theorem is referenced by:  7lt9  12352  6lt9  12353  5lt9  12354  4lt9  12355  3lt9  12356  2lt9  12357  1lt9  12358  10re  12636  9lt10  12748  8lt10  12749  0.999...  15765  cos2bnd  16069  sincos2sgn  16075  slotsdifplendx  17255  dsndxntsetndx  17273  unifndxntsetndx  17280  cnfldfunALTOLD  20808  tuslemOLD  23617  setsmsdsOLD  23829  tnglemOLD  23995  tngdsOLD  24010  2logb9irr  26143  sqrt2cxp2logb9e3  26147  log2tlbnd  26293  bposlem4  26633  bposlem5  26634  bposlem7  26636  bposlem8  26637  bposlem9  26638  ex-fv  29334  dp2lt10  31684  hgt750lem  33204  hgt750lem2  33205  hgt750leme  33211  problem5  34197  60gcd7e1  40452  lcmineqlem23  40498  3lexlogpow5ineq1  40501  3lexlogpow5ineq2  40502  3lexlogpow5ineq4  40503  3lexlogpow5ineq3  40504  3lexlogpow2ineq2  40506  3lexlogpow5ineq5  40507  aks4d1lem1  40509  aks4d1p1  40523  aks4d1p6  40528  aks4d1p7d1  40529  aks4d1p7  40530  aks4d1p8  40534  31prm  45760  2exp340mod341  45896  341fppr2  45897  9fppr8  45900  nfermltl8rev  45905  nfermltl2rev  45906  wtgoldbnnsum4prm  45965  bgoldbnnsum3prm  45967  bgoldbtbndlem1  45968  ackval42  46753
  Copyright terms: Public domain W3C validator