Step | Hyp | Ref
| Expression |
1 | | xmulgt0 13262 |
. . . . . . . 8
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โ 0 < (๐ด ยทe ๐ต)) |
2 | 1 | an4s 659 |
. . . . . . 7
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง (0 < ๐ด โง 0 < ๐ต)) โ 0 < (๐ด ยทe ๐ต)) |
3 | | 0xr 11261 |
. . . . . . . 8
โข 0 โ
โ* |
4 | | xmulcl 13252 |
. . . . . . . . 9
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (๐ด ยทe ๐ต) โ
โ*) |
5 | 4 | adantr 482 |
. . . . . . . 8
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง (0 < ๐ด โง 0 < ๐ต)) โ (๐ด ยทe ๐ต) โ
โ*) |
6 | | xrltle 13128 |
. . . . . . . 8
โข ((0
โ โ* โง (๐ด ยทe ๐ต) โ โ*) โ (0 <
(๐ด ยทe
๐ต) โ 0 โค (๐ด ยทe ๐ต))) |
7 | 3, 5, 6 | sylancr 588 |
. . . . . . 7
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง (0 < ๐ด โง 0 < ๐ต)) โ (0 < (๐ด ยทe ๐ต) โ 0 โค (๐ด ยทe ๐ต))) |
8 | 2, 7 | mpd 15 |
. . . . . 6
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง (0 < ๐ด โง 0 < ๐ต)) โ 0 โค (๐ด ยทe ๐ต)) |
9 | 8 | ex 414 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ ((0 < ๐ด โง 0 < ๐ต) โ 0 โค (๐ด ยทe ๐ต))) |
10 | 9 | ad2ant2r 746 |
. . . 4
โข (((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โ ((0 < ๐ด โง 0 < ๐ต) โ 0 โค (๐ด ยทe ๐ต))) |
11 | 10 | impl 457 |
. . 3
โข
(((((๐ด โ
โ* โง 0 โค ๐ด) โง (๐ต โ โ* โง 0 โค
๐ต)) โง 0 < ๐ด) โง 0 < ๐ต) โ 0 โค (๐ด ยทe ๐ต)) |
12 | | 0le0 12313 |
. . . . 5
โข 0 โค
0 |
13 | | oveq2 7417 |
. . . . . . 7
โข (0 =
๐ต โ (๐ด ยทe 0) = (๐ด ยทe ๐ต)) |
14 | 13 | eqcomd 2739 |
. . . . . 6
โข (0 =
๐ต โ (๐ด ยทe ๐ต) = (๐ด ยทe 0)) |
15 | | xmul01 13246 |
. . . . . . 7
โข (๐ด โ โ*
โ (๐ด
ยทe 0) = 0) |
16 | 15 | ad2antrr 725 |
. . . . . 6
โข (((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โ (๐ด ยทe 0) =
0) |
17 | 14, 16 | sylan9eqr 2795 |
. . . . 5
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 = ๐ต) โ (๐ด ยทe ๐ต) = 0) |
18 | 12, 17 | breqtrrid 5187 |
. . . 4
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 = ๐ต) โ 0 โค (๐ด ยทe ๐ต)) |
19 | 18 | adantlr 714 |
. . 3
โข
(((((๐ด โ
โ* โง 0 โค ๐ด) โง (๐ต โ โ* โง 0 โค
๐ต)) โง 0 < ๐ด) โง 0 = ๐ต) โ 0 โค (๐ด ยทe ๐ต)) |
20 | | xrleloe 13123 |
. . . . . 6
โข ((0
โ โ* โง ๐ต โ โ*) โ (0 โค
๐ต โ (0 < ๐ต โจ 0 = ๐ต))) |
21 | 3, 20 | mpan 689 |
. . . . 5
โข (๐ต โ โ*
โ (0 โค ๐ต โ (0
< ๐ต โจ 0 = ๐ต))) |
22 | 21 | biimpa 478 |
. . . 4
โข ((๐ต โ โ*
โง 0 โค ๐ต) โ (0
< ๐ต โจ 0 = ๐ต)) |
23 | 22 | ad2antlr 726 |
. . 3
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 < ๐ด) โ (0 < ๐ต โจ 0 = ๐ต)) |
24 | 11, 19, 23 | mpjaodan 958 |
. 2
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 < ๐ด) โ 0 โค (๐ด ยทe ๐ต)) |
25 | | oveq1 7416 |
. . . . 5
โข (0 =
๐ด โ (0
ยทe ๐ต) =
(๐ด ยทe
๐ต)) |
26 | 25 | eqcomd 2739 |
. . . 4
โข (0 =
๐ด โ (๐ด ยทe ๐ต) = (0 ยทe ๐ต)) |
27 | | xmul02 13247 |
. . . . 5
โข (๐ต โ โ*
โ (0 ยทe ๐ต) = 0) |
28 | 27 | ad2antrl 727 |
. . . 4
โข (((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โ (0 ยทe ๐ต) = 0) |
29 | 26, 28 | sylan9eqr 2795 |
. . 3
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 = ๐ด) โ (๐ด ยทe ๐ต) = 0) |
30 | 12, 29 | breqtrrid 5187 |
. 2
โข ((((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โง 0 = ๐ด) โ 0 โค (๐ด ยทe ๐ต)) |
31 | | xrleloe 13123 |
. . . . 5
โข ((0
โ โ* โง ๐ด โ โ*) โ (0 โค
๐ด โ (0 < ๐ด โจ 0 = ๐ด))) |
32 | 3, 31 | mpan 689 |
. . . 4
โข (๐ด โ โ*
โ (0 โค ๐ด โ (0
< ๐ด โจ 0 = ๐ด))) |
33 | 32 | biimpa 478 |
. . 3
โข ((๐ด โ โ*
โง 0 โค ๐ด) โ (0
< ๐ด โจ 0 = ๐ด)) |
34 | 33 | adantr 482 |
. 2
โข (((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โ (0 < ๐ด โจ 0 = ๐ด)) |
35 | 24, 30, 34 | mpjaodan 958 |
1
โข (((๐ด โ โ*
โง 0 โค ๐ด) โง
(๐ต โ
โ* โง 0 โค ๐ต)) โ 0 โค (๐ด ยทe ๐ต)) |