![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lttri | Structured version Visualization version GIF 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 11327 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
5 | 1, 2, 3, 4 | mp3an 1457 | 1 ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 class class class wbr 5149 ℝcr 11144 < clt 11285 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741 ax-resscn 11202 ax-pre-lttrn 11220 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-nel 3036 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-fv 6557 df-er 8725 df-en 8965 df-dom 8966 df-sdom 8967 df-pnf 11287 df-mnf 11288 df-ltxr 11290 |
This theorem is referenced by: 1lt3 12423 2lt4 12425 1lt4 12426 3lt5 12428 2lt5 12429 1lt5 12430 4lt6 12432 3lt6 12433 2lt6 12434 1lt6 12435 5lt7 12437 4lt7 12438 3lt7 12439 2lt7 12440 1lt7 12441 6lt8 12443 5lt8 12444 4lt8 12445 3lt8 12446 2lt8 12447 1lt8 12448 7lt9 12450 6lt9 12451 5lt9 12452 4lt9 12453 3lt9 12454 2lt9 12455 1lt9 12456 8lt10 12847 7lt10 12848 6lt10 12849 5lt10 12850 4lt10 12851 3lt10 12852 2lt10 12853 1lt10 12854 sincos2sgn 16179 epos 16192 ene1 16195 dvdslelem 16294 oppcbasOLD 17708 sralemOLD 21079 zlmlemOLD 21465 psgnodpmr 21544 tnglemOLD 24599 xrhmph 24921 vitalilem4 25589 pipos 26445 logi 26571 logneg 26572 asin1 26876 reasinsin 26878 atan1 26910 log2le1 26932 bposlem8 27274 bposlem9 27275 chebbnd1lem2 27453 chebbnd1lem3 27454 chebbnd1 27455 mulog2sumlem2 27518 pntibndlem1 27572 pntlemb 27580 pntlemk 27589 ttglemOLD 28759 cchhllemOLD 28775 axlowdimlem16 28845 dp2ltc 32700 sgnnbi 34298 sgnpbi 34299 signswch 34326 hgt750lem 34416 hgt750lem2 34417 cnndvlem1 36145 bj-minftyccb 36837 bj-pinftynminfty 36839 irrdiff 36938 asindmre 37309 fdc 37351 sn-0ne2 42098 fourierdlem94 45728 fourierdlem102 45736 fourierdlem103 45737 fourierdlem104 45738 fourierdlem112 45746 fourierdlem113 45747 fourierdlem114 45748 fouriersw 45759 etransclem23 45785 |
Copyright terms: Public domain | W3C validator |