Step | Hyp | Ref
| Expression |
1 | | 0z 12517 |
. . . . . . . 8
โข 0 โ
โค |
2 | | 0le1 11685 |
. . . . . . . 8
โข 0 โค
1 |
3 | | fveq2 6847 |
. . . . . . . . . . 11
โข (๐ฅ = 0 โ (absโ๐ฅ) =
(absโ0)) |
4 | | abs0 15177 |
. . . . . . . . . . 11
โข
(absโ0) = 0 |
5 | 3, 4 | eqtrdi 2793 |
. . . . . . . . . 10
โข (๐ฅ = 0 โ (absโ๐ฅ) = 0) |
6 | 5 | breq1d 5120 |
. . . . . . . . 9
โข (๐ฅ = 0 โ ((absโ๐ฅ) โค 1 โ 0 โค
1)) |
7 | | lgsfcl2.z |
. . . . . . . . 9
โข ๐ = {๐ฅ โ โค โฃ (absโ๐ฅ) โค 1} |
8 | 6, 7 | elrab2 3653 |
. . . . . . . 8
โข (0 โ
๐ โ (0 โ โค
โง 0 โค 1)) |
9 | 1, 2, 8 | mpbir2an 710 |
. . . . . . 7
โข 0 โ
๐ |
10 | | 1z 12540 |
. . . . . . . . 9
โข 1 โ
โค |
11 | | 1le1 11790 |
. . . . . . . . 9
โข 1 โค
1 |
12 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ (absโ๐ฅ) =
(absโ1)) |
13 | | abs1 15189 |
. . . . . . . . . . . 12
โข
(absโ1) = 1 |
14 | 12, 13 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ (absโ๐ฅ) = 1) |
15 | 14 | breq1d 5120 |
. . . . . . . . . 10
โข (๐ฅ = 1 โ ((absโ๐ฅ) โค 1 โ 1 โค
1)) |
16 | 15, 7 | elrab2 3653 |
. . . . . . . . 9
โข (1 โ
๐ โ (1 โ โค
โง 1 โค 1)) |
17 | 10, 11, 16 | mpbir2an 710 |
. . . . . . . 8
โข 1 โ
๐ |
18 | | neg1z 12546 |
. . . . . . . . 9
โข -1 โ
โค |
19 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ฅ = -1 โ (absโ๐ฅ) =
(absโ-1)) |
20 | | ax-1cn 11116 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
21 | 20 | absnegi 15292 |
. . . . . . . . . . . . 13
โข
(absโ-1) = (absโ1) |
22 | 21, 13 | eqtri 2765 |
. . . . . . . . . . . 12
โข
(absโ-1) = 1 |
23 | 19, 22 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (๐ฅ = -1 โ (absโ๐ฅ) = 1) |
24 | 23 | breq1d 5120 |
. . . . . . . . . 10
โข (๐ฅ = -1 โ ((absโ๐ฅ) โค 1 โ 1 โค
1)) |
25 | 24, 7 | elrab2 3653 |
. . . . . . . . 9
โข (-1
โ ๐ โ (-1 โ
โค โง 1 โค 1)) |
26 | 18, 11, 25 | mpbir2an 710 |
. . . . . . . 8
โข -1 โ
๐ |
27 | 17, 26 | ifcli 4538 |
. . . . . . 7
โข if((๐ด mod 8) โ {1, 7}, 1, -1)
โ ๐ |
28 | 9, 27 | ifcli 4538 |
. . . . . 6
โข if(2
โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1))
โ ๐ |
29 | 28 | a1i 11 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ๐ = 2) โ if(2
โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1))
โ ๐) |
30 | | simpl1 1192 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โ ๐ด โ
โค) |
31 | 30 | ad2antrr 725 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
๐ด โ
โค) |
32 | | simplr 768 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
๐ โ
โ) |
33 | | simpr 486 |
. . . . . . . 8
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
ยฌ ๐ =
2) |
34 | 33 | neqned 2951 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
๐ โ 2) |
35 | | eldifsn 4752 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง ๐ โ
2)) |
36 | 32, 34, 35 | sylanbrc 584 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
๐ โ (โ โ
{2})) |
37 | 7 | lgslem4 26664 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ (โ โ {2}))
โ ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1) โ ๐) |
38 | 31, 36, 37 | syl2anc 585 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ โ
โค โง ๐ โ 0)
โง ๐ โ โ)
โง ๐ โ โ)
โง ยฌ ๐ = 2) โ
((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1) โ ๐) |
39 | 29, 38 | ifclda 4526 |
. . . 4
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ if(๐ = 2, if(2 โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1)) โ ๐) |
40 | | simpr 486 |
. . . . 5
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ
โ) |
41 | | simpll2 1214 |
. . . . 5
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ
โค) |
42 | | simpll3 1215 |
. . . . 5
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ 0) |
43 | | pczcl 16727 |
. . . . 5
โข ((๐ โ โ โง (๐ โ โค โง ๐ โ 0)) โ (๐ pCnt ๐) โ
โ0) |
44 | 40, 41, 42, 43 | syl12anc 836 |
. . . 4
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ (๐ pCnt ๐) โ
โ0) |
45 | 7 | ssrab3 4045 |
. . . . . 6
โข ๐ โ
โค |
46 | | zsscn 12514 |
. . . . . 6
โข โค
โ โ |
47 | 45, 46 | sstri 3958 |
. . . . 5
โข ๐ โ
โ |
48 | 7 | lgslem3 26663 |
. . . . 5
โข ((๐ โ ๐ โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) |
49 | 47, 48, 17 | expcllem 13985 |
. . . 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 ๐)) โ ๐) |
50 | 39, 44, 49 | syl2anc 585 |
. . 3
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ๐ โ โ) โ
(if(๐ = 2, if(2 โฅ
๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)) โ ๐) |
51 | 17 | a1i 11 |
. . 3
โข ((((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โง ยฌ
๐ โ โ) โ 1
โ ๐) |
52 | 50, 51 | ifclda 4526 |
. 2
โข (((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โง ๐ โ โ) โ if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1) โ ๐) |
53 | | lgsval.1 |
. 2
โข ๐น = (๐ โ โ โฆ if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1)) |
54 | 52, 53 | fmptd 7067 |
1
โข ((๐ด โ โค โง ๐ โ โค โง ๐ โ 0) โ ๐น:โโถ๐) |