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

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

Proof of Theorem 6re
StepHypRef Expression
1 df-6 7977 . 2 6 = (5 + 1)
2 5re 7994 . . 3 5 ∈ ℝ
3 1re 7026 . . 3 1 ∈ ℝ
42, 3readdcli 7040 . 2 (5 + 1) ∈ ℝ
51, 4eqeltri 2110 1 6 ∈ ℝ
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1393  (class class class)co 5512  ℝcr 6888  1c1 6890   + caddc 6892  5c5 7967  6c6 7968 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022  ax-1re 6978  ax-addrcl 6981 This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-2 7973  df-3 7974  df-4 7975  df-5 7976  df-6 7977 This theorem is referenced by:  6cn  7997  7re  7998  7pos  8018  4lt6  8097  3lt6  8098  2lt6  8099  1lt6  8100  6lt7  8101  5lt7  8102  6lt8  8108  5lt8  8109  6lt9  8116  5lt9  8117  6lt10  8125  5lt10  8126  8th4div3  8144  halfpm6th  8145  div4p1lem1div2  8177
 Copyright terms: Public domain W3C validator