![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 5re | GIF version |
Description: The number 5 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
5re | ⊢ 5 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-5 8977 | . 2 ⊢ 5 = (4 + 1) | |
2 | 4re 8992 | . . 3 ⊢ 4 ∈ ℝ | |
3 | 1re 7953 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7967 | . 2 ⊢ (4 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 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 |