Step | Hyp | Ref
| Expression |
1 | | mulscl 27953 |
. . . . . . 7
โข ((๐ด โ
No โง ๐ต โ
No ) โ (๐ด ยทs ๐ต) โ No
) |
2 | 1 | adantr 480 |
. . . . . 6
โข (((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โ (๐ด ยทs ๐ต) โ No
) |
3 | | simplll 772 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง 0s โคs ๐ต) โ ๐ด โ No
) |
4 | | simpllr 773 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง 0s โคs ๐ต) โ ๐ต โ No
) |
5 | | simplr 766 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง 0s โคs ๐ต) โ 0s โคs
๐ด) |
6 | | simpr 484 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง 0s โคs ๐ต) โ 0s โคs
๐ต) |
7 | 3, 4, 5, 6 | mulsge0d 27965 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง 0s โคs ๐ต) โ 0s โคs
(๐ด ยทs
๐ต)) |
8 | | abssid 28054 |
. . . . . 6
โข (((๐ด ยทs ๐ต) โ
No โง 0s โคs (๐ด ยทs ๐ต)) โ (abssโ(๐ด ยทs ๐ต)) = (๐ด ยทs ๐ต)) |
9 | 2, 7, 8 | syl2an2r 682 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง 0s โคs ๐ต) โ
(abssโ(๐ด
ยทs ๐ต)) =
(๐ด ยทs
๐ต)) |
10 | | abssid 28054 |
. . . . . . 7
โข ((๐ต โ
No โง 0s โคs ๐ต) โ (abssโ๐ต) = ๐ต) |
11 | 10 | ad4ant24 751 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง 0s โคs ๐ต) โ
(abssโ๐ต) =
๐ต) |
12 | 11 | oveq2d 7418 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง 0s โคs ๐ต) โ (๐ด ยทs
(abssโ๐ต))
= (๐ด ยทs
๐ต)) |
13 | 9, 12 | eqtr4d 2767 |
. . . 4
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง 0s โคs ๐ต) โ
(abssโ(๐ด
ยทs ๐ต)) =
(๐ด ยทs
(abssโ๐ต))) |
14 | | simplll 772 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ ๐ด โ
No ) |
15 | | simpllr 773 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ ๐ต โ
No ) |
16 | 14, 15 | mulnegs2d 27980 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ (๐ด ยทs (
-us โ๐ต)) =
( -us โ(๐ด
ยทs ๐ต))) |
17 | | abssnid 28056 |
. . . . . . 7
โข ((๐ต โ
No โง ๐ต โคs
0s ) โ (abssโ๐ต) = ( -us โ๐ต)) |
18 | 17 | ad4ant24 751 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ
(abssโ๐ต) =
( -us โ๐ต)) |
19 | 18 | oveq2d 7418 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ (๐ด ยทs
(abssโ๐ต))
= (๐ด ยทs (
-us โ๐ต))) |
20 | | negs0s 27858 |
. . . . . . . 8
โข (
-us โ 0s ) = 0s |
21 | 15 | negscld 27868 |
. . . . . . . . . 10
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ (
-us โ๐ต)
โ No ) |
22 | | simplr 766 |
. . . . . . . . . 10
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ 0s
โคs ๐ด) |
23 | | simpr 484 |
. . . . . . . . . . . 12
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ ๐ต โคs 0s
) |
24 | | 0sno 27678 |
. . . . . . . . . . . . . 14
โข
0s โ No |
25 | 24 | a1i 11 |
. . . . . . . . . . . . 13
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ 0s
โ No ) |
26 | 15, 25 | slenegd 27879 |
. . . . . . . . . . . 12
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ (๐ต โคs 0s โ (
-us โ 0s ) โคs ( -us โ๐ต))) |
27 | 23, 26 | mpbid 231 |
. . . . . . . . . . 11
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ (
-us โ 0s ) โคs ( -us โ๐ต)) |
28 | 20, 27 | eqbrtrrid 5175 |
. . . . . . . . . 10
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ 0s
โคs ( -us โ๐ต)) |
29 | 14, 21, 22, 28 | mulsge0d 27965 |
. . . . . . . . 9
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ 0s
โคs (๐ด
ยทs ( -us โ๐ต))) |
30 | 29, 16 | breqtrd 5165 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ 0s
โคs ( -us โ(๐ด ยทs ๐ต))) |
31 | 20, 30 | eqbrtrid 5174 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ (
-us โ 0s ) โคs ( -us โ(๐ด ยทs ๐ต))) |
32 | 2 | adantr 480 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ (๐ด ยทs ๐ต) โ
No ) |
33 | 32, 25 | slenegd 27879 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ ((๐ด ยทs ๐ต) โคs 0s โ (
-us โ 0s ) โคs ( -us โ(๐ด ยทs ๐ต)))) |
34 | 31, 33 | mpbird 257 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ (๐ด ยทs ๐ต) โคs 0s
) |
35 | | abssnid 28056 |
. . . . . 6
โข (((๐ด ยทs ๐ต) โ
No โง (๐ด
ยทs ๐ต)
โคs 0s ) โ (abssโ(๐ด ยทs ๐ต)) = ( -us โ(๐ด ยทs ๐ต))) |
36 | 2, 34, 35 | syl2an2r 682 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ
(abssโ(๐ด
ยทs ๐ต)) =
( -us โ(๐ด
ยทs ๐ต))) |
37 | 16, 19, 36 | 3eqtr4rd 2775 |
. . . 4
โข ((((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โง ๐ต โคs 0s ) โ
(abssโ(๐ด
ยทs ๐ต)) =
(๐ด ยทs
(abssโ๐ต))) |
38 | | sletric 27616 |
. . . . . 6
โข ((
0s โ No โง ๐ต โ No )
โ ( 0s โคs ๐ต โจ ๐ต โคs 0s )) |
39 | 24, 38 | mpan 687 |
. . . . 5
โข (๐ต โ
No โ ( 0s โคs ๐ต โจ ๐ต โคs 0s )) |
40 | 39 | ad2antlr 724 |
. . . 4
โข (((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โ ( 0s โคs ๐ต โจ ๐ต โคs 0s )) |
41 | 13, 37, 40 | mpjaodan 955 |
. . 3
โข (((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โ (abssโ(๐ด ยทs ๐ต)) = (๐ด ยทs
(abssโ๐ต))) |
42 | | abssid 28054 |
. . . . 5
โข ((๐ด โ
No โง 0s โคs ๐ด) โ (abssโ๐ด) = ๐ด) |
43 | 42 | adantlr 712 |
. . . 4
โข (((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โ (abssโ๐ด) = ๐ด) |
44 | 43 | oveq1d 7417 |
. . 3
โข (((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โ ((abssโ๐ด) ยทs
(abssโ๐ต))
= (๐ด ยทs
(abssโ๐ต))) |
45 | 41, 44 | eqtr4d 2767 |
. 2
โข (((๐ด โ
No โง ๐ต โ
No ) โง 0s โคs ๐ด) โ (abssโ(๐ด ยทs ๐ต)) =
((abssโ๐ด)
ยทs (abssโ๐ต))) |
46 | | simplll 772 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ ๐ด โ
No ) |
47 | | simpllr 773 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ ๐ต โ
No ) |
48 | 46, 47 | mulnegs1d 27979 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ ((
-us โ๐ด)
ยทs ๐ต) = (
-us โ(๐ด
ยทs ๐ต))) |
49 | 10 | ad4ant24 751 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ
(abssโ๐ต) =
๐ต) |
50 | 49 | oveq2d 7418 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ ((
-us โ๐ด)
ยทs (abssโ๐ต)) = (( -us โ๐ด) ยทs ๐ต)) |
51 | 1 | adantr 480 |
. . . . . 6
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โ (๐ด ยทs ๐ต) โ
No ) |
52 | 46 | negscld 27868 |
. . . . . . . . . 10
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ (
-us โ๐ด)
โ No ) |
53 | | simplr 766 |
. . . . . . . . . . . 12
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ ๐ด โคs 0s
) |
54 | 24 | a1i 11 |
. . . . . . . . . . . . 13
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ
0s โ No ) |
55 | 46, 54 | slenegd 27879 |
. . . . . . . . . . . 12
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ (๐ด โคs 0s โ (
-us โ 0s ) โคs ( -us โ๐ด))) |
56 | 53, 55 | mpbid 231 |
. . . . . . . . . . 11
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ (
-us โ 0s ) โคs ( -us โ๐ด)) |
57 | 20, 56 | eqbrtrrid 5175 |
. . . . . . . . . 10
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ
0s โคs ( -us โ๐ด)) |
58 | | simpr 484 |
. . . . . . . . . 10
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ
0s โคs ๐ต) |
59 | 52, 47, 57, 58 | mulsge0d 27965 |
. . . . . . . . 9
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ
0s โคs (( -us โ๐ด) ยทs ๐ต)) |
60 | 59, 48 | breqtrd 5165 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ
0s โคs ( -us โ(๐ด ยทs ๐ต))) |
61 | 20, 60 | eqbrtrid 5174 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ (
-us โ 0s ) โคs ( -us โ(๐ด ยทs ๐ต))) |
62 | 51 | adantr 480 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ (๐ด ยทs ๐ต) โ
No ) |
63 | 62, 54 | slenegd 27879 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ ((๐ด ยทs ๐ต) โคs 0s โ (
-us โ 0s ) โคs ( -us โ(๐ด ยทs ๐ต)))) |
64 | 61, 63 | mpbird 257 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ (๐ด ยทs ๐ต) โคs 0s
) |
65 | 51, 64, 35 | syl2an2r 682 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ
(abssโ(๐ด
ยทs ๐ต)) =
( -us โ(๐ด
ยทs ๐ต))) |
66 | 48, 50, 65 | 3eqtr4rd 2775 |
. . . 4
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง 0s
โคs ๐ต) โ
(abssโ(๐ด
ยทs ๐ต)) =
(( -us โ๐ด)
ยทs (abssโ๐ต))) |
67 | | simplll 772 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
๐ด โ No ) |
68 | | simpllr 773 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
๐ต โ No ) |
69 | 67, 68 | mul2negsd 27981 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ ((
-us โ๐ด)
ยทs ( -us โ๐ต)) = (๐ด ยทs ๐ต)) |
70 | 17 | ad4ant24 751 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
(abssโ๐ต) =
( -us โ๐ต)) |
71 | 70 | oveq2d 7418 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ ((
-us โ๐ด)
ยทs (abssโ๐ต)) = (( -us โ๐ด) ยทs (
-us โ๐ต))) |
72 | 67 | negscld 27868 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ (
-us โ๐ด)
โ No ) |
73 | 68 | negscld 27868 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ (
-us โ๐ต)
โ No ) |
74 | | simplr 766 |
. . . . . . . . . 10
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
๐ด โคs 0s
) |
75 | 24 | a1i 11 |
. . . . . . . . . . 11
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
0s โ No ) |
76 | 67, 75 | slenegd 27879 |
. . . . . . . . . 10
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
(๐ด โคs 0s
โ ( -us โ 0s ) โคs ( -us
โ๐ด))) |
77 | 74, 76 | mpbid 231 |
. . . . . . . . 9
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ (
-us โ 0s ) โคs ( -us โ๐ด)) |
78 | 20, 77 | eqbrtrrid 5175 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
0s โคs ( -us โ๐ด)) |
79 | | simpr 484 |
. . . . . . . . . 10
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
๐ต โคs 0s
) |
80 | 68, 75 | slenegd 27879 |
. . . . . . . . . 10
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
(๐ต โคs 0s
โ ( -us โ 0s ) โคs ( -us
โ๐ต))) |
81 | 79, 80 | mpbid 231 |
. . . . . . . . 9
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ (
-us โ 0s ) โคs ( -us โ๐ต)) |
82 | 20, 81 | eqbrtrrid 5175 |
. . . . . . . 8
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
0s โคs ( -us โ๐ต)) |
83 | 72, 73, 78, 82 | mulsge0d 27965 |
. . . . . . 7
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
0s โคs (( -us โ๐ด) ยทs ( -us
โ๐ต))) |
84 | 83, 69 | breqtrd 5165 |
. . . . . 6
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
0s โคs (๐ด
ยทs ๐ต)) |
85 | 51, 84, 8 | syl2an2r 682 |
. . . . 5
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
(abssโ(๐ด
ยทs ๐ต)) =
(๐ด ยทs
๐ต)) |
86 | 69, 71, 85 | 3eqtr4rd 2775 |
. . . 4
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โง ๐ต โคs 0s ) โ
(abssโ(๐ด
ยทs ๐ต)) =
(( -us โ๐ด)
ยทs (abssโ๐ต))) |
87 | 39 | ad2antlr 724 |
. . . 4
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โ (
0s โคs ๐ต โจ
๐ต โคs 0s
)) |
88 | 66, 86, 87 | mpjaodan 955 |
. . 3
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โ
(abssโ(๐ด
ยทs ๐ต)) =
(( -us โ๐ด)
ยทs (abssโ๐ต))) |
89 | | abssnid 28056 |
. . . . 5
โข ((๐ด โ
No โง ๐ด โคs
0s ) โ (abssโ๐ด) = ( -us โ๐ด)) |
90 | 89 | oveq1d 7417 |
. . . 4
โข ((๐ด โ
No โง ๐ด โคs
0s ) โ ((abssโ๐ด) ยทs
(abssโ๐ต))
= (( -us โ๐ด) ยทs
(abssโ๐ต))) |
91 | 90 | adantlr 712 |
. . 3
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โ
((abssโ๐ด)
ยทs (abssโ๐ต)) = (( -us โ๐ด) ยทs
(abssโ๐ต))) |
92 | 88, 91 | eqtr4d 2767 |
. 2
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ด โคs 0s ) โ
(abssโ(๐ด
ยทs ๐ต)) =
((abssโ๐ด)
ยทs (abssโ๐ต))) |
93 | | sletric 27616 |
. . . 4
โข ((
0s โ No โง ๐ด โ No )
โ ( 0s โคs ๐ด โจ ๐ด โคs 0s )) |
94 | 24, 93 | mpan 687 |
. . 3
โข (๐ด โ
No โ ( 0s โคs ๐ด โจ ๐ด โคs 0s )) |
95 | 94 | adantr 480 |
. 2
โข ((๐ด โ
No โง ๐ต โ
No ) โ ( 0s โคs ๐ด โจ ๐ด โคs 0s )) |
96 | 45, 92, 95 | mpjaodan 955 |
1
โข ((๐ด โ
No โง ๐ต โ
No ) โ (abssโ(๐ด ยทs ๐ต)) =
((abssโ๐ด)
ยทs (abssโ๐ต))) |