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

Theorem 6re 8070
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 8052 . 2 6 = (5 + 1)
2 5re 8068 . . 3 5 ∈ ℝ
3 1re 7083 . . 3 1 ∈ ℝ
42, 3readdcli 7097 . 2 (5 + 1) ∈ ℝ
51, 4eqeltri 2126 1 6 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1409  (class class class)co 5539  cr 6945  1c1 6947   + caddc 6949  5c5 8042  6c6 8043
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038  ax-1re 7035  ax-addrcl 7038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052  df-2 8048  df-3 8049  df-4 8050  df-5 8051  df-6 8052
This theorem is referenced by:  6cn  8071  7re  8072  7pos  8091  4lt6  8162  3lt6  8163  2lt6  8164  1lt6  8165  6lt7  8166  5lt7  8167  6lt8  8173  5lt8  8174  6lt9  8181  5lt9  8182  8th4div3  8200  halfpm6th  8201  div4p1lem1div2  8234  6lt10  8559  5lt10  8560
  Copyright terms: Public domain W3C validator