Step | Hyp | Ref
| Expression |
1 | | 0red 11163 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โ
โ) |
2 | | simpl 484 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
3 | 1, 2 | leloed 11303 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค
๐ด โ (0 < ๐ด โจ 0 = ๐ด))) |
4 | | simpr 486 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
5 | 1, 4 | leloed 11303 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค
๐ต โ (0 < ๐ต โจ 0 = ๐ต))) |
6 | 3, 5 | anbi12d 632 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 โค
๐ด โง 0 โค ๐ต) โ ((0 < ๐ด โจ 0 = ๐ด) โง (0 < ๐ต โจ 0 = ๐ต)))) |
7 | | 0red 11163 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 <
๐ด โง 0 < ๐ต)) โ 0 โ
โ) |
8 | | simpll 766 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 <
๐ด โง 0 < ๐ต)) โ ๐ด โ โ) |
9 | | simplr 768 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 <
๐ด โง 0 < ๐ต)) โ ๐ต โ โ) |
10 | 8, 9 | remulcld 11190 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 <
๐ด โง 0 < ๐ต)) โ (๐ด ยท ๐ต) โ โ) |
11 | | mulgt0 11237 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 < (๐ด ยท ๐ต)) |
12 | 11 | an4s 659 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 <
๐ด โง 0 < ๐ต)) โ 0 < (๐ด ยท ๐ต)) |
13 | 7, 10, 12 | ltled 11308 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 <
๐ด โง 0 < ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |
14 | 13 | ex 414 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 <
๐ด โง 0 < ๐ต) โ 0 โค (๐ด ยท ๐ต))) |
15 | | 0re 11162 |
. . . . . . . . 9
โข 0 โ
โ |
16 | | leid 11256 |
. . . . . . . . 9
โข (0 โ
โ โ 0 โค 0) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . 8
โข 0 โค
0 |
18 | 4 | recnd 11188 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
19 | 18 | mul02d 11358 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (0
ยท ๐ต) =
0) |
20 | 17, 19 | breqtrrid 5144 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
(0 ยท ๐ต)) |
21 | | oveq1 7365 |
. . . . . . . 8
โข (0 =
๐ด โ (0 ยท ๐ต) = (๐ด ยท ๐ต)) |
22 | 21 | breq2d 5118 |
. . . . . . 7
โข (0 =
๐ด โ (0 โค (0
ยท ๐ต) โ 0 โค
(๐ด ยท ๐ต))) |
23 | 20, 22 | syl5ibcom 244 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 =
๐ด โ 0 โค (๐ด ยท ๐ต))) |
24 | 23 | adantrd 493 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 =
๐ด โง 0 < ๐ต) โ 0 โค (๐ด ยท ๐ต))) |
25 | 2 | recnd 11188 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
26 | 25 | mul01d 11359 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท 0) =
0) |
27 | 17, 26 | breqtrrid 5144 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
(๐ด ยท
0)) |
28 | | oveq2 7366 |
. . . . . . . 8
โข (0 =
๐ต โ (๐ด ยท 0) = (๐ด ยท ๐ต)) |
29 | 28 | breq2d 5118 |
. . . . . . 7
โข (0 =
๐ต โ (0 โค (๐ด ยท 0) โ 0 โค
(๐ด ยท ๐ต))) |
30 | 27, 29 | syl5ibcom 244 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 =
๐ต โ 0 โค (๐ด ยท ๐ต))) |
31 | 30 | adantld 492 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 <
๐ด โง 0 = ๐ต) โ 0 โค (๐ด ยท ๐ต))) |
32 | 30 | adantld 492 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 =
๐ด โง 0 = ๐ต) โ 0 โค (๐ด ยท ๐ต))) |
33 | 14, 24, 31, 32 | ccased 1038 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (((0
< ๐ด โจ 0 = ๐ด) โง (0 < ๐ต โจ 0 = ๐ต)) โ 0 โค (๐ด ยท ๐ต))) |
34 | 6, 33 | sylbid 239 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 โค
๐ด โง 0 โค ๐ต) โ 0 โค (๐ด ยท ๐ต))) |
35 | 34 | imp 408 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |
36 | 35 | an4s 659 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |