Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . 5
โข ((๐ โ โ โง ๐
โ โ+)
โ ๐ โ
โ) |
2 | | rpre 12930 |
. . . . . 6
โข (๐
โ โ+
โ ๐
โ
โ) |
3 | | remulcl 11143 |
. . . . . 6
โข ((๐ โ โ โง ๐
โ โ) โ (๐ ยท ๐
) โ โ) |
4 | 2, 3 | sylan2 594 |
. . . . 5
โข ((๐ โ โ โง ๐
โ โ+)
โ (๐ ยท ๐
) โ
โ) |
5 | 1, 4 | 2thd 265 |
. . . 4
โข ((๐ โ โ โง ๐
โ โ+)
โ (๐ โ โ
โ (๐ ยท ๐
) โ
โ)) |
6 | 5 | adantl 483 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐
โ โ+))
โ (๐ โ โ
โ (๐ ยท ๐
) โ
โ)) |
7 | | elrp 12924 |
. . . . . . 7
โข (๐
โ โ+
โ (๐
โ โ
โง 0 < ๐
)) |
8 | | lemul1 12014 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ โง (๐
โ โ โง 0 <
๐
)) โ (๐ด โค ๐ โ (๐ด ยท ๐
) โค (๐ ยท ๐
))) |
9 | 7, 8 | syl3an3b 1406 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ โง ๐
โ โ+)
โ (๐ด โค ๐ โ (๐ด ยท ๐
) โค (๐ ยท ๐
))) |
10 | 9 | 3expb 1121 |
. . . . 5
โข ((๐ด โ โ โง (๐ โ โ โง ๐
โ โ+))
โ (๐ด โค ๐ โ (๐ด ยท ๐
) โค (๐ ยท ๐
))) |
11 | 10 | adantlr 714 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐
โ โ+))
โ (๐ด โค ๐ โ (๐ด ยท ๐
) โค (๐ ยท ๐
))) |
12 | | iccdil.1 |
. . . . 5
โข (๐ด ยท ๐
) = ๐ถ |
13 | 12 | breq1i 5117 |
. . . 4
โข ((๐ด ยท ๐
) โค (๐ ยท ๐
) โ ๐ถ โค (๐ ยท ๐
)) |
14 | 11, 13 | bitrdi 287 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐
โ โ+))
โ (๐ด โค ๐ โ ๐ถ โค (๐ ยท ๐
))) |
15 | | lemul1 12014 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ต โ โ โง (๐
โ โ โง 0 <
๐
)) โ (๐ โค ๐ต โ (๐ ยท ๐
) โค (๐ต ยท ๐
))) |
16 | 7, 15 | syl3an3b 1406 |
. . . . . . 7
โข ((๐ โ โ โง ๐ต โ โ โง ๐
โ โ+)
โ (๐ โค ๐ต โ (๐ ยท ๐
) โค (๐ต ยท ๐
))) |
17 | 16 | 3expb 1121 |
. . . . . 6
โข ((๐ โ โ โง (๐ต โ โ โง ๐
โ โ+))
โ (๐ โค ๐ต โ (๐ ยท ๐
) โค (๐ต ยท ๐
))) |
18 | 17 | an12s 648 |
. . . . 5
โข ((๐ต โ โ โง (๐ โ โ โง ๐
โ โ+))
โ (๐ โค ๐ต โ (๐ ยท ๐
) โค (๐ต ยท ๐
))) |
19 | 18 | adantll 713 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐
โ โ+))
โ (๐ โค ๐ต โ (๐ ยท ๐
) โค (๐ต ยท ๐
))) |
20 | | iccdil.2 |
. . . . 5
โข (๐ต ยท ๐
) = ๐ท |
21 | 20 | breq2i 5118 |
. . . 4
โข ((๐ ยท ๐
) โค (๐ต ยท ๐
) โ (๐ ยท ๐
) โค ๐ท) |
22 | 19, 21 | bitrdi 287 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐
โ โ+))
โ (๐ โค ๐ต โ (๐ ยท ๐
) โค ๐ท)) |
23 | 6, 14, 22 | 3anbi123d 1437 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐
โ โ+))
โ ((๐ โ โ
โง ๐ด โค ๐ โง ๐ โค ๐ต) โ ((๐ ยท ๐
) โ โ โง ๐ถ โค (๐ ยท ๐
) โง (๐ ยท ๐
) โค ๐ท))) |
24 | | elicc2 13336 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ โ (๐ด[,]๐ต) โ (๐ โ โ โง ๐ด โค ๐ โง ๐ โค ๐ต))) |
25 | 24 | adantr 482 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐
โ โ+))
โ (๐ โ (๐ด[,]๐ต) โ (๐ โ โ โง ๐ด โค ๐ โง ๐ โค ๐ต))) |
26 | | remulcl 11143 |
. . . . . . 7
โข ((๐ด โ โ โง ๐
โ โ) โ (๐ด ยท ๐
) โ โ) |
27 | 12, 26 | eqeltrrid 2843 |
. . . . . 6
โข ((๐ด โ โ โง ๐
โ โ) โ ๐ถ โ
โ) |
28 | | remulcl 11143 |
. . . . . . 7
โข ((๐ต โ โ โง ๐
โ โ) โ (๐ต ยท ๐
) โ โ) |
29 | 20, 28 | eqeltrrid 2843 |
. . . . . 6
โข ((๐ต โ โ โง ๐
โ โ) โ ๐ท โ
โ) |
30 | | elicc2 13336 |
. . . . . 6
โข ((๐ถ โ โ โง ๐ท โ โ) โ ((๐ ยท ๐
) โ (๐ถ[,]๐ท) โ ((๐ ยท ๐
) โ โ โง ๐ถ โค (๐ ยท ๐
) โง (๐ ยท ๐
) โค ๐ท))) |
31 | 27, 29, 30 | syl2an 597 |
. . . . 5
โข (((๐ด โ โ โง ๐
โ โ) โง (๐ต โ โ โง ๐
โ โ)) โ ((๐ ยท ๐
) โ (๐ถ[,]๐ท) โ ((๐ ยท ๐
) โ โ โง ๐ถ โค (๐ ยท ๐
) โง (๐ ยท ๐
) โค ๐ท))) |
32 | 31 | anandirs 678 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐
โ โ) โ ((๐ ยท ๐
) โ (๐ถ[,]๐ท) โ ((๐ ยท ๐
) โ โ โง ๐ถ โค (๐ ยท ๐
) โง (๐ ยท ๐
) โค ๐ท))) |
33 | 2, 32 | sylan2 594 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐
โ โ+)
โ ((๐ ยท ๐
) โ (๐ถ[,]๐ท) โ ((๐ ยท ๐
) โ โ โง ๐ถ โค (๐ ยท ๐
) โง (๐ ยท ๐
) โค ๐ท))) |
34 | 33 | adantrl 715 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐
โ โ+))
โ ((๐ ยท ๐
) โ (๐ถ[,]๐ท) โ ((๐ ยท ๐
) โ โ โง ๐ถ โค (๐ ยท ๐
) โง (๐ ยท ๐
) โค ๐ท))) |
35 | 23, 25, 34 | 3bitr4d 311 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐
โ โ+))
โ (๐ โ (๐ด[,]๐ต) โ (๐ ยท ๐
) โ (๐ถ[,]๐ท))) |