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 8909 | . 2 | |
2 | 3re 8922 | . . 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 c3 8900 c4 8901 |
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 |
This theorem is referenced by: 4cn 8926 5re 8927 4ne0 8946 4ap0 8947 5pos 8948 2lt4 9021 1lt4 9022 4lt5 9023 3lt5 9024 2lt5 9025 1lt5 9026 4lt6 9028 3lt6 9029 4lt7 9034 3lt7 9035 4lt8 9041 3lt8 9042 4lt9 9049 3lt9 9050 8th4div3 9067 div4p1lem1div2 9101 4lt10 9448 3lt10 9449 eluz4eluz2 9496 fz0to4untppr 10049 fzo0to42pr 10145 fldiv4p1lem1div2 10230 faclbnd2 10644 4bc2eq6 10676 resqrexlemover 10938 resqrexlemcalc1 10942 resqrexlemcalc2 10943 resqrexlemcalc3 10944 resqrexlemnm 10946 resqrexlemga 10951 sqrt2gt1lt2 10977 amgm2 11046 ef01bndlem 11683 sin01bnd 11684 cos01bnd 11685 cos2bnd 11687 flodddiv4 11856 dveflem 13228 sin0pilem2 13244 sinhalfpilem 13253 sincosq1lem 13287 coseq0negpitopi 13298 tangtx 13300 sincos4thpi 13302 pigt3 13306 |
Copyright terms: Public domain | W3C validator |