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 8785 | . 2 | |
2 | 7re 8803 | . . 3 | |
3 | 1re 7765 | . . 3 | |
4 | 2, 3 | readdcli 7779 | . 2 |
5 | 1, 4 | eqeltri 2212 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1480 (class class class)co 5774 cr 7619 c1 7621 caddc 7623 c7 8776 c8 8777 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-ext 2121 ax-1re 7714 ax-addrcl 7717 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 df-clel 2135 df-2 8779 df-3 8780 df-4 8781 df-5 8782 df-6 8783 df-7 8784 df-8 8785 |
This theorem is referenced by: 8cn 8806 9re 8807 9pos 8824 6lt8 8911 5lt8 8912 4lt8 8913 3lt8 8914 2lt8 8915 1lt8 8916 8lt9 8917 7lt9 8918 8th4div3 8939 8lt10 9313 7lt10 9314 ef01bndlem 11463 cos2bnd 11467 |
Copyright terms: Public domain | W3C validator |