ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  8re Unicode version

Theorem 8re 8663
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 8643 . 2  |-  8  =  ( 7  +  1 )
2 7re 8661 . . 3  |-  7  e.  RR
3 1re 7637 . . 3  |-  1  e.  RR
42, 3readdcli 7651 . 2  |-  ( 7  +  1 )  e.  RR
51, 4eqeltri 2172 1  |-  8  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1448  (class class class)co 5706   RRcr 7499   1c1 7501    + caddc 7503   7c7 8634   8c8 8635
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082  ax-1re 7589  ax-addrcl 7592
This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096  df-2 8637  df-3 8638  df-4 8639  df-5 8640  df-6 8641  df-7 8642  df-8 8643
This theorem is referenced by:  8cn  8664  9re  8665  9pos  8682  6lt8  8763  5lt8  8764  4lt8  8765  3lt8  8766  2lt8  8767  1lt8  8768  8lt9  8769  7lt9  8770  8th4div3  8791  8lt10  9165  7lt10  9166  ef01bndlem  11261  cos2bnd  11265
  Copyright terms: Public domain W3C validator