Step | Hyp | Ref
| Expression |
1 | | breq2 5147 |
. . . . 5
โข (๐ = (๐ ยทs ๐) โ ((abssโ(๐ด ยทs ๐ต)) <s ๐ โ (abssโ(๐ด ยทs ๐ต)) <s (๐ ยทs ๐))) |
2 | | nnmulscl 28237 |
. . . . . 6
โข ((๐ โ โs
โง ๐ โ
โs) โ (๐ ยทs ๐) โ
โs) |
3 | 2 | ad2antlr 725 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (๐ ยทs ๐) โ
โs) |
4 | | absmuls 28160 |
. . . . . . 7
โข ((๐ด โ
No โง ๐ต โ
No ) โ (abssโ(๐ด ยทs ๐ต)) =
((abssโ๐ด)
ยทs (abssโ๐ต))) |
5 | 4 | ad2antrr 724 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ(๐ด ยทs ๐ต)) =
((abssโ๐ด)
ยทs (abssโ๐ต))) |
6 | | absscl 28156 |
. . . . . . . 8
โข (๐ด โ
No โ (abssโ๐ด) โ No
) |
7 | 6 | ad3antrrr 728 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ๐ด) โ
No ) |
8 | | simplrl 775 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ ๐ โ
โs) |
9 | 8 | nnsnod 28220 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ ๐ โ No
) |
10 | | absscl 28156 |
. . . . . . . 8
โข (๐ต โ
No โ (abssโ๐ต) โ No
) |
11 | 10 | ad3antlr 729 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ๐ต) โ
No ) |
12 | | simplrr 776 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ ๐ โ
โs) |
13 | 12 | nnsnod 28220 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ ๐ โ No
) |
14 | | abssge0 28161 |
. . . . . . . 8
โข (๐ด โ
No โ 0s โคs (abssโ๐ด)) |
15 | 14 | ad3antrrr 728 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ 0s โคs
(abssโ๐ด)) |
16 | | simprl 769 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ๐ด) <s ๐) |
17 | | abssge0 28161 |
. . . . . . . 8
โข (๐ต โ
No โ 0s โคs (abssโ๐ต)) |
18 | 17 | ad3antlr 729 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ 0s โคs
(abssโ๐ต)) |
19 | | simprr 771 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ๐ต) <s ๐) |
20 | 7, 9, 11, 13, 15, 16, 18, 19 | sltmul12ad 28105 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ ((abssโ๐ด) ยทs
(abssโ๐ต))
<s (๐
ยทs ๐)) |
21 | 5, 20 | eqbrtrd 5165 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ (abssโ(๐ด ยทs ๐ต)) <s (๐ ยทs ๐)) |
22 | 1, 3, 21 | rspcedvdw 3604 |
. . . 4
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐)) โ โ๐ โ โs
(abssโ(๐ด
ยทs ๐ต))
<s ๐) |
23 | 22 | ex 411 |
. . 3
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โ (((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐) โ โ๐ โ โs
(abssโ(๐ด
ยทs ๐ต))
<s ๐)) |
24 | | nnsno 28218 |
. . . . . 6
โข (๐ โ โs
โ ๐ โ No ) |
25 | | absslt 28165 |
. . . . . 6
โข ((๐ด โ
No โง ๐ โ
No ) โ ((abssโ๐ด) <s ๐ โ (( -us โ๐) <s ๐ด โง ๐ด <s ๐))) |
26 | 24, 25 | sylan2 591 |
. . . . 5
โข ((๐ด โ
No โง ๐ โ
โs) โ ((abssโ๐ด) <s ๐ โ (( -us โ๐) <s ๐ด โง ๐ด <s ๐))) |
27 | | nnsno 28218 |
. . . . . 6
โข (๐ โ โs
โ ๐ โ No ) |
28 | | absslt 28165 |
. . . . . 6
โข ((๐ต โ
No โง ๐ โ
No ) โ ((abssโ๐ต) <s ๐ โ (( -us โ๐) <s ๐ต โง ๐ต <s ๐))) |
29 | 27, 28 | sylan2 591 |
. . . . 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 658 |
. . 3
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โ (((abssโ๐ด) <s ๐ โง (abssโ๐ต) <s ๐) โ ((( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐)))) |
32 | | mulscl 28056 |
. . . . . 6
โข ((๐ด โ
No โง ๐ต โ
No ) โ (๐ด ยทs ๐ต) โ No
) |
33 | 32 | adantr 479 |
. . . . 5
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โ (๐ด
ยทs ๐ต)
โ No ) |
34 | | nnsno 28218 |
. . . . 5
โข (๐ โ โs
โ ๐ โ No ) |
35 | | absslt 28165 |
. . . . 5
โข (((๐ด ยทs ๐ต) โ
No โง ๐ โ
No ) โ ((abssโ(๐ด ยทs ๐ต)) <s ๐ โ (( -us โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐))) |
36 | 33, 34, 35 | syl2an 594 |
. . . 4
โข ((((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โง ๐ โ
โs) โ ((abssโ(๐ด ยทs ๐ต)) <s ๐ โ (( -us โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐))) |
37 | 36 | rexbidva 3167 |
. . 3
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โ (โ๐ โ
โs (abssโ(๐ด ยทs ๐ต)) <s ๐ โ โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐))) |
38 | 23, 31, 37 | 3imtr3d 292 |
. 2
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โ (((( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐)) โ โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐))) |
39 | 38 | impr 453 |
1
โข (((๐ด โ
No โง ๐ต โ
No ) โง ((๐ โ โs โง ๐ โ โs)
โง ((( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐)))) โ โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐)) |