![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 8re | GIF version |
Description: The number 8 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
8re | ⊢ 8 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-8 9015 | . 2 ⊢ 8 = (7 + 1) | |
2 | 7re 9033 | . . 3 ⊢ 7 ∈ ℝ | |
3 | 1re 7987 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 8001 | . 2 ⊢ (7 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2262 | 1 ⊢ 8 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2160 (class class class)co 5897 ℝcr 7841 1c1 7843 + caddc 7845 7c7 9006 8c8 9007 |
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 df-7 9014 df-8 9015 |
This theorem is referenced by: 8cn 9036 9re 9037 9pos 9054 6lt8 9141 5lt8 9142 4lt8 9143 3lt8 9144 2lt8 9145 1lt8 9146 8lt9 9147 7lt9 9148 8th4div3 9169 8lt10 9546 7lt10 9547 ef01bndlem 11799 cos2bnd 11803 slotstnscsi 12709 slotsdnscsi 12733 2lgsoddprmlem1 14931 2lgsoddprmlem2 14932 2lgsoddprmlem3a 14933 2lgsoddprmlem3b 14934 2lgsoddprmlem3c 14935 2lgsoddprmlem3d 14936 |
Copyright terms: Public domain | W3C validator |