![]() |
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 8485 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5re 8501 | . . 3 ⊢ 5 ∈ ℝ | |
3 | 1re 7487 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7501 | . 2 ⊢ (5 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2160 | 1 ⊢ 6 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1438 (class class class)co 5652 ℝcr 7349 1c1 7351 + caddc 7353 5c5 8476 6c6 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 7439 ax-addrcl 7442 |
This theorem depends on definitions: df-bi 115 df-cleq 2081 df-clel 2084 df-2 8481 df-3 8482 df-4 8483 df-5 8484 df-6 8485 |
This theorem is referenced by: 6cn 8504 7re 8505 7pos 8524 4lt6 8596 3lt6 8597 2lt6 8598 1lt6 8599 6lt7 8600 5lt7 8601 6lt8 8607 5lt8 8608 6lt9 8615 5lt9 8616 8th4div3 8635 halfpm6th 8636 div4p1lem1div2 8669 6lt10 9010 5lt10 9011 efi4p 11008 resin4p 11009 recos4p 11010 ef01bndlem 11047 sin01bnd 11048 cos01bnd 11049 |
Copyright terms: Public domain | W3C validator |