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 8941 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5re 8957 | . . 3 ⊢ 5 ∈ ℝ | |
3 | 1re 7919 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7933 | . 2 ⊢ (5 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2243 | 1 ⊢ 6 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2141 (class class class)co 5853 ℝcr 7773 1c1 7775 + caddc 7777 5c5 8932 6c6 8933 |
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 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-ext 2152 ax-1re 7868 ax-addrcl 7871 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-clel 2166 df-2 8937 df-3 8938 df-4 8939 df-5 8940 df-6 8941 |
This theorem is referenced by: 6cn 8960 7re 8961 7pos 8980 4lt6 9058 3lt6 9059 2lt6 9060 1lt6 9061 6lt7 9062 5lt7 9063 6lt8 9069 5lt8 9070 6lt9 9077 5lt9 9078 8th4div3 9097 halfpm6th 9098 div4p1lem1div2 9131 6lt10 9476 5lt10 9477 5recm6rec 9486 efi4p 11680 resin4p 11681 recos4p 11682 ef01bndlem 11719 sin01bnd 11720 cos01bnd 11721 sincos6thpi 13557 pigt3 13559 |
Copyright terms: Public domain | W3C validator |