Step | Hyp | Ref
| Expression |
1 | | breq2 5145 |
. . . . 5
โข (๐ = (๐ ยทs ๐) โ ((abssโ(๐ด ยทs ๐ต)) <s ๐ โ (abssโ(๐ด ยทs ๐ต)) <s (๐ ยทs ๐))) |
2 | | nnmulscl 28168 |
. . . . . 6
โข ((๐ โ โs
โง ๐ โ
โs) โ (๐ ยทs ๐) โ
โs) |
3 | 2 | ad2antlr 724 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (๐ ยทs ๐) โ
โs) |
4 | | absmuls 28093 |
. . . . . . 7
โข ((๐ด โ
No โง ๐ต โ
No ) โ (abssโ(๐ด ยทs ๐ต)) =
((abssโ๐ด)
ยทs (abssโ๐ต))) |
5 | 4 | ad2antrr 723 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ(๐ด ยทs ๐ต)) =
((abssโ๐ด)
ยทs (abssโ๐ต))) |
6 | | absscl 28089 |
. . . . . . . 8
โข (๐ด โ
No โ (abssโ๐ด) โ No
) |
7 | 6 | ad3antrrr 727 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ๐ด) โ
No ) |
8 | | simplrl 774 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ ๐ โ
โs) |
9 | 8 | nnsnod 28153 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ ๐ โ No
) |
10 | | absscl 28089 |
. . . . . . . 8
โข (๐ต โ
No โ (abssโ๐ต) โ No
) |
11 | 10 | ad3antlr 728 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ๐ต) โ
No ) |
12 | | simplrr 775 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ ๐ โ
โs) |
13 | 12 | nnsnod 28153 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ ๐ โ No
) |
14 | | abssge0 28094 |
. . . . . . . 8
โข (๐ด โ
No โ 0s โคs (abssโ๐ด)) |
15 | 14 | ad3antrrr 727 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ 0s โคs
(abssโ๐ด)) |
16 | | simprl 768 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ๐ด) <s ๐) |
17 | | abssge0 28094 |
. . . . . . . 8
โข (๐ต โ
No โ 0s โคs (abssโ๐ต)) |
18 | 17 | ad3antlr 728 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ 0s โคs
(abssโ๐ต)) |
19 | | simprr 770 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ๐ต) <s ๐) |
20 | 7, 9, 11, 13, 15, 16, 18, 19 | sltmul12ad 28038 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ ((abssโ๐ด) ยทs
(abssโ๐ต))
<s (๐
ยทs ๐)) |
21 | 5, 20 | eqbrtrd 5163 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ(๐ด ยทs ๐ต)) <s (๐ ยทs ๐)) |
22 | 1, 3, 21 | rspcedvdw 3609 |
. . . 4
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ โ๐ โ โs
(abssโ(๐ด
ยทs ๐ต))
<s ๐) |
23 | 22 | ex 412 |
. . 3
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โ (((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐) โ โ๐ โ โs
(abssโ(๐ด
ยทs ๐ต))
<s ๐)) |
24 | | nnsno 28151 |
. . . . . 6
โข (๐ โ โs
โ ๐ โ No ) |
25 | | absslt 28098 |
. . . . . 6
โข ((๐ด โ
No โง ๐ โ
No ) โ ((abssโ๐ด) <s ๐ โ (( -us โ๐) <s ๐ด โง ๐ด <s ๐))) |
26 | 24, 25 | sylan2 592 |
. . . . 5
โข ((๐ด โ
No โง ๐ โ
โs) โ ((abssโ๐ด) <s ๐ โ (( -us โ๐) <s ๐ด โง ๐ด <s ๐))) |
27 | | nnsno 28151 |
. . . . . 6
โข (๐ โ โs
โ ๐ โ No ) |
28 | | absslt 28098 |
. . . . . 6
โข ((๐ต โ
No โง ๐ โ
No ) โ ((abssโ๐ต) <s ๐ โ (( -us โ๐) <s ๐ต โง ๐ต <s ๐))) |
29 | 27, 28 | sylan2 592 |
. . . . 5
โข ((๐ต โ
No โง ๐ โ
โs) โ ((abssโ๐ต) <s ๐ โ (( -us โ๐) <s ๐ต โง ๐ต <s ๐))) |
30 | 26, 29 | bi2anan9 636 |
. . . 4
โข (((๐ด โ
No โง ๐ โ
โs) โง (๐ต โ No
โง ๐ โ
โs)) โ (((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐) โ ((( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐)))) |
31 | 30 | an4s 657 |
. . 3
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โ (((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐) โ ((( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐)))) |
32 | | mulscl 27989 |
. . . . . 6
โข ((๐ด โ
No โง ๐ต โ
No ) โ (๐ด ยทs ๐ต) โ No
) |
33 | 32 | adantr 480 |
. . . . 5
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โ (๐ด
ยทs ๐ต)
โ No ) |
34 | | nnsno 28151 |
. . . . 5
โข (๐ โ โs
โ ๐ โ No ) |
35 | | absslt 28098 |
. . . . 5
โข (((๐ด ยทs ๐ต) โ
No โง ๐ โ
No ) โ ((abssโ(๐ด ยทs ๐ต)) <s ๐ โ (( -us โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐))) |
36 | 33, 34, 35 | syl2an 595 |
. . . 4
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ๐ โ
โs) โ ((abssโ(๐ด ยทs ๐ต)) <s ๐ โ (( -us โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐))) |
37 | 36 | rexbidva 3170 |
. . 3
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โ (โ๐ โ
โs (abssโ(๐ด ยทs ๐ต)) <s ๐ โ โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐))) |
38 | 23, 31, 37 | 3imtr3d 293 |
. 2
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โ (((( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐)) โ โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐))) |
39 | 38 | impr 454 |
1
โข (((๐ด โ
No โง ๐ต โ
No ) โง ((๐ โ โs โง ๐ โ โs)
โง ((( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐)))) โ โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐)) |