![]() |
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 9013 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5re 9029 | . . 3 ⊢ 5 ∈ ℝ | |
3 | 1re 7987 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 8001 | . 2 ⊢ (5 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2262 | 1 ⊢ 6 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2160 (class class class)co 5897 ℝcr 7841 1c1 7843 + caddc 7845 5c5 9004 6c6 9005 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 ax-ext 2171 ax-1re 7936 ax-addrcl 7939 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 df-clel 2185 df-2 9009 df-3 9010 df-4 9011 df-5 9012 df-6 9013 |
This theorem is referenced by: 6cn 9032 7re 9033 7pos 9052 4lt6 9130 3lt6 9131 2lt6 9132 1lt6 9133 6lt7 9134 5lt7 9135 6lt8 9141 5lt8 9142 6lt9 9149 5lt9 9150 8th4div3 9169 halfpm6th 9170 div4p1lem1div2 9203 6lt10 9548 5lt10 9549 5recm6rec 9558 efi4p 11760 resin4p 11761 recos4p 11762 ef01bndlem 11799 sin01bnd 11800 cos01bnd 11801 slotsdifipndx 12689 slotstnscsi 12709 plendxnvscandx 12723 slotsdnscsi 12733 sincos6thpi 14740 pigt3 14742 |
Copyright terms: Public domain | W3C validator |