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 8896 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5re 8912 | . . 3 ⊢ 5 ∈ ℝ | |
3 | 1re 7877 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7891 | . 2 ⊢ (5 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2230 | 1 ⊢ 6 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2128 (class class class)co 5824 ℝcr 7731 1c1 7733 + caddc 7735 5c5 8887 6c6 8888 |
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 1427 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-4 1490 ax-17 1506 ax-ial 1514 ax-ext 2139 ax-1re 7826 ax-addrcl 7829 |
This theorem depends on definitions: df-bi 116 df-cleq 2150 df-clel 2153 df-2 8892 df-3 8893 df-4 8894 df-5 8895 df-6 8896 |
This theorem is referenced by: 6cn 8915 7re 8916 7pos 8935 4lt6 9013 3lt6 9014 2lt6 9015 1lt6 9016 6lt7 9017 5lt7 9018 6lt8 9024 5lt8 9025 6lt9 9032 5lt9 9033 8th4div3 9052 halfpm6th 9053 div4p1lem1div2 9086 6lt10 9428 5lt10 9429 5recm6rec 9438 efi4p 11614 resin4p 11615 recos4p 11616 ef01bndlem 11653 sin01bnd 11654 cos01bnd 11655 sincos6thpi 13174 pigt3 13176 |
Copyright terms: Public domain | W3C validator |