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 7726 | . 2 | |
2 | 0re 7766 | . . 3 | |
3 | 1re 7765 | . . 3 | |
4 | ltxrlt 7830 | . . 3 | |
5 | 2, 3, 4 | mp2an 422 | . 2 |
6 | 1, 5 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wcel 1480 class class class wbr 3929 cr 7619 cc0 7620 c1 7621 cltrr 7624 clt 7800 |
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-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-cnex 7711 ax-resscn 7712 ax-1re 7714 ax-addrcl 7717 ax-0lt1 7726 ax-rnegex 7729 |
This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-nel 2404 df-ral 2421 df-rex 2422 df-rab 2425 df-v 2688 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-br 3930 df-opab 3990 df-xp 4545 df-pnf 7802 df-mnf 7803 df-ltxr 7805 |
This theorem is referenced by: ine0 8156 0le1 8243 inelr 8346 1ap0 8352 eqneg 8492 ltp1 8602 ltm1 8604 recgt0 8608 mulgt1 8621 reclt1 8654 recgt1 8655 recgt1i 8656 recp1lt1 8657 recreclt 8658 sup3exmid 8715 nnge1 8743 nngt0 8745 0nnn 8747 nnrecgt0 8758 0ne1 8787 2pos 8811 3pos 8814 4pos 8817 5pos 8820 6pos 8821 7pos 8822 8pos 8823 9pos 8824 neg1lt0 8828 halflt1 8937 nn0p1gt0 9006 elnnnn0c 9022 elnnz1 9077 recnz 9144 1rp 9445 divlt1lt 9511 divle1le 9512 ledivge1le 9513 nnledivrp 9553 fz10 9826 fzpreddisj 9851 elfz1b 9870 modqfrac 10110 expgt1 10331 ltexp2a 10345 leexp2a 10346 expnbnd 10415 expnlbnd 10416 expnlbnd2 10417 expcanlem 10462 expcan 10463 bcn1 10504 resqrexlem1arp 10777 mulcn2 11081 reccn2ap 11082 georeclim 11282 geoisumr 11287 cos1bnd 11466 sin01gt0 11468 sincos1sgn 11471 nnoddm1d2 11607 dvdsnprmd 11806 divdenle 11875 mopnex 12674 cos02pilt1 12932 |
Copyright terms: Public domain | W3C validator |