![]() |
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 8807 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5re 8823 | . . 3 ⊢ 5 ∈ ℝ | |
3 | 1re 7789 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7803 | . 2 ⊢ (5 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2213 | 1 ⊢ 6 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1481 (class class class)co 5782 ℝcr 7643 1c1 7645 + caddc 7647 5c5 8798 6c6 8799 |
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 |
This theorem is referenced by: 6cn 8826 7re 8827 7pos 8846 4lt6 8924 3lt6 8925 2lt6 8926 1lt6 8927 6lt7 8928 5lt7 8929 6lt8 8935 5lt8 8936 6lt9 8943 5lt9 8944 8th4div3 8963 halfpm6th 8964 div4p1lem1div2 8997 6lt10 9339 5lt10 9340 5recm6rec 9349 efi4p 11460 resin4p 11461 recos4p 11462 ef01bndlem 11499 sin01bnd 11500 cos01bnd 11501 sincos6thpi 12971 pigt3 12973 |
Copyright terms: Public domain | W3C validator |