Step | Hyp | Ref
| Expression |
1 | | 0sno 27678 |
. . . . 5
โข
0s โ No |
2 | 1 | a1i 11 |
. . . 4
โข (((๐ โง 0s <s ๐ด) โง 0s <s
๐ต) โ 0s
โ No ) |
3 | | mulsge0d.1 |
. . . . . 6
โข (๐ โ ๐ด โ No
) |
4 | | mulsge0d.2 |
. . . . . 6
โข (๐ โ ๐ต โ No
) |
5 | 3, 4 | mulscld 27954 |
. . . . 5
โข (๐ โ (๐ด ยทs ๐ต) โ No
) |
6 | 5 | ad2antrr 723 |
. . . 4
โข (((๐ โง 0s <s ๐ด) โง 0s <s
๐ต) โ (๐ด ยทs ๐ต) โ
No ) |
7 | 3 | ad2antrr 723 |
. . . . 5
โข (((๐ โง 0s <s ๐ด) โง 0s <s
๐ต) โ ๐ด โ No
) |
8 | 4 | ad2antrr 723 |
. . . . 5
โข (((๐ โง 0s <s ๐ด) โง 0s <s
๐ต) โ ๐ต โ No
) |
9 | | simplr 766 |
. . . . 5
โข (((๐ โง 0s <s ๐ด) โง 0s <s
๐ต) โ 0s
<s ๐ด) |
10 | | simpr 484 |
. . . . 5
โข (((๐ โง 0s <s ๐ด) โง 0s <s
๐ต) โ 0s
<s ๐ต) |
11 | 7, 8, 9, 10 | mulsgt0d 27964 |
. . . 4
โข (((๐ โง 0s <s ๐ด) โง 0s <s
๐ต) โ 0s
<s (๐ด
ยทs ๐ต)) |
12 | 2, 6, 11 | sltled 27621 |
. . 3
โข (((๐ โง 0s <s ๐ด) โง 0s <s
๐ต) โ 0s
โคs (๐ด
ยทs ๐ต)) |
13 | | slerflex 27615 |
. . . . . 6
โข (
0s โ No โ 0s
โคs 0s ) |
14 | 1, 13 | ax-mp 5 |
. . . . 5
โข
0s โคs 0s |
15 | | oveq2 7410 |
. . . . . . 7
โข (
0s = ๐ต โ
(๐ด ยทs
0s ) = (๐ด
ยทs ๐ต)) |
16 | 15 | adantl 481 |
. . . . . 6
โข ((๐ โง 0s = ๐ต) โ (๐ด ยทs 0s ) =
(๐ด ยทs
๐ต)) |
17 | | muls01 27931 |
. . . . . . . 8
โข (๐ด โ
No โ (๐ด
ยทs 0s ) = 0s ) |
18 | 3, 17 | syl 17 |
. . . . . . 7
โข (๐ โ (๐ด ยทs 0s ) =
0s ) |
19 | 18 | adantr 480 |
. . . . . 6
โข ((๐ โง 0s = ๐ต) โ (๐ด ยทs 0s ) =
0s ) |
20 | 16, 19 | eqtr3d 2766 |
. . . . 5
โข ((๐ โง 0s = ๐ต) โ (๐ด ยทs ๐ต) = 0s ) |
21 | 14, 20 | breqtrrid 5177 |
. . . 4
โข ((๐ โง 0s = ๐ต) โ 0s โคs
(๐ด ยทs
๐ต)) |
22 | 21 | adantlr 712 |
. . 3
โข (((๐ โง 0s <s ๐ด) โง 0s = ๐ต) โ 0s โคs
(๐ด ยทs
๐ต)) |
23 | | mulsge0d.4 |
. . . . 5
โข (๐ โ 0s โคs ๐ต) |
24 | | sleloe 27606 |
. . . . . 6
โข ((
0s โ No โง ๐ต โ No )
โ ( 0s โคs ๐ต โ ( 0s <s ๐ต โจ 0s = ๐ต))) |
25 | 1, 4, 24 | sylancr 586 |
. . . . 5
โข (๐ โ ( 0s โคs
๐ต โ ( 0s
<s ๐ต โจ 0s
= ๐ต))) |
26 | 23, 25 | mpbid 231 |
. . . 4
โข (๐ โ ( 0s <s
๐ต โจ 0s =
๐ต)) |
27 | 26 | adantr 480 |
. . 3
โข ((๐ โง 0s <s ๐ด) โ ( 0s <s
๐ต โจ 0s =
๐ต)) |
28 | 12, 22, 27 | mpjaodan 955 |
. 2
โข ((๐ โง 0s <s ๐ด) โ 0s โคs
(๐ด ยทs
๐ต)) |
29 | | oveq1 7409 |
. . . . 5
โข (
0s = ๐ด โ (
0s ยทs ๐ต) = (๐ด ยทs ๐ต)) |
30 | 29 | adantl 481 |
. . . 4
โข ((๐ โง 0s = ๐ด) โ ( 0s
ยทs ๐ต) =
(๐ด ยทs
๐ต)) |
31 | | muls02 27960 |
. . . . . 6
โข (๐ต โ
No โ ( 0s ยทs ๐ต) = 0s ) |
32 | 4, 31 | syl 17 |
. . . . 5
โข (๐ โ ( 0s
ยทs ๐ต) =
0s ) |
33 | 32 | adantr 480 |
. . . 4
โข ((๐ โง 0s = ๐ด) โ ( 0s
ยทs ๐ต) =
0s ) |
34 | 30, 33 | eqtr3d 2766 |
. . 3
โข ((๐ โง 0s = ๐ด) โ (๐ด ยทs ๐ต) = 0s ) |
35 | 14, 34 | breqtrrid 5177 |
. 2
โข ((๐ โง 0s = ๐ด) โ 0s โคs
(๐ด ยทs
๐ต)) |
36 | | mulsge0d.3 |
. . 3
โข (๐ โ 0s โคs ๐ด) |
37 | | sleloe 27606 |
. . . 4
โข ((
0s โ No โง ๐ด โ No )
โ ( 0s โคs ๐ด โ ( 0s <s ๐ด โจ 0s = ๐ด))) |
38 | 1, 3, 37 | sylancr 586 |
. . 3
โข (๐ โ ( 0s โคs
๐ด โ ( 0s
<s ๐ด โจ 0s
= ๐ด))) |
39 | 36, 38 | mpbid 231 |
. 2
โข (๐ โ ( 0s <s
๐ด โจ 0s =
๐ด)) |
40 | 28, 35, 39 | mpjaodan 955 |
1
โข (๐ โ 0s โคs (๐ด ยทs ๐ต)) |