Step | Hyp | Ref
| Expression |
1 | | 0z 9263 |
. . . . . . . . 9
โข 0 โ
โค |
2 | | 0le1 8437 |
. . . . . . . . 9
โข 0 โค
1 |
3 | | fveq2 5515 |
. . . . . . . . . . . 12
โข (๐ฅ = 0 โ (absโ๐ฅ) =
(absโ0)) |
4 | | abs0 11066 |
. . . . . . . . . . . 12
โข
(absโ0) = 0 |
5 | 3, 4 | eqtrdi 2226 |
. . . . . . . . . . 11
โข (๐ฅ = 0 โ (absโ๐ฅ) = 0) |
6 | 5 | breq1d 4013 |
. . . . . . . . . 10
โข (๐ฅ = 0 โ ((absโ๐ฅ) โค 1 โ 0 โค
1)) |
7 | | lgsfcl2.z |
. . . . . . . . . 10
โข ๐ = {๐ฅ โ โค โฃ (absโ๐ฅ) โค 1} |
8 | 6, 7 | elrab2 2896 |
. . . . . . . . 9
โข (0 โ
๐ โ (0 โ โค
โง 0 โค 1)) |
9 | 1, 2, 8 | mpbir2an 942 |
. . . . . . . 8
โข 0 โ
๐ |
10 | 9 | a1i 9 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ 0 โ ๐) |
11 | | 1z 9278 |
. . . . . . . . . 10
โข 1 โ
โค |
12 | | 1le1 8528 |
. . . . . . . . . 10
โข 1 โค
1 |
13 | | fveq2 5515 |
. . . . . . . . . . . . 13
โข (๐ฅ = 1 โ (absโ๐ฅ) =
(absโ1)) |
14 | | abs1 11080 |
. . . . . . . . . . . . 13
โข
(absโ1) = 1 |
15 | 13, 14 | eqtrdi 2226 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ (absโ๐ฅ) = 1) |
16 | 15 | breq1d 4013 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ ((absโ๐ฅ) โค 1 โ 1 โค
1)) |
17 | 16, 7 | elrab2 2896 |
. . . . . . . . . 10
โข (1 โ
๐ โ (1 โ โค
โง 1 โค 1)) |
18 | 11, 12, 17 | mpbir2an 942 |
. . . . . . . . 9
โข 1 โ
๐ |
19 | 18 | a1i 9 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ 1 โ ๐) |
20 | | neg1z 9284 |
. . . . . . . . . 10
โข -1 โ
โค |
21 | | fveq2 5515 |
. . . . . . . . . . . . 13
โข (๐ฅ = -1 โ (absโ๐ฅ) =
(absโ-1)) |
22 | | ax-1cn 7903 |
. . . . . . . . . . . . . . 15
โข 1 โ
โ |
23 | 22 | absnegi 11155 |
. . . . . . . . . . . . . 14
โข
(absโ-1) = (absโ1) |
24 | 23, 14 | eqtri 2198 |
. . . . . . . . . . . . 13
โข
(absโ-1) = 1 |
25 | 21, 24 | eqtrdi 2226 |
. . . . . . . . . . . 12
โข (๐ฅ = -1 โ (absโ๐ฅ) = 1) |
26 | 25 | breq1d 4013 |
. . . . . . . . . . 11
โข (๐ฅ = -1 โ ((absโ๐ฅ) โค 1 โ 1 โค
1)) |
27 | 26, 7 | elrab2 2896 |
. . . . . . . . . 10
โข (-1
โ ๐ โ (-1 โ
โค โง 1 โค 1)) |
28 | 20, 12, 27 | mpbir2an 942 |
. . . . . . . . 9
โข -1 โ
๐ |
29 | 28 | a1i 9 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ -1 โ ๐) |
30 | | simp1 997 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ ๐ด โ
โค) |
31 | | 8nn 9085 |
. . . . . . . . . . . . . 14
โข 8 โ
โ |
32 | 31 | a1i 9 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ 8 โ
โ) |
33 | 30, 32 | zmodcld 10344 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ (๐ด mod 8) โ
โ0) |
34 | 33 | nn0zd 9372 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ (๐ด mod 8) โ
โค) |
35 | | zdceq 9327 |
. . . . . . . . . . 11
โข (((๐ด mod 8) โ โค โง 1
โ โค) โ DECID (๐ด mod 8) = 1) |
36 | 34, 11, 35 | sylancl 413 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ
DECID (๐ด mod
8) = 1) |
37 | | 7nn 9084 |
. . . . . . . . . . . 12
โข 7 โ
โ |
38 | 37 | nnzi 9273 |
. . . . . . . . . . 11
โข 7 โ
โค |
39 | | zdceq 9327 |
. . . . . . . . . . 11
โข (((๐ด mod 8) โ โค โง 7
โ โค) โ DECID (๐ด mod 8) = 7) |
40 | 34, 38, 39 | sylancl 413 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ
DECID (๐ด mod
8) = 7) |
41 | | dcor 935 |
. . . . . . . . . 10
โข
(DECID (๐ด mod 8) = 1 โ (DECID
(๐ด mod 8) = 7 โ
DECID ((๐ด
mod 8) = 1 โจ (๐ด mod 8) =
7))) |
42 | 36, 40, 41 | sylc 62 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ
DECID ((๐ด
mod 8) = 1 โจ (๐ด mod 8) =
7)) |
43 | | elprg 3612 |
. . . . . . . . . . 11
โข ((๐ด mod 8) โ
โ0 โ ((๐ด mod 8) โ {1, 7} โ ((๐ด mod 8) = 1 โจ (๐ด mod 8) = 7))) |
44 | 33, 43 | syl 14 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ ((๐ด mod 8) โ {1, 7} โ
((๐ด mod 8) = 1 โจ (๐ด mod 8) = 7))) |
45 | 44 | dcbid 838 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ
(DECID (๐ด
mod 8) โ {1, 7} โ DECID ((๐ด mod 8) = 1 โจ (๐ด mod 8) = 7))) |
46 | 42, 45 | mpbird 167 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ
DECID (๐ด mod
8) โ {1, 7}) |
47 | 19, 29, 46 | ifcldcd 3570 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ if((๐ด mod 8) โ {1, 7}, 1, -1)
โ ๐) |
48 | | 2nn 9079 |
. . . . . . . . 9
โข 2 โ
โ |
49 | 48 | a1i 9 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ 2 โ
โ) |
50 | | dvdsdc 11804 |
. . . . . . . 8
โข ((2
โ โ โง ๐ด
โ โค) โ DECID 2 โฅ ๐ด) |
51 | 49, 30, 50 | syl2anc 411 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ
DECID 2 โฅ ๐ด) |
52 | 10, 47, 51 | ifcldcd 3570 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ if(2 โฅ
๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)) โ ๐) |
53 | 52 | ad3antrrr 492 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ๐ = 2) โ if(2
โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1))
โ ๐) |
54 | | simpl1 1000 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โ ๐ด โ
โค) |
55 | 54 | ad2antrr 488 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
๐ด โ
โค) |
56 | | simplr 528 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
๐ โ
โ) |
57 | | simpr 110 |
. . . . . . . 8
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
ยฌ ๐ =
2) |
58 | 57 | neqned 2354 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
๐ โ 2) |
59 | | eldifsn 3719 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง ๐ โ
2)) |
60 | 56, 58, 59 | sylanbrc 417 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
๐ โ (โ โ
{2})) |
61 | 7 | lgslem4 14374 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ (โ โ {2}))
โ ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1) โ ๐) |
62 | 55, 60, 61 | syl2anc 411 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1) โ ๐) |
63 | | simplr 528 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ
โ) |
64 | 63 | nnzd 9373 |
. . . . . 6
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ
โค) |
65 | | 2z 9280 |
. . . . . 6
โข 2 โ
โค |
66 | | zdceq 9327 |
. . . . . 6
โข ((๐ โ โค โง 2 โ
โค) โ DECID ๐ = 2) |
67 | 64, 65, 66 | sylancl 413 |
. . . . 5
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ
DECID ๐ =
2) |
68 | 53, 62, 67 | ifcldadc 3563 |
. . . 4
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ if(๐ = 2, if(2 โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1)) โ ๐) |
69 | | simpr 110 |
. . . . 5
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ
โ) |
70 | | simpll2 1037 |
. . . . 5
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ
โค) |
71 | | simpll3 1038 |
. . . . 5
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ 0) |
72 | | pczcl 12297 |
. . . . 5
โข ((๐ โ โ โง (๐ โ โค โง ๐ โ 0)) โ (๐ pCnt ๐) โ
โ0) |
73 | 69, 70, 71, 72 | syl12anc 1236 |
. . . 4
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ (๐ pCnt ๐) โ
โ0) |
74 | 7 | ssrab3 3241 |
. . . . . 6
โข ๐ โ
โค |
75 | | zsscn 9260 |
. . . . . 6
โข โค
โ โ |
76 | 74, 75 | sstri 3164 |
. . . . 5
โข ๐ โ
โ |
77 | 7 | lgslem3 14373 |
. . . . 5
โข ((๐ โ ๐ โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) |
78 | 76, 77, 18 | expcllem 10530 |
. . . 4
โข
((if(๐ = 2, if(2
โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)),
((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1)) โ ๐ โง (๐ pCnt ๐) โ โ0) โ
(if(๐ = 2, if(2 โฅ
๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)) โ ๐) |
79 | 68, 73, 78 | syl2anc 411 |
. . 3
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ
(if(๐ = 2, if(2 โฅ
๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)) โ ๐) |
80 | 18 | a1i 9 |
. . 3
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ยฌ
๐ โ โ) โ 1
โ ๐) |
81 | | simpr 110 |
. . . 4
โข (((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โ ๐ โ
โ) |
82 | | prmdc 12129 |
. . . 4
โข (๐ โ โ โ
DECID ๐
โ โ) |
83 | 81, 82 | syl 14 |
. . 3
โข (((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โ
DECID ๐
โ โ) |
84 | 79, 80, 83 | ifcldadc 3563 |
. 2
โข (((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โ if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1) โ ๐) |
85 | | lgsval.1 |
. 2
โข ๐น = (๐ โ โ โฆ if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1)) |
86 | 84, 85 | fmptd 5670 |
1
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ ๐น:โโถ๐) |