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

Theorem 8re 10611
Description: The number 8 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
8re  |-  8  e.  RR

Proof of Theorem 8re
StepHypRef Expression
1 df-8 10591 . 2  |-  8  =  ( 7  +  1 )
2 7re 10609 . . 3  |-  7  e.  RR
3 1re 9586 . . 3  |-  1  e.  RR
42, 3readdcli 9600 . 2  |-  ( 7  +  1 )  e.  RR
51, 4eqeltri 2546 1  |-  8  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762  (class class class)co 6277   RRcr 9482   1c1 9484    + caddc 9486   7c7 10581   8c8 10582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-i2m1 9551  ax-1ne0 9552  ax-rrecex 9555  ax-cnre 9556
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-iota 5544  df-fv 5589  df-ov 6280  df-2 10585  df-3 10586  df-4 10587  df-5 10588  df-6 10589  df-7 10590  df-8 10591
This theorem is referenced by:  8cn  10612  9re  10613  9pos  10628  6lt8  10715  5lt8  10716  4lt8  10717  3lt8  10718  2lt8  10719  1lt8  10720  8lt9  10721  7lt9  10722  8lt10  10730  7lt10  10731  8th4div3  10750  ef01bndlem  13771  cos2bnd  13775  sralem  17601  chtub  23210  bposlem8  23289  bposlem9  23290  lgsdir2lem1  23321  lgsdir2lem4  23324  lgsdir2lem5  23325  chebbnd1lem2  23378  chebbnd1lem3  23379  chebbnd1  23380  pntlemf  23513  cchhllem  23861
  Copyright terms: Public domain W3C validator