![]() |
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 9010 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3re 9023 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 7986 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | readdcli 8000 |
. 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 7935 ax-addrcl 7938 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 df-clel 2185 df-2 9008 df-3 9009 df-4 9010 |
This theorem is referenced by: 4cn 9027 5re 9028 4ne0 9047 4ap0 9048 5pos 9049 2lt4 9122 1lt4 9123 4lt5 9124 3lt5 9125 2lt5 9126 1lt5 9127 4lt6 9129 3lt6 9130 4lt7 9135 3lt7 9136 4lt8 9142 3lt8 9143 4lt9 9150 3lt9 9151 8th4div3 9168 div4p1lem1div2 9202 4lt10 9549 3lt10 9550 eluz4eluz2 9597 fz0to4untppr 10154 fzo0to42pr 10250 fldiv4p1lem1div2 10336 faclbnd2 10754 4bc2eq6 10786 resqrexlemover 11051 resqrexlemcalc1 11055 resqrexlemcalc2 11056 resqrexlemcalc3 11057 resqrexlemnm 11059 resqrexlemga 11064 sqrt2gt1lt2 11090 amgm2 11159 ef01bndlem 11796 sin01bnd 11797 cos01bnd 11798 cos2bnd 11800 flodddiv4 11971 4sqlem12 12434 tsetndxnstarvndx 12705 slotsdifplendx 12721 slotsdifdsndx 12732 slotsdifunifndx 12739 cnfldstr 13866 dveflem 14644 sin0pilem2 14660 sinhalfpilem 14669 sincosq1lem 14703 coseq0negpitopi 14714 tangtx 14716 sincos4thpi 14718 pigt3 14722 |
Copyright terms: Public domain | W3C validator |