![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 6re | GIF version |
Description: The number 6 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
6re | ⊢ 6 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-6 8548 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5re 8564 | . . 3 ⊢ 5 ∈ ℝ | |
3 | 1re 7550 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7564 | . 2 ⊢ (5 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2161 | 1 ⊢ 6 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1439 (class class class)co 5668 ℝcr 7412 1c1 7414 + caddc 7416 5c5 8539 6c6 8540 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-4 1446 ax-17 1465 ax-ial 1473 ax-ext 2071 ax-1re 7502 ax-addrcl 7505 |
This theorem depends on definitions: df-bi 116 df-cleq 2082 df-clel 2085 df-2 8544 df-3 8545 df-4 8546 df-5 8547 df-6 8548 |
This theorem is referenced by: 6cn 8567 7re 8568 7pos 8587 4lt6 8659 3lt6 8660 2lt6 8661 1lt6 8662 6lt7 8663 5lt7 8664 6lt8 8670 5lt8 8671 6lt9 8678 5lt9 8679 8th4div3 8698 halfpm6th 8699 div4p1lem1div2 8732 6lt10 9073 5lt10 9074 efi4p 11071 resin4p 11072 recos4p 11073 ef01bndlem 11110 sin01bnd 11111 cos01bnd 11112 |
Copyright terms: Public domain | W3C validator |