![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0lt1 | Unicode version |
Description: 0 is less than 1. Theorem I.21 of [Apostol] p. 20. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 17-Jan-1997.) |
Ref | Expression |
---|---|
0lt1 |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-0lt1 7916 |
. 2
![]() ![]() ![]() ![]() | |
2 | 0re 7956 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 7955 |
. . 3
![]() ![]() ![]() ![]() | |
4 | ltxrlt 8021 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | mp2an 426 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | mpbir 146 |
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-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4121 ax-pow 4174 ax-pr 4209 ax-un 4433 ax-setind 4536 ax-cnex 7901 ax-resscn 7902 ax-1re 7904 ax-addrcl 7907 ax-0lt1 7916 ax-rnegex 7919 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2739 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-pw 3577 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3810 df-br 4004 df-opab 4065 df-xp 4632 df-pnf 7992 df-mnf 7993 df-ltxr 7995 |
This theorem is referenced by: ine0 8349 0le1 8436 inelr 8539 1ap0 8545 eqneg 8687 ltp1 8799 ltm1 8801 recgt0 8805 mulgt1 8818 reclt1 8851 recgt1 8852 recgt1i 8853 recp1lt1 8854 recreclt 8855 sup3exmid 8912 nnge1 8940 nngt0 8942 0nnn 8944 nnrecgt0 8955 0ne1 8984 2pos 9008 3pos 9011 4pos 9014 5pos 9017 6pos 9018 7pos 9019 8pos 9020 9pos 9021 neg1lt0 9025 halflt1 9134 nn0p1gt0 9203 elnnnn0c 9219 elnnz1 9274 recnz 9344 1rp 9655 divlt1lt 9722 divle1le 9723 ledivge1le 9724 nnledivrp 9764 fz10 10043 fzpreddisj 10068 elfz1b 10087 modqfrac 10334 expgt1 10555 ltexp2a 10569 leexp2a 10570 expnbnd 10640 expnlbnd 10641 expnlbnd2 10642 nn0ltexp2 10685 expcanlem 10690 expcan 10691 bcn1 10733 resqrexlem1arp 11009 mulcn2 11315 reccn2ap 11316 georeclim 11516 geoisumr 11521 cos1bnd 11762 sin01gt0 11764 sincos1sgn 11767 p1modz1 11796 nnoddm1d2 11909 dvdsnprmd 12119 divdenle 12191 mopnex 13936 reeff1olem 14123 cos02pilt1 14203 rplogcl 14231 cxplt 14267 cxple 14268 ltexp2 14291 apdiff 14716 |
Copyright terms: Public domain | W3C validator |