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 7082 | . 2 ⊢ 0 <ℝ 1 | |
2 | 0re 7119 | . . 3 ⊢ 0 ∈ ℝ | |
3 | 1re 7118 | . . 3 ⊢ 1 ∈ ℝ | |
4 | ltxrlt 7178 | . . 3 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 1 ↔ 0 <ℝ 1)) | |
5 | 2, 3, 4 | mp2an 416 | . 2 ⊢ (0 < 1 ↔ 0 <ℝ 1) |
6 | 1, 5 | mpbir 144 | 1 ⊢ 0 < 1 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 ∈ wcel 1433 class class class wbr 3785 ℝcr 6980 0cc0 6981 1c1 6982 <ℝ cltrr 6985 < clt 7153 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 576 ax-in2 577 ax-io 662 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-10 1436 ax-11 1437 ax-i12 1438 ax-bndl 1439 ax-4 1440 ax-13 1444 ax-14 1445 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 ax-sep 3896 ax-pow 3948 ax-pr 3964 ax-un 4188 ax-setind 4280 ax-cnex 7067 ax-resscn 7068 ax-1re 7070 ax-addrcl 7073 ax-0lt1 7082 ax-rnegex 7085 |
This theorem depends on definitions: df-bi 115 df-3an 921 df-tru 1287 df-fal 1290 df-nf 1390 df-sb 1686 df-eu 1944 df-mo 1945 df-clab 2068 df-cleq 2074 df-clel 2077 df-nfc 2208 df-ne 2246 df-nel 2340 df-ral 2353 df-rex 2354 df-rab 2357 df-v 2603 df-dif 2975 df-un 2977 df-in 2979 df-ss 2986 df-pw 3384 df-sn 3404 df-pr 3405 df-op 3407 df-uni 3602 df-br 3786 df-opab 3840 df-xp 4369 df-pnf 7155 df-mnf 7156 df-ltxr 7158 |
This theorem is referenced by: ine0 7498 0le1 7585 inelr 7684 1ap0 7690 eqneg 7820 ltp1 7922 ltm1 7924 recgt0 7928 mulgt1 7941 reclt1 7974 recgt1 7975 recgt1i 7976 recp1lt1 7977 recreclt 7978 nnge1 8062 nngt0 8064 0nnn 8066 nnrecgt0 8076 0ne1 8106 2pos 8130 3pos 8133 4pos 8136 5pos 8139 6pos 8140 7pos 8141 8pos 8142 9pos 8143 neg1lt0 8147 halflt1 8248 nn0p1gt0 8317 elnnnn0c 8333 elnnz1 8374 recnz 8440 1rp 8738 divlt1lt 8801 divle1le 8802 ledivge1le 8803 nnledivrp 8837 fz10 9065 fzpreddisj 9088 elfz1b 9107 modqfrac 9339 expgt1 9514 ltexp2a 9528 leexp2a 9529 expnbnd 9596 expnlbnd 9597 expnlbnd2 9598 expcanlem 9643 expcan 9644 bcn1 9685 resqrexlem1arp 9891 mulcn2 10151 nnoddm1d2 10310 dvdsnprmd 10507 |
Copyright terms: Public domain | W3C validator |