Step | Hyp | Ref
| Expression |
1 | | xmulgt0 13266 |
. . . . . . . 8
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โ 0 < (๐ด ยทe ๐ต)) |
2 | 1 | an4s 658 |
. . . . . . 7
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง (0 < ๐ด โง 0 < ๐ต)) โ 0 < (๐ด ยทe ๐ต)) |
3 | | 0xr 11265 |
. . . . . . . 8
โข 0 โ
โ* |
4 | | xmulcl 13256 |
. . . . . . . . 9
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (๐ด ยทe ๐ต) โ
โ*) |
5 | 4 | adantr 481 |
. . . . . . . 8
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง (0 < ๐ด โง 0 < ๐ต)) โ (๐ด ยทe ๐ต) โ
โ*) |
6 | | xrltle 13132 |
. . . . . . . 8
โข ((0
โ โ* โง (๐ด ยทe ๐ต) โ โ*) โ (0 <
(๐ด ยทe
๐ต) โ 0 โค (๐ด ยทe ๐ต))) |
7 | 3, 5, 6 | sylancr 587 |
. . . . . . 7
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง (0 < ๐ด โง 0 < ๐ต)) โ (0 < (๐ด ยทe ๐ต) โ 0 โค (๐ด ยทe ๐ต))) |
8 | 2, 7 | mpd 15 |
. . . . . 6
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง (0 < ๐ด โง 0 < ๐ต)) โ 0 โค (๐ด ยทe ๐ต)) |
9 | 8 | ex 413 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ ((0 < ๐ด โง 0 < ๐ต) โ 0 โค (๐ด ยทe ๐ต))) |
10 | 9 | ad2ant2r 745 |
. . . 4
โข (((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โ ((0 < ๐ด โง 0 < ๐ต) โ 0 โค (๐ด ยทe ๐ต))) |
11 | 10 | impl 456 |
. . 3
โข
(((((๐ด โ
โ* โง 0 โค ๐ด) โง (๐ต โ โ* โง 0 โค
๐ต)) โง 0 < ๐ด) โง 0 < ๐ต) โ 0 โค (๐ด ยทe ๐ต)) |
12 | | 0le0 12317 |
. . . . 5
โข 0 โค
0 |
13 | | oveq2 7419 |
. . . . . . 7
โข (0 =
๐ต โ (๐ด ยทe 0) = (๐ด ยทe ๐ต)) |
14 | 13 | eqcomd 2738 |
. . . . . 6
โข (0 =
๐ต โ (๐ด ยทe ๐ต) = (๐ด ยทe 0)) |
15 | | xmul01 13250 |
. . . . . . 7
โข (๐ด โ โ*
โ (๐ด
ยทe 0) = 0) |
16 | 15 | ad2antrr 724 |
. . . . . 6
โข (((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โ (๐ด ยทe 0) =
0) |
17 | 14, 16 | sylan9eqr 2794 |
. . . . 5
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 = ๐ต) โ (๐ด ยทe ๐ต) = 0) |
18 | 12, 17 | breqtrrid 5186 |
. . . 4
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 = ๐ต) โ 0 โค (๐ด ยทe ๐ต)) |
19 | 18 | adantlr 713 |
. . 3
โข
(((((๐ด โ
โ* โง 0 โค ๐ด) โง (๐ต โ โ* โง 0 โค
๐ต)) โง 0 < ๐ด) โง 0 = ๐ต) โ 0 โค (๐ด ยทe ๐ต)) |
20 | | xrleloe 13127 |
. . . . . 6
โข ((0
โ โ* โง ๐ต โ โ*) โ (0 โค
๐ต โ (0 < ๐ต โจ 0 = ๐ต))) |
21 | 3, 20 | mpan 688 |
. . . . 5
โข (๐ต โ โ*
โ (0 โค ๐ต โ (0
< ๐ต โจ 0 = ๐ต))) |
22 | 21 | biimpa 477 |
. . . 4
โข ((๐ต โ โ*
โง 0 โค ๐ต) โ (0
< ๐ต โจ 0 = ๐ต)) |
23 | 22 | ad2antlr 725 |
. . 3
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 < ๐ด) โ (0 < ๐ต โจ 0 = ๐ต)) |
24 | 11, 19, 23 | mpjaodan 957 |
. 2
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 < ๐ด) โ 0 โค (๐ด ยทe ๐ต)) |
25 | | oveq1 7418 |
. . . . 5
โข (0 =
๐ด โ (0
ยทe ๐ต) =
(๐ด ยทe
๐ต)) |
26 | 25 | eqcomd 2738 |
. . . 4
โข (0 =
๐ด โ (๐ด ยทe ๐ต) = (0 ยทe ๐ต)) |
27 | | xmul02 13251 |
. . . . 5
โข (๐ต โ โ*
โ (0 ยทe ๐ต) = 0) |
28 | 27 | ad2antrl 726 |
. . . 4
โข (((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โ (0 ยทe ๐ต) = 0) |
29 | 26, 28 | sylan9eqr 2794 |
. . 3
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 = ๐ด) โ (๐ด ยทe ๐ต) = 0) |
30 | 12, 29 | breqtrrid 5186 |
. 2
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 = ๐ด) โ 0 โค (๐ด ยทe ๐ต)) |
31 | | xrleloe 13127 |
. . . . 5
โข ((0
โ โ* โง ๐ด โ โ*) โ (0 โค
๐ด โ (0 < ๐ด โจ 0 = ๐ด))) |
32 | 3, 31 | mpan 688 |
. . . 4
โข (๐ด โ โ*
โ (0 โค ๐ด โ (0
< ๐ด โจ 0 = ๐ด))) |
33 | 32 | biimpa 477 |
. . 3
โข ((๐ด โ โ*
โง 0 โค ๐ด) โ (0
< ๐ด โจ 0 = ๐ด)) |
34 | 33 | adantr 481 |
. 2
โข (((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โ (0 < ๐ด โจ 0 = ๐ด)) |
35 | 24, 30, 34 | mpjaodan 957 |
1
โข (((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โ 0 โค (๐ด ยทe ๐ต)) |