![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 9re | Unicode version |
Description: The number 9 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
9re |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-9 9003 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 8re 9022 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 7974 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | readdcli 7988 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2262 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
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 7923 ax-addrcl 7926 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 df-clel 2185 df-2 8996 df-3 8997 df-4 8998 df-5 8999 df-6 9000 df-7 9001 df-8 9002 df-9 9003 |
This theorem is referenced by: 9cn 9025 7lt9 9135 6lt9 9136 5lt9 9137 4lt9 9138 3lt9 9139 2lt9 9140 1lt9 9141 9lt10 9532 8lt10 9533 0.999... 11547 cos2bnd 11786 sincos2sgn 11791 slotsdifplendx 12687 dsndxntsetndx 12697 unifndxntsetndx 12704 cnfldstr 13827 setsmsdsg 14377 2logb9irr 14786 2logb9irrap 14792 |
Copyright terms: Public domain | W3C validator |