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

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

Proof of Theorem 5re
StepHypRef Expression
1 df-5 8977 . 2 5 = (4 + 1)
2 4re 8992 . . 3 4 ∈ ℝ
3 1re 7953 . . 3 1 ∈ ℝ
42, 3readdcli 7967 . 2 (4 + 1) ∈ ℝ
51, 4eqeltri 2250 1 5 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 2148  (class class class)co 5872  cr 7807  1c1 7809   + caddc 7811  4c4 8968  5c5 8969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7902  ax-addrcl 7905
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8974  df-3 8975  df-4 8976  df-5 8977
This theorem is referenced by:  5cn  8995  6re  8996  6pos  9016  3lt5  9091  2lt5  9092  1lt5  9093  5lt6  9094  4lt6  9095  5lt7  9100  4lt7  9101  5lt8  9107  4lt8  9108  5lt9  9115  4lt9  9116  5lt10  9514  4lt10  9515  5recm6rec  9523  ef01bndlem  11757  vscandxnscandx  12612  slotsdifipndx  12625  slotstnscsi  12642  plendxnscandx  12655  slotsdnscsi  12666  lgsdir2lem1  14300
  Copyright terms: Public domain W3C validator