![]() |
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 10455 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
5 | 1, 2, 3, 4 | mp3an 1534 | 1 ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2107 class class class wbr 4888 ℝcr 10273 < clt 10413 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 ax-un 7228 ax-resscn 10331 ax-pre-lttrn 10349 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-nel 3076 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-mpt 4968 df-id 5263 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-rn 5368 df-res 5369 df-ima 5370 df-iota 6101 df-fun 6139 df-fn 6140 df-f 6141 df-f1 6142 df-fo 6143 df-f1o 6144 df-fv 6145 df-er 8028 df-en 8244 df-dom 8245 df-sdom 8246 df-pnf 10415 df-mnf 10416 df-ltxr 10418 |
This theorem is referenced by: 1lt3 11559 2lt4 11561 1lt4 11562 3lt5 11564 2lt5 11565 1lt5 11566 4lt6 11568 3lt6 11569 2lt6 11570 1lt6 11571 5lt7 11573 4lt7 11574 3lt7 11575 2lt7 11576 1lt7 11577 6lt8 11579 5lt8 11580 4lt8 11581 3lt8 11582 2lt8 11583 1lt8 11584 7lt9 11586 6lt9 11587 5lt9 11588 4lt9 11589 3lt9 11590 2lt9 11591 1lt9 11592 8lt10 11983 7lt10 11984 6lt10 11985 5lt10 11986 4lt10 11987 3lt10 11988 2lt10 11989 1lt10 11990 sincos2sgn 15330 epos 15343 ene1 15346 dvdslelem 15442 oppcbas 16767 sralem 19578 zlmlem 20265 psgnodpmr 20335 tnglem 22856 xrhmph 23158 vitalilem4 23819 pipos 24654 logneg 24775 asin1 25076 reasinsin 25078 atan1 25110 log2le1 25133 bposlem8 25472 bposlem9 25473 chebbnd1lem2 25615 chebbnd1lem3 25616 chebbnd1 25617 mulog2sumlem2 25680 pntibndlem1 25734 pntlemb 25742 pntlemk 25751 ttglem 26229 cchhllem 26240 axlowdimlem16 26310 dp2ltc 30161 sgnnbi 31210 sgnpbi 31211 signswch 31242 hgt750lem 31335 hgt750lem2 31336 logi 32218 cnndvlem1 33114 bj-minftyccb 33706 bj-pinftynminfty 33708 asindmre 34125 fdc 34170 fourierdlem94 41354 fourierdlem102 41362 fourierdlem103 41363 fourierdlem104 41364 fourierdlem112 41372 fourierdlem113 41373 fourierdlem114 41374 fouriersw 41385 etransclem23 41411 |
Copyright terms: Public domain | W3C validator |