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

Theorem 8re 10948
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 10928 . 2 8 = (7 + 1)
2 7re 10946 . . 3 7 ∈ ℝ
3 1re 9891 . . 3 1 ∈ ℝ
42, 3readdcli 9905 . 2 (7 + 1) ∈ ℝ
51, 4eqeltri 2679 1 8 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1975  (class class class)co 6523  cr 9787  1c1 9789   + caddc 9791  7c7 10918  8c8 10919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-i2m1 9856  ax-1ne0 9857  ax-rrecex 9860  ax-cnre 9861
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-iota 5750  df-fv 5794  df-ov 6526  df-2 10922  df-3 10923  df-4 10924  df-5 10925  df-6 10926  df-7 10927  df-8 10928
This theorem is referenced by:  8cn  10949  9re  10950  9pos  10965  6lt8  11059  5lt8  11060  4lt8  11061  3lt8  11062  2lt8  11063  1lt8  11064  8lt9  11065  7lt9  11066  8lt10OLD  11074  7lt10OLD  11075  8th4div3  11095  8lt10  11502  7lt10  11503  ef01bndlem  14695  cos2bnd  14699  sralem  18940  chtub  24650  bposlem8  24729  bposlem9  24730  lgsdir2lem1  24763  lgsdir2lem4  24766  lgsdir2lem5  24767  2lgsoddprmlem1  24846  2lgsoddprmlem2  24847  chebbnd1lem2  24872  chebbnd1lem3  24873  chebbnd1  24874  pntlemf  25007  cchhllem  25481  fmtnoprmfac2lem1  39817  mod42tp1mod8  39858  nnsum3primesle9  40011  nnsum4primesoddALTV  40014  nnsum4primesevenALTV  40018  bgoldbtbndlem1  40022  tgoldbach  40033  tgoldbachOLD  40040
  Copyright terms: Public domain W3C validator