![]() |
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 8485 | . 2 ⊢ 8 = (7 + 1) | |
2 | 7re 8503 | . . 3 ⊢ 7 ∈ ℝ | |
3 | 1re 7485 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7499 | . 2 ⊢ (7 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2160 | 1 ⊢ 8 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1438 (class class class)co 5652 ℝcr 7347 1c1 7349 + caddc 7351 7c7 8476 8c8 8477 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-4 1445 ax-17 1464 ax-ial 1472 ax-ext 2070 ax-1re 7437 ax-addrcl 7440 |
This theorem depends on definitions: df-bi 115 df-cleq 2081 df-clel 2084 df-2 8479 df-3 8480 df-4 8481 df-5 8482 df-6 8483 df-7 8484 df-8 8485 |
This theorem is referenced by: 8cn 8506 9re 8507 9pos 8524 6lt8 8605 5lt8 8606 4lt8 8607 3lt8 8608 2lt8 8609 1lt8 8610 8lt9 8611 7lt9 8612 8th4div3 8633 8lt10 9006 7lt10 9007 ef01bndlem 11043 cos2bnd 11047 |
Copyright terms: Public domain | W3C validator |