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

Theorem 6re 8808
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 8790 . 2 6 = (5 + 1)
2 5re 8806 . . 3 5 ∈ ℝ
3 1re 7772 . . 3 1 ∈ ℝ
42, 3readdcli 7786 . 2 (5 + 1) ∈ ℝ
51, 4eqeltri 2212 1 6 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1480  (class class class)co 5774  cr 7626  1c1 7628   + caddc 7630  5c5 8781  6c6 8782
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1re 7721  ax-addrcl 7724
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135  df-2 8786  df-3 8787  df-4 8788  df-5 8789  df-6 8790
This theorem is referenced by:  6cn  8809  7re  8810  7pos  8829  4lt6  8907  3lt6  8908  2lt6  8909  1lt6  8910  6lt7  8911  5lt7  8912  6lt8  8918  5lt8  8919  6lt9  8926  5lt9  8927  8th4div3  8946  halfpm6th  8947  div4p1lem1div2  8980  6lt10  9322  5lt10  9323  5recm6rec  9332  efi4p  11431  resin4p  11432  recos4p  11433  ef01bndlem  11470  sin01bnd  11471  cos01bnd  11472  sincos6thpi  12936  pigt3  12938
  Copyright terms: Public domain W3C validator