Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 8re | Unicode version |
Description: The number 8 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
8re |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-8 8913 | . 2 | |
2 | 7re 8931 | . . 3 | |
3 | 1re 7889 | . . 3 | |
4 | 2, 3 | readdcli 7903 | . 2 |
5 | 1, 4 | eqeltri 2237 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2135 (class class class)co 5836 cr 7743 c1 7745 caddc 7747 c7 8904 c8 8905 |
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 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-17 1513 ax-ial 1521 ax-ext 2146 ax-1re 7838 ax-addrcl 7841 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 df-clel 2160 df-2 8907 df-3 8908 df-4 8909 df-5 8910 df-6 8911 df-7 8912 df-8 8913 |
This theorem is referenced by: 8cn 8934 9re 8935 9pos 8952 6lt8 9039 5lt8 9040 4lt8 9041 3lt8 9042 2lt8 9043 1lt8 9044 8lt9 9045 7lt9 9046 8th4div3 9067 8lt10 9444 7lt10 9445 ef01bndlem 11683 cos2bnd 11687 |
Copyright terms: Public domain | W3C validator |