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

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

Proof of Theorem 8re
StepHypRef Expression
1 df-8 11694 . 2 8 = (7 + 1)
2 7re 11718 . . 3 7 ∈ ℝ
3 1re 10629 . . 3 1 ∈ ℝ
42, 3readdcli 10644 . 2 (7 + 1) ∈ ℝ
51, 4eqeltri 2906 1 8 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  (class class class)co 7145  cr 10524  1c1 10526   + caddc 10528  7c7 11685  8c8 11686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-i2m1 10593  ax-1ne0 10594  ax-rrecex 10597  ax-cnre 10598
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694
This theorem is referenced by:  9re  11724  9pos  11738  6lt8  11818  5lt8  11819  4lt8  11820  3lt8  11821  2lt8  11822  1lt8  11823  8lt9  11824  7lt9  11825  8th4div3  11845  8lt10  12218  7lt10  12219  ef01bndlem  15525  cos2bnd  15529  sralem  19878  chtub  25715  bposlem8  25794  bposlem9  25795  lgsdir2lem1  25828  lgsdir2lem4  25831  lgsdir2lem5  25832  2lgsoddprmlem1  25911  2lgsoddprmlem2  25912  chebbnd1lem2  25973  chebbnd1lem3  25974  chebbnd1  25975  pntlemf  26108  cchhllem  26600  hgt750lem  31821  hgt750lem2  31822  hgt750leme  31828  fmtnoprmfac2lem1  43605  mod42tp1mod8  43644  nnsum3primesle9  43836  nnsum4primesoddALTV  43839  nnsum4primesevenALTV  43843  bgoldbtbndlem1  43847  tgoldbach  43859
  Copyright terms: Public domain W3C validator