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

Theorem 9re 12257
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 12228 . 2 9 = (8 + 1)
2 8re 12254 . . 3 8 ∈ ℝ
3 1re 11160 . . 3 1 ∈ ℝ
42, 3readdcli 11175 . 2 (8 + 1) ∈ ℝ
51, 4eqeltri 2830 1 9 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7358  cr 11055  1c1 11057   + caddc 11059  8c8 12219  9c9 12220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-i2m1 11124  ax-1ne0 11125  ax-rrecex 11128  ax-cnre 11129
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228
This theorem is referenced by:  7lt9  12358  6lt9  12359  5lt9  12360  4lt9  12361  3lt9  12362  2lt9  12363  1lt9  12364  10re  12642  9lt10  12754  8lt10  12755  0.999...  15771  cos2bnd  16075  sincos2sgn  16081  slotsdifplendx  17261  dsndxntsetndx  17279  unifndxntsetndx  17286  cnfldfunALTOLD  20826  tuslemOLD  23635  setsmsdsOLD  23847  tnglemOLD  24013  tngdsOLD  24028  2logb9irr  26161  sqrt2cxp2logb9e3  26165  log2tlbnd  26311  bposlem4  26651  bposlem5  26652  bposlem7  26654  bposlem8  26655  bposlem9  26656  ex-fv  29429  dp2lt10  31789  hgt750lem  33321  hgt750lem2  33322  hgt750leme  33328  problem5  34314  60gcd7e1  40508  lcmineqlem23  40554  3lexlogpow5ineq1  40557  3lexlogpow5ineq2  40558  3lexlogpow5ineq4  40559  3lexlogpow5ineq3  40560  3lexlogpow2ineq2  40562  3lexlogpow5ineq5  40563  aks4d1lem1  40565  aks4d1p1  40579  aks4d1p6  40584  aks4d1p7d1  40585  aks4d1p7  40586  aks4d1p8  40590  31prm  45875  2exp340mod341  46011  341fppr2  46012  9fppr8  46015  nfermltl8rev  46020  nfermltl2rev  46021  wtgoldbnnsum4prm  46080  bgoldbnnsum3prm  46082  bgoldbtbndlem1  46083  ackval42  46868
  Copyright terms: Public domain W3C validator