Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 0lt1 | GIF 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 | ⊢ 0 < 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-0lt1 7719 | . 2 ⊢ 0 <ℝ 1 | |
2 | 0re 7759 | . . 3 ⊢ 0 ∈ ℝ | |
3 | 1re 7758 | . . 3 ⊢ 1 ∈ ℝ | |
4 | ltxrlt 7823 | . . 3 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 1 ↔ 0 <ℝ 1)) | |
5 | 2, 3, 4 | mp2an 422 | . 2 ⊢ (0 < 1 ↔ 0 <ℝ 1) |
6 | 1, 5 | mpbir 145 | 1 ⊢ 0 < 1 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∈ wcel 1480 class class class wbr 3924 ℝcr 7612 0cc0 7613 1c1 7614 <ℝ cltrr 7617 < clt 7793 |
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 2119 ax-sep 4041 ax-pow 4093 ax-pr 4126 ax-un 4350 ax-setind 4447 ax-cnex 7704 ax-resscn 7705 ax-1re 7707 ax-addrcl 7710 ax-0lt1 7719 ax-rnegex 7722 |
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 2000 df-mo 2001 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-ne 2307 df-nel 2402 df-ral 2419 df-rex 2420 df-rab 2423 df-v 2683 df-dif 3068 df-un 3070 df-in 3072 df-ss 3079 df-pw 3507 df-sn 3528 df-pr 3529 df-op 3531 df-uni 3732 df-br 3925 df-opab 3985 df-xp 4540 df-pnf 7795 df-mnf 7796 df-ltxr 7798 |
This theorem is referenced by: ine0 8149 0le1 8236 inelr 8339 1ap0 8345 eqneg 8485 ltp1 8595 ltm1 8597 recgt0 8601 mulgt1 8614 reclt1 8647 recgt1 8648 recgt1i 8649 recp1lt1 8650 recreclt 8651 sup3exmid 8708 nnge1 8736 nngt0 8738 0nnn 8740 nnrecgt0 8751 0ne1 8780 2pos 8804 3pos 8807 4pos 8810 5pos 8813 6pos 8814 7pos 8815 8pos 8816 9pos 8817 neg1lt0 8821 halflt1 8930 nn0p1gt0 8999 elnnnn0c 9015 elnnz1 9070 recnz 9137 1rp 9438 divlt1lt 9504 divle1le 9505 ledivge1le 9506 nnledivrp 9546 fz10 9819 fzpreddisj 9844 elfz1b 9863 modqfrac 10103 expgt1 10324 ltexp2a 10338 leexp2a 10339 expnbnd 10408 expnlbnd 10409 expnlbnd2 10410 expcanlem 10455 expcan 10456 bcn1 10497 resqrexlem1arp 10770 mulcn2 11074 reccn2ap 11075 georeclim 11275 geoisumr 11280 cos1bnd 11455 sin01gt0 11457 sincos1sgn 11460 nnoddm1d2 11596 dvdsnprmd 11795 divdenle 11864 mopnex 12663 cos02pilt1 12921 |
Copyright terms: Public domain | W3C validator |