Step | Hyp | Ref
| Expression |
1 | | simplll 772 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ ๐ด โ โ) |
2 | | simpllr 773 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ ๐ต โ โ) |
3 | | simpll 764 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 โค
๐ถ โง ๐ถ < ๐ท)) โ ๐ถ โ โ) |
4 | | simprl 768 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 โค
๐ถ โง ๐ถ < ๐ท)) โ 0 โค ๐ถ) |
5 | 3, 4 | jca 511 |
. . . . 5
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 โค
๐ถ โง ๐ถ < ๐ท)) โ (๐ถ โ โ โง 0 โค ๐ถ)) |
6 | 5 | ad2ant2l 743 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (๐ถ โ โ โง 0 โค ๐ถ)) |
7 | | ltle 11306 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ ๐ด โค ๐ต)) |
8 | 7 | imp 406 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด < ๐ต) โ ๐ด โค ๐ต) |
9 | 8 | adantrl 713 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ด โค ๐ต) |
10 | 9 | ad2ant2r 744 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ ๐ด โค ๐ต) |
11 | | lemul1a 12072 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)) |
12 | 1, 2, 6, 10, 11 | syl31anc 1370 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)) |
13 | | simplrl 774 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ถ โ โ) |
14 | | simplrr 775 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ท โ โ) |
15 | | simpllr 773 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ต โ โ) |
16 | | 0re 11220 |
. . . . . . . . . 10
โข 0 โ
โ |
17 | | lelttr 11308 |
. . . . . . . . . 10
โข ((0
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ ((0 โค ๐ด โง ๐ด < ๐ต) โ 0 < ๐ต)) |
18 | 16, 17 | mp3an1 1444 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 โค
๐ด โง ๐ด < ๐ต) โ 0 < ๐ต)) |
19 | 18 | imp 406 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ 0 < ๐ต) |
20 | 19 | adantlr 712 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ 0 < ๐ต) |
21 | | ltmul2 12069 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ท โ โ โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ถ < ๐ท โ (๐ต ยท ๐ถ) < (๐ต ยท ๐ท))) |
22 | 13, 14, 15, 20, 21 | syl112anc 1371 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ถ < ๐ท โ (๐ต ยท ๐ถ) < (๐ต ยท ๐ท))) |
23 | 22 | biimpa 476 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ถ โ
โ โง ๐ท โ
โ)) โง (0 โค ๐ด
โง ๐ด < ๐ต)) โง ๐ถ < ๐ท) โ (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) |
24 | 23 | anasss 466 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง ๐ถ < ๐ท)) โ (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) |
25 | 24 | adantrrl 721 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) |
26 | | remulcl 11197 |
. . . . . 6
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด ยท ๐ถ) โ โ) |
27 | 26 | ad2ant2r 744 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ด ยท ๐ถ) โ โ) |
28 | | remulcl 11197 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) โ โ) |
29 | 28 | ad2ant2lr 745 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต ยท ๐ถ) โ โ) |
30 | | remulcl 11197 |
. . . . . 6
โข ((๐ต โ โ โง ๐ท โ โ) โ (๐ต ยท ๐ท) โ โ) |
31 | 30 | ad2ant2l 743 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต ยท ๐ท) โ โ) |
32 | | lelttr 11308 |
. . . . 5
โข (((๐ด ยท ๐ถ) โ โ โง (๐ต ยท ๐ถ) โ โ โง (๐ต ยท ๐ท) โ โ) โ (((๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ) โง (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท))) |
33 | 27, 29, 31, 32 | syl3anc 1368 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ) โง (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท))) |
34 | 33 | adantr 480 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (((๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ) โง (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท))) |
35 | 12, 25, 34 | mp2and 696 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท)) |
36 | 35 | an4s 657 |
1
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท)) |