Step | Hyp | Ref
| Expression |
1 | | simplll 533 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ ๐ด โ โ) |
2 | | simpllr 534 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ ๐ต โ โ) |
3 | | simpll 527 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 โค
๐ถ โง ๐ถ < ๐ท)) โ ๐ถ โ โ) |
4 | | simprl 529 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 โค
๐ถ โง ๐ถ < ๐ท)) โ 0 โค ๐ถ) |
5 | 3, 4 | jca 306 |
. . . . 5
โข (((๐ถ โ โ โง ๐ท โ โ) โง (0 โค
๐ถ โง ๐ถ < ๐ท)) โ (๐ถ โ โ โง 0 โค ๐ถ)) |
6 | 5 | ad2ant2l 508 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (๐ถ โ โ โง 0 โค ๐ถ)) |
7 | | ltle 8045 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ ๐ด โค ๐ต)) |
8 | 7 | imp 124 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด < ๐ต) โ ๐ด โค ๐ต) |
9 | 8 | adantrl 478 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ด โค ๐ต) |
10 | 9 | ad2ant2r 509 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ ๐ด โค ๐ต) |
11 | | lemul1a 8815 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)) |
12 | 1, 2, 6, 10, 11 | syl31anc 1241 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)) |
13 | | simplrl 535 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ถ โ โ) |
14 | | simplrr 536 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ท โ โ) |
15 | | simpllr 534 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ต โ โ) |
16 | | 0re 7957 |
. . . . . . . . . 10
โข 0 โ
โ |
17 | | lelttr 8046 |
. . . . . . . . . 10
โข ((0
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ ((0 โค ๐ด โง ๐ด < ๐ต) โ 0 < ๐ต)) |
18 | 16, 17 | mp3an1 1324 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 โค
๐ด โง ๐ด < ๐ต) โ 0 < ๐ต)) |
19 | 18 | imp 124 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ 0 < ๐ต) |
20 | 19 | adantlr 477 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ 0 < ๐ต) |
21 | | ltmul2 8813 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ท โ โ โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ถ < ๐ท โ (๐ต ยท ๐ถ) < (๐ต ยท ๐ท))) |
22 | 13, 14, 15, 20, 21 | syl112anc 1242 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ถ < ๐ท โ (๐ต ยท ๐ถ) < (๐ต ยท ๐ท))) |
23 | 22 | biimpa 296 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ถ โ
โ โง ๐ท โ
โ)) โง (0 โค ๐ด
โง ๐ด < ๐ต)) โง ๐ถ < ๐ท) โ (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) |
24 | 23 | anasss 399 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง ๐ถ < ๐ท)) โ (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) |
25 | 24 | adantrrl 486 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) |
26 | | remulcl 7939 |
. . . . . 6
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด ยท ๐ถ) โ โ) |
27 | 26 | ad2ant2r 509 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ด ยท ๐ถ) โ โ) |
28 | | remulcl 7939 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) โ โ) |
29 | 28 | ad2ant2lr 510 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต ยท ๐ถ) โ โ) |
30 | | remulcl 7939 |
. . . . . 6
โข ((๐ต โ โ โง ๐ท โ โ) โ (๐ต ยท ๐ท) โ โ) |
31 | 30 | ad2ant2l 508 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต ยท ๐ท) โ โ) |
32 | | lelttr 8046 |
. . . . 5
โข (((๐ด ยท ๐ถ) โ โ โง (๐ต ยท ๐ถ) โ โ โง (๐ต ยท ๐ท) โ โ) โ (((๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ) โง (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท))) |
33 | 27, 29, 31, 32 | syl3anc 1238 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ) โง (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท))) |
34 | 33 | adantr 276 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (((๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ) โง (๐ต ยท ๐ถ) < (๐ต ยท ๐ท)) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท))) |
35 | 12, 25, 34 | mp2and 433 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ((0 โค
๐ด โง ๐ด < ๐ต) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท)) |
36 | 35 | an4s 588 |
1
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท)) |