Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 4re | Unicode version |
Description: The number 4 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
4re |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-4 8774 | . 2 | |
2 | 3re 8787 | . . 3 | |
3 | 1re 7758 | . . 3 | |
4 | 2, 3 | readdcli 7772 | . 2 |
5 | 1, 4 | eqeltri 2210 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1480 (class class class)co 5767 cr 7612 c1 7614 caddc 7616 c3 8765 c4 8766 |
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 2119 ax-1re 7707 ax-addrcl 7710 |
This theorem depends on definitions: df-bi 116 df-cleq 2130 df-clel 2133 df-2 8772 df-3 8773 df-4 8774 |
This theorem is referenced by: 4cn 8791 5re 8792 4ne0 8811 4ap0 8812 5pos 8813 2lt4 8886 1lt4 8887 4lt5 8888 3lt5 8889 2lt5 8890 1lt5 8891 4lt6 8893 3lt6 8894 4lt7 8899 3lt7 8900 4lt8 8906 3lt8 8907 4lt9 8914 3lt9 8915 8th4div3 8932 div4p1lem1div2 8966 4lt10 9310 3lt10 9311 fzo0to42pr 9990 fldiv4p1lem1div2 10071 faclbnd2 10481 4bc2eq6 10513 resqrexlemover 10775 resqrexlemcalc1 10779 resqrexlemcalc2 10780 resqrexlemcalc3 10781 resqrexlemnm 10783 resqrexlemga 10788 sqrt2gt1lt2 10814 amgm2 10883 ef01bndlem 11452 sin01bnd 11453 cos01bnd 11454 cos2bnd 11456 flodddiv4 11620 dveflem 12844 sin0pilem2 12852 sinhalfpilem 12861 sincosq1lem 12895 coseq0negpitopi 12906 tangtx 12908 sincos4thpi 12910 pigt3 12914 |
Copyright terms: Public domain | W3C validator |