![]() |
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 8685 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3re 8698 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 7683 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | readdcli 7697 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2185 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-4 1468 ax-17 1487 ax-ial 1495 ax-ext 2095 ax-1re 7633 ax-addrcl 7636 |
This theorem depends on definitions: df-bi 116 df-cleq 2106 df-clel 2109 df-2 8683 df-3 8684 df-4 8685 |
This theorem is referenced by: 4cn 8702 5re 8703 4ne0 8722 4ap0 8723 5pos 8724 2lt4 8791 1lt4 8792 4lt5 8793 3lt5 8794 2lt5 8795 1lt5 8796 4lt6 8798 3lt6 8799 4lt7 8804 3lt7 8805 4lt8 8811 3lt8 8812 4lt9 8819 3lt9 8820 8th4div3 8837 div4p1lem1div2 8871 4lt10 9215 3lt10 9216 fzo0to42pr 9884 fldiv4p1lem1div2 9965 faclbnd2 10375 4bc2eq6 10407 resqrexlemover 10668 resqrexlemcalc1 10672 resqrexlemcalc2 10673 resqrexlemcalc3 10674 resqrexlemnm 10676 resqrexlemga 10681 sqrt2gt1lt2 10707 amgm2 10776 ef01bndlem 11308 sin01bnd 11309 cos01bnd 11310 cos2bnd 11312 flodddiv4 11473 |
Copyright terms: Public domain | W3C validator |