Step | Hyp | Ref
| Expression |
1 | | 0re 11162 |
. . . . . . 7
โข 0 โ
โ |
2 | | leloe 11246 |
. . . . . . 7
โข ((0
โ โ โง ๐ถ
โ โ) โ (0 โค ๐ถ โ (0 < ๐ถ โจ 0 = ๐ถ))) |
3 | 1, 2 | mpan 689 |
. . . . . 6
โข (๐ถ โ โ โ (0 โค
๐ถ โ (0 < ๐ถ โจ 0 = ๐ถ))) |
4 | 3 | pm5.32i 576 |
. . . . 5
โข ((๐ถ โ โ โง 0 โค
๐ถ) โ (๐ถ โ โ โง (0 <
๐ถ โจ 0 = ๐ถ))) |
5 | | lemul1 12012 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) |
6 | 5 | biimpd 228 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) |
7 | 6 | 3expia 1122 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ถ โ โ โง 0 <
๐ถ) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)))) |
8 | 7 | com12 32 |
. . . . . 6
โข ((๐ถ โ โ โง 0 <
๐ถ) โ ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)))) |
9 | 1 | leidi 11694 |
. . . . . . . . . 10
โข 0 โค
0 |
10 | | recn 11146 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ ๐ด โ
โ) |
11 | 10 | mul01d 11359 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (๐ด ยท 0) =
0) |
12 | | recn 11146 |
. . . . . . . . . . . 12
โข (๐ต โ โ โ ๐ต โ
โ) |
13 | 12 | mul01d 11359 |
. . . . . . . . . . 11
โข (๐ต โ โ โ (๐ต ยท 0) =
0) |
14 | 11, 13 | breqan12d 5122 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท 0) โค (๐ต ยท 0) โ 0 โค
0)) |
15 | 9, 14 | mpbiri 258 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท 0) โค (๐ต ยท 0)) |
16 | | oveq2 7366 |
. . . . . . . . . 10
โข (0 =
๐ถ โ (๐ด ยท 0) = (๐ด ยท ๐ถ)) |
17 | | oveq2 7366 |
. . . . . . . . . 10
โข (0 =
๐ถ โ (๐ต ยท 0) = (๐ต ยท ๐ถ)) |
18 | 16, 17 | breq12d 5119 |
. . . . . . . . 9
โข (0 =
๐ถ โ ((๐ด ยท 0) โค (๐ต ยท 0) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) |
19 | 15, 18 | imbitrid 243 |
. . . . . . . 8
โข (0 =
๐ถ โ ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) |
20 | 19 | a1dd 50 |
. . . . . . 7
โข (0 =
๐ถ โ ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)))) |
21 | 20 | adantl 483 |
. . . . . 6
โข ((๐ถ โ โ โง 0 = ๐ถ) โ ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)))) |
22 | 8, 21 | jaodan 957 |
. . . . 5
โข ((๐ถ โ โ โง (0 <
๐ถ โจ 0 = ๐ถ)) โ ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)))) |
23 | 4, 22 | sylbi 216 |
. . . 4
โข ((๐ถ โ โ โง 0 โค
๐ถ) โ ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)))) |
24 | 23 | com12 32 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ถ โ โ โง 0 โค
๐ถ) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)))) |
25 | 24 | 3impia 1118 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) |
26 | 25 | imp 408 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)) |