Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . . 5
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ ๐ท โ โ) |
2 | | 0re 11216 |
. . . . . . . 8
โข 0 โ
โ |
3 | | ltletr 11306 |
. . . . . . . 8
โข ((0
โ โ โง ๐ถ
โ โ โง ๐ท
โ โ) โ ((0 < ๐ถ โง ๐ถ โค ๐ท) โ 0 < ๐ท)) |
4 | 2, 3 | mp3an1 1449 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ท โ โ) โ ((0 <
๐ถ โง ๐ถ โค ๐ท) โ 0 < ๐ท)) |
5 | 4 | imp 408 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ 0 < ๐ท) |
6 | 5 | gt0ne0d 11778 |
. . . . 5
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ ๐ท โ 0) |
7 | 1, 6 | rereccld 12041 |
. . . 4
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ (1 / ๐ท) โ โ) |
8 | | gt0ne0 11679 |
. . . . . 6
โข ((๐ถ โ โ โง 0 <
๐ถ) โ ๐ถ โ 0) |
9 | | rereccl 11932 |
. . . . . 6
โข ((๐ถ โ โ โง ๐ถ โ 0) โ (1 / ๐ถ) โ
โ) |
10 | 8, 9 | syldan 592 |
. . . . 5
โข ((๐ถ โ โ โง 0 <
๐ถ) โ (1 / ๐ถ) โ
โ) |
11 | 10 | ad2ant2r 746 |
. . . 4
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ (1 / ๐ถ) โ โ) |
12 | | recgt0 12060 |
. . . . . . 7
โข ((๐ท โ โ โง 0 <
๐ท) โ 0 < (1 / ๐ท)) |
13 | 1, 5, 12 | syl2anc 585 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ 0 < (1 / ๐ท)) |
14 | | ltle 11302 |
. . . . . . 7
โข ((0
โ โ โง (1 / ๐ท) โ โ) โ (0 < (1 / ๐ท) โ 0 โค (1 / ๐ท))) |
15 | 2, 7, 14 | sylancr 588 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ (0 < (1 / ๐ท) โ 0 โค (1 / ๐ท))) |
16 | 13, 15 | mpd 15 |
. . . . 5
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ 0 โค (1 / ๐ท)) |
17 | | simprr 772 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ ๐ถ โค ๐ท) |
18 | | id 22 |
. . . . . . . 8
โข ((๐ถ โ โ โง 0 <
๐ถ) โ (๐ถ โ โ โง 0 <
๐ถ)) |
19 | 18 | ad2ant2r 746 |
. . . . . . 7
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ (๐ถ โ โ โง 0 < ๐ถ)) |
20 | | lerec 12097 |
. . . . . . 7
โข (((๐ถ โ โ โง 0 <
๐ถ) โง (๐ท โ โ โง 0 < ๐ท)) โ (๐ถ โค ๐ท โ (1 / ๐ท) โค (1 / ๐ถ))) |
21 | 19, 1, 5, 20 | syl12anc 836 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ (๐ถ โค ๐ท โ (1 / ๐ท) โค (1 / ๐ถ))) |
22 | 17, 21 | mpbid 231 |
. . . . 5
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ (1 / ๐ท) โค (1 / ๐ถ)) |
23 | 16, 22 | jca 513 |
. . . 4
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ (0 โค (1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ))) |
24 | 7, 11, 23 | jca31 516 |
. . 3
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) |
25 | | simplll 774 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ ๐ด โ โ) |
26 | | simplrl 776 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ 0 โค ๐ด) |
27 | | simpllr 775 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ ๐ต โ โ) |
28 | 25, 26, 27 | jca31 516 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ ((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ)) |
29 | | simprll 778 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ (1 / ๐ท) โ โ) |
30 | | simprrl 780 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ 0 โค (1 / ๐ท)) |
31 | 29, 30 | jca 513 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ ((1 / ๐ท) โ โ โง 0 โค (1 / ๐ท))) |
32 | | simprlr 779 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ (1 / ๐ถ) โ โ) |
33 | 28, 31, 32 | jca32 517 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ (((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ) โง (((1 / ๐ท) โ โ โง 0 โค (1
/ ๐ท)) โง (1 / ๐ถ) โ
โ))) |
34 | | simplrr 777 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ ๐ด โค ๐ต) |
35 | | simprrr 781 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ (1 / ๐ท) โค (1 / ๐ถ)) |
36 | 34, 35 | jca 513 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ (๐ด โค ๐ต โง (1 / ๐ท) โค (1 / ๐ถ))) |
37 | | lemul12a 12072 |
. . . 4
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ) โง (((1 / ๐ท) โ โ โง 0 โค (1
/ ๐ท)) โง (1 / ๐ถ) โ โ)) โ
((๐ด โค ๐ต โง (1 / ๐ท) โค (1 / ๐ถ)) โ (๐ด ยท (1 / ๐ท)) โค (๐ต ยท (1 / ๐ถ)))) |
38 | 33, 36, 37 | sylc 65 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง (((1 / ๐ท) โ โ โง (1 / ๐ถ) โ โ) โง (0 โค
(1 / ๐ท) โง (1 / ๐ท) โค (1 / ๐ถ)))) โ (๐ด ยท (1 / ๐ท)) โค (๐ต ยท (1 / ๐ถ))) |
39 | 24, 38 | sylan2 594 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 < ๐ถ โง ๐ถ โค ๐ท))) โ (๐ด ยท (1 / ๐ท)) โค (๐ต ยท (1 / ๐ถ))) |
40 | | recn 11200 |
. . . . 5
โข (๐ด โ โ โ ๐ด โ
โ) |
41 | 40 | adantr 482 |
. . . 4
โข ((๐ด โ โ โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท))) โ ๐ด โ โ) |
42 | | recn 11200 |
. . . . . 6
โข (๐ท โ โ โ ๐ท โ
โ) |
43 | 42 | ad2antlr 726 |
. . . . 5
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท)) โ ๐ท โ โ) |
44 | 43 | adantl 483 |
. . . 4
โข ((๐ด โ โ โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท))) โ ๐ท โ โ) |
45 | 6 | adantl 483 |
. . . 4
โข ((๐ด โ โ โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท))) โ ๐ท โ 0) |
46 | 41, 44, 45 | divrecd 11993 |
. . 3
โข ((๐ด โ โ โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท))) โ (๐ด / ๐ท) = (๐ด ยท (1 / ๐ท))) |
47 | 46 | ad4ant14 751 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 < ๐ถ โง ๐ถ โค ๐ท))) โ (๐ด / ๐ท) = (๐ด ยท (1 / ๐ท))) |
48 | | recn 11200 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
49 | 48 | adantr 482 |
. . . . . 6
โข ((๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โ ๐ต โ
โ) |
50 | | recn 11200 |
. . . . . . 7
โข (๐ถ โ โ โ ๐ถ โ
โ) |
51 | 50 | ad2antrl 727 |
. . . . . 6
โข ((๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โ ๐ถ โ
โ) |
52 | 8 | adantl 483 |
. . . . . 6
โข ((๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โ ๐ถ โ 0) |
53 | 49, 51, 52 | divrecd 11993 |
. . . . 5
โข ((๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โ (๐ต / ๐ถ) = (๐ต ยท (1 / ๐ถ))) |
54 | 53 | adantrrr 724 |
. . . 4
โข ((๐ต โ โ โง (๐ถ โ โ โง (0 <
๐ถ โง ๐ถ โค ๐ท))) โ (๐ต / ๐ถ) = (๐ต ยท (1 / ๐ถ))) |
55 | 54 | adantrlr 722 |
. . 3
โข ((๐ต โ โ โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 <
๐ถ โง ๐ถ โค ๐ท))) โ (๐ต / ๐ถ) = (๐ต ยท (1 / ๐ถ))) |
56 | 55 | ad4ant24 753 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 < ๐ถ โง ๐ถ โค ๐ท))) โ (๐ต / ๐ถ) = (๐ต ยท (1 / ๐ถ))) |
57 | 39, 47, 56 | 3brtr4d 5181 |
1
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด โค ๐ต)) โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 < ๐ถ โง ๐ถ โค ๐ท))) โ (๐ด / ๐ท) โค (๐ต / ๐ถ)) |