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

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

Proof of Theorem 6re
StepHypRef Expression
1 df-6 8743 . 2  |-  6  =  ( 5  +  1 )
2 5re 8759 . . 3  |-  5  e.  RR
3 1re 7729 . . 3  |-  1  e.  RR
42, 3readdcli 7743 . 2  |-  ( 5  +  1 )  e.  RR
51, 4eqeltri 2188 1  |-  6  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1463  (class class class)co 5740   RRcr 7583   1c1 7585    + caddc 7587   5c5 8734   6c6 8735
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097  ax-1re 7678  ax-addrcl 7681
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111  df-2 8739  df-3 8740  df-4 8741  df-5 8742  df-6 8743
This theorem is referenced by:  6cn  8762  7re  8763  7pos  8782  4lt6  8854  3lt6  8855  2lt6  8856  1lt6  8857  6lt7  8858  5lt7  8859  6lt8  8865  5lt8  8866  6lt9  8873  5lt9  8874  8th4div3  8893  halfpm6th  8894  div4p1lem1div2  8927  6lt10  9269  5lt10  9270  efi4p  11334  resin4p  11335  recos4p  11336  ef01bndlem  11373  sin01bnd  11374  cos01bnd  11375
  Copyright terms: Public domain W3C validator