![]() |
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 8809 | . 2 ⊢ 8 = (7 + 1) | |
2 | 7re 8827 | . . 3 ⊢ 7 ∈ ℝ | |
3 | 1re 7789 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7803 | . 2 ⊢ (7 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2213 | 1 ⊢ 8 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1481 (class class class)co 5782 ℝcr 7643 1c1 7645 + caddc 7647 7c7 8800 8c8 8801 |
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 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-ext 2122 ax-1re 7738 ax-addrcl 7741 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 df-clel 2136 df-2 8803 df-3 8804 df-4 8805 df-5 8806 df-6 8807 df-7 8808 df-8 8809 |
This theorem is referenced by: 8cn 8830 9re 8831 9pos 8848 6lt8 8935 5lt8 8936 4lt8 8937 3lt8 8938 2lt8 8939 1lt8 8940 8lt9 8941 7lt9 8942 8th4div3 8963 8lt10 9337 7lt10 9338 ef01bndlem 11499 cos2bnd 11503 |
Copyright terms: Public domain | W3C validator |