Step | Hyp | Ref
| Expression |
1 | | slemuld.1 |
. . . . . . . 8
โข (๐ โ ๐ด โ No
) |
2 | | slemuld.4 |
. . . . . . . 8
โข (๐ โ ๐ท โ No
) |
3 | 1, 2 | mulscld 27504 |
. . . . . . 7
โข (๐ โ (๐ด ยทs ๐ท) โ No
) |
4 | | slemuld.3 |
. . . . . . . 8
โข (๐ โ ๐ถ โ No
) |
5 | 1, 4 | mulscld 27504 |
. . . . . . 7
โข (๐ โ (๐ด ยทs ๐ถ) โ No
) |
6 | 3, 5 | subscld 27449 |
. . . . . 6
โข (๐ โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โ No
) |
7 | 6 | adantr 481 |
. . . . 5
โข ((๐ โง (๐ด <s ๐ต โง ๐ถ <s ๐ท)) โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โ No
) |
8 | | slemuld.2 |
. . . . . . . 8
โข (๐ โ ๐ต โ No
) |
9 | 8, 2 | mulscld 27504 |
. . . . . . 7
โข (๐ โ (๐ต ยทs ๐ท) โ No
) |
10 | 8, 4 | mulscld 27504 |
. . . . . . 7
โข (๐ โ (๐ต ยทs ๐ถ) โ No
) |
11 | 9, 10 | subscld 27449 |
. . . . . 6
โข (๐ โ ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ)) โ No
) |
12 | 11 | adantr 481 |
. . . . 5
โข ((๐ โง (๐ด <s ๐ต โง ๐ถ <s ๐ท)) โ ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ)) โ No
) |
13 | 1 | adantr 481 |
. . . . . 6
โข ((๐ โง (๐ด <s ๐ต โง ๐ถ <s ๐ท)) โ ๐ด โ No
) |
14 | 8 | adantr 481 |
. . . . . 6
โข ((๐ โง (๐ด <s ๐ต โง ๐ถ <s ๐ท)) โ ๐ต โ No
) |
15 | 4 | adantr 481 |
. . . . . 6
โข ((๐ โง (๐ด <s ๐ต โง ๐ถ <s ๐ท)) โ ๐ถ โ No
) |
16 | 2 | adantr 481 |
. . . . . 6
โข ((๐ โง (๐ด <s ๐ต โง ๐ถ <s ๐ท)) โ ๐ท โ No
) |
17 | | simprl 769 |
. . . . . 6
โข ((๐ โง (๐ด <s ๐ต โง ๐ถ <s ๐ท)) โ ๐ด <s ๐ต) |
18 | | simprr 771 |
. . . . . 6
โข ((๐ โง (๐ด <s ๐ต โง ๐ถ <s ๐ท)) โ ๐ถ <s ๐ท) |
19 | 13, 14, 15, 16, 17, 18 | sltmuld 27506 |
. . . . 5
โข ((๐ โง (๐ด <s ๐ต โง ๐ถ <s ๐ท)) โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) <s ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ))) |
20 | 7, 12, 19 | sltled 27199 |
. . . 4
โข ((๐ โง (๐ด <s ๐ต โง ๐ถ <s ๐ท)) โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ))) |
21 | 20 | anassrs 468 |
. . 3
โข (((๐ โง ๐ด <s ๐ต) โง ๐ถ <s ๐ท) โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ))) |
22 | | 0sno 27253 |
. . . . . . . 8
โข
0s โ No |
23 | | slerflex 27193 |
. . . . . . . 8
โข (
0s โ No โ 0s
โคs 0s ) |
24 | 22, 23 | mp1i 13 |
. . . . . . 7
โข (๐ โ 0s โคs
0s ) |
25 | | subsid 27451 |
. . . . . . . 8
โข ((๐ด ยทs ๐ท) โ
No โ ((๐ด
ยทs ๐ท)
-s (๐ด
ยทs ๐ท)) =
0s ) |
26 | 3, 25 | syl 17 |
. . . . . . 7
โข (๐ โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ท)) = 0s ) |
27 | | subsid 27451 |
. . . . . . . 8
โข ((๐ต ยทs ๐ท) โ
No โ ((๐ต
ยทs ๐ท)
-s (๐ต
ยทs ๐ท)) =
0s ) |
28 | 9, 27 | syl 17 |
. . . . . . 7
โข (๐ โ ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ท)) = 0s ) |
29 | 24, 26, 28 | 3brtr4d 5173 |
. . . . . 6
โข (๐ โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ท)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ท))) |
30 | | oveq2 7401 |
. . . . . . . 8
โข (๐ถ = ๐ท โ (๐ด ยทs ๐ถ) = (๐ด ยทs ๐ท)) |
31 | 30 | oveq2d 7409 |
. . . . . . 7
โข (๐ถ = ๐ท โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) = ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ท))) |
32 | | oveq2 7401 |
. . . . . . . 8
โข (๐ถ = ๐ท โ (๐ต ยทs ๐ถ) = (๐ต ยทs ๐ท)) |
33 | 32 | oveq2d 7409 |
. . . . . . 7
โข (๐ถ = ๐ท โ ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ)) = ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ท))) |
34 | 31, 33 | breq12d 5154 |
. . . . . 6
โข (๐ถ = ๐ท โ (((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ)) โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ท)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ท)))) |
35 | 29, 34 | syl5ibrcom 246 |
. . . . 5
โข (๐ โ (๐ถ = ๐ท โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ)))) |
36 | 35 | imp 407 |
. . . 4
โข ((๐ โง ๐ถ = ๐ท) โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ))) |
37 | 36 | adantlr 713 |
. . 3
โข (((๐ โง ๐ด <s ๐ต) โง ๐ถ = ๐ท) โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ))) |
38 | | slemuld.6 |
. . . . 5
โข (๐ โ ๐ถ โคs ๐ท) |
39 | | sleloe 27184 |
. . . . . 6
โข ((๐ถ โ
No โง ๐ท โ
No ) โ (๐ถ โคs ๐ท โ (๐ถ <s ๐ท โจ ๐ถ = ๐ท))) |
40 | 4, 2, 39 | syl2anc 584 |
. . . . 5
โข (๐ โ (๐ถ โคs ๐ท โ (๐ถ <s ๐ท โจ ๐ถ = ๐ท))) |
41 | 38, 40 | mpbid 231 |
. . . 4
โข (๐ โ (๐ถ <s ๐ท โจ ๐ถ = ๐ท)) |
42 | 41 | adantr 481 |
. . 3
โข ((๐ โง ๐ด <s ๐ต) โ (๐ถ <s ๐ท โจ ๐ถ = ๐ท)) |
43 | 21, 37, 42 | mpjaodan 957 |
. 2
โข ((๐ โง ๐ด <s ๐ต) โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ))) |
44 | | slerflex 27193 |
. . . . 5
โข (((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ)) โ
No โ ((๐ต
ยทs ๐ท)
-s (๐ต
ยทs ๐ถ))
โคs ((๐ต
ยทs ๐ท)
-s (๐ต
ยทs ๐ถ))) |
45 | 11, 44 | syl 17 |
. . . 4
โข (๐ โ ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ))) |
46 | | oveq1 7400 |
. . . . . 6
โข (๐ด = ๐ต โ (๐ด ยทs ๐ท) = (๐ต ยทs ๐ท)) |
47 | | oveq1 7400 |
. . . . . 6
โข (๐ด = ๐ต โ (๐ด ยทs ๐ถ) = (๐ต ยทs ๐ถ)) |
48 | 46, 47 | oveq12d 7411 |
. . . . 5
โข (๐ด = ๐ต โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) = ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ))) |
49 | 48 | breq1d 5151 |
. . . 4
โข (๐ด = ๐ต โ (((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ)) โ ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ)))) |
50 | 45, 49 | syl5ibrcom 246 |
. . 3
โข (๐ โ (๐ด = ๐ต โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ)))) |
51 | 50 | imp 407 |
. 2
โข ((๐ โง ๐ด = ๐ต) โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ))) |
52 | | slemuld.5 |
. . 3
โข (๐ โ ๐ด โคs ๐ต) |
53 | | sleloe 27184 |
. . . 4
โข ((๐ด โ
No โง ๐ต โ
No ) โ (๐ด โคs ๐ต โ (๐ด <s ๐ต โจ ๐ด = ๐ต))) |
54 | 1, 8, 53 | syl2anc 584 |
. . 3
โข (๐ โ (๐ด โคs ๐ต โ (๐ด <s ๐ต โจ ๐ด = ๐ต))) |
55 | 52, 54 | mpbid 231 |
. 2
โข (๐ โ (๐ด <s ๐ต โจ ๐ด = ๐ต)) |
56 | 43, 51, 55 | mpjaodan 957 |
1
โข (๐ โ ((๐ด ยทs ๐ท) -s (๐ด ยทs ๐ถ)) โคs ((๐ต ยทs ๐ท) -s (๐ต ยทs ๐ถ))) |