![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 8re | GIF version |
Description: The number 8 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
8re | ⊢ 8 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-8 8960 | . 2 ⊢ 8 = (7 + 1) | |
2 | 7re 8978 | . . 3 ⊢ 7 ∈ ℝ | |
3 | 1re 7934 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7948 | . 2 ⊢ (7 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2250 | 1 ⊢ 8 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2148 (class class class)co 5868 ℝcr 7788 1c1 7790 + caddc 7792 7c7 8951 8c8 8952 |
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 7883 ax-addrcl 7886 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-clel 2173 df-2 8954 df-3 8955 df-4 8956 df-5 8957 df-6 8958 df-7 8959 df-8 8960 |
This theorem is referenced by: 8cn 8981 9re 8982 9pos 8999 6lt8 9086 5lt8 9087 4lt8 9088 3lt8 9089 2lt8 9090 1lt8 9091 8lt9 9092 7lt9 9093 8th4div3 9114 8lt10 9491 7lt10 9492 ef01bndlem 11735 cos2bnd 11739 slotstnscsi 12604 slotsdnscsi 12620 |
Copyright terms: Public domain | W3C validator |