![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lttri | Structured version Visualization version Unicode version |
Description: 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
Ref | Expression |
---|---|
lt.1 |
![]() ![]() ![]() ![]() |
lt.2 |
![]() ![]() ![]() ![]() |
lt.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
lttri |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lt.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | lt.2 |
. 2
![]() ![]() ![]() ![]() | |
3 | lt.3 |
. 2
![]() ![]() ![]() ![]() | |
4 | lttr 9736 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | mp3an 1373 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-resscn 9622 ax-pre-lttrn 9640 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4417 df-opab 4476 df-mpt 4477 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-er 7389 df-en 7596 df-dom 7597 df-sdom 7598 df-pnf 9703 df-mnf 9704 df-ltxr 9706 |
This theorem is referenced by: 1lt3 10807 2lt4 10809 1lt4 10810 3lt5 10812 2lt5 10813 1lt5 10814 4lt6 10816 3lt6 10817 2lt6 10818 1lt6 10819 5lt7 10821 4lt7 10822 3lt7 10823 2lt7 10824 1lt7 10825 6lt8 10827 5lt8 10828 4lt8 10829 3lt8 10830 2lt8 10831 1lt8 10832 7lt9 10834 6lt9 10835 5lt9 10836 4lt9 10837 3lt9 10838 2lt9 10839 1lt9 10840 8lt10 10842 7lt10 10843 6lt10 10844 5lt10 10845 4lt10 10846 3lt10 10847 2lt10 10848 1lt10 10849 sincos2sgn 14297 epos 14308 ene1 14311 dvdslelem 14398 oppcbas 15672 sralem 18449 zlmlem 19137 psgnodpmr 19207 tnglem 21697 xrhmph 22024 vitalilem4 22618 pipos 23464 logneg 23586 asin1 23869 reasinsin 23871 atan1 23903 log2le1 23925 bposlem8 24268 bposlem9 24269 chebbnd1lem2 24357 chebbnd1lem3 24358 chebbnd1 24359 mulog2sumlem2 24422 pntibndlem1 24476 pntlemb 24484 pntlemk 24493 ttglem 24955 cchhllem 24966 axlowdimlem16 25036 sgnnbi 29465 sgnpbi 29466 signswch 29499 logi 30419 bj-minftyccb 31712 bj-pinftynminfty 31714 asindmre 32072 fdc 32119 fourierdlem94 38102 fourierdlem102 38110 fourierdlem103 38111 fourierdlem104 38112 fourierdlem112 38120 fourierdlem113 38121 fourierdlem114 38122 fouriersw 38133 etransclem23 38160 |
Copyright terms: Public domain | W3C validator |