Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
โข ((๐ = ๐ด โง ๐ = ๐) โ ๐ = ๐) |
2 | 1 | eqeq1d 2739 |
. . 3
โข ((๐ = ๐ด โง ๐ = ๐) โ (๐ = 0 โ ๐ = 0)) |
3 | | simpl 484 |
. . . . . 6
โข ((๐ = ๐ด โง ๐ = ๐) โ ๐ = ๐ด) |
4 | 3 | oveq1d 7377 |
. . . . 5
โข ((๐ = ๐ด โง ๐ = ๐) โ (๐โ2) = (๐ดโ2)) |
5 | 4 | eqeq1d 2739 |
. . . 4
โข ((๐ = ๐ด โง ๐ = ๐) โ ((๐โ2) = 1 โ (๐ดโ2) = 1)) |
6 | 5 | ifbid 4514 |
. . 3
โข ((๐ = ๐ด โง ๐ = ๐) โ if((๐โ2) = 1, 1, 0) = if((๐ดโ2) = 1, 1, 0)) |
7 | 1 | breq1d 5120 |
. . . . . 6
โข ((๐ = ๐ด โง ๐ = ๐) โ (๐ < 0 โ ๐ < 0)) |
8 | 3 | breq1d 5120 |
. . . . . 6
โข ((๐ = ๐ด โง ๐ = ๐) โ (๐ < 0 โ ๐ด < 0)) |
9 | 7, 8 | anbi12d 632 |
. . . . 5
โข ((๐ = ๐ด โง ๐ = ๐) โ ((๐ < 0 โง ๐ < 0) โ (๐ < 0 โง ๐ด < 0))) |
10 | 9 | ifbid 4514 |
. . . 4
โข ((๐ = ๐ด โง ๐ = ๐) โ if((๐ < 0 โง ๐ < 0), -1, 1) = if((๐ < 0 โง ๐ด < 0), -1, 1)) |
11 | 3 | breq2d 5122 |
. . . . . . . . . . . 12
โข ((๐ = ๐ด โง ๐ = ๐) โ (2 โฅ ๐ โ 2 โฅ ๐ด)) |
12 | 3 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข ((๐ = ๐ด โง ๐ = ๐) โ (๐ mod 8) = (๐ด mod 8)) |
13 | 12 | eleq1d 2823 |
. . . . . . . . . . . . 13
โข ((๐ = ๐ด โง ๐ = ๐) โ ((๐ mod 8) โ {1, 7} โ (๐ด mod 8) โ {1,
7})) |
14 | 13 | ifbid 4514 |
. . . . . . . . . . . 12
โข ((๐ = ๐ด โง ๐ = ๐) โ if((๐ mod 8) โ {1, 7}, 1, -1) = if((๐ด mod 8) โ {1, 7}, 1,
-1)) |
15 | 11, 14 | ifbieq2d 4517 |
. . . . . . . . . . 11
โข ((๐ = ๐ด โง ๐ = ๐) โ if(2 โฅ ๐, 0, if((๐ mod 8) โ {1, 7}, 1, -1)) = if(2 โฅ
๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1,
-1))) |
16 | 3 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข ((๐ = ๐ด โง ๐ = ๐) โ (๐โ((๐ โ 1) / 2)) = (๐ดโ((๐ โ 1) / 2))) |
17 | 16 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข ((๐ = ๐ด โง ๐ = ๐) โ ((๐โ((๐ โ 1) / 2)) + 1) = ((๐ดโ((๐ โ 1) / 2)) + 1)) |
18 | 17 | oveq1d 7377 |
. . . . . . . . . . . 12
โข ((๐ = ๐ด โง ๐ = ๐) โ (((๐โ((๐ โ 1) / 2)) + 1) mod ๐) = (((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐)) |
19 | 18 | oveq1d 7377 |
. . . . . . . . . . 11
โข ((๐ = ๐ด โง ๐ = ๐) โ ((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1) = ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1)) |
20 | 15, 19 | ifeq12d 4512 |
. . . . . . . . . 10
โข ((๐ = ๐ด โง ๐ = ๐) โ if(๐ = 2, if(2 โฅ ๐, 0, if((๐ mod 8) โ {1, 7}, 1, -1)), ((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1)) = if(๐ = 2, if(2 โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))) |
21 | 1 | oveq2d 7378 |
. . . . . . . . . 10
โข ((๐ = ๐ด โง ๐ = ๐) โ (๐ pCnt ๐) = (๐ pCnt ๐)) |
22 | 20, 21 | oveq12d 7380 |
. . . . . . . . 9
โข ((๐ = ๐ด โง ๐ = ๐) โ (if(๐ = 2, if(2 โฅ ๐, 0, if((๐ mod 8) โ {1, 7}, 1, -1)), ((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)) = (if(๐ = 2, if(2 โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐))) |
23 | 22 | ifeq1d 4510 |
. . . . . . . 8
โข ((๐ = ๐ด โง ๐ = ๐) โ if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐, 0, if((๐ mod 8) โ {1, 7}, 1, -1)), ((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1) = if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1)) |
24 | 23 | mpteq2dv 5212 |
. . . . . . 7
โข ((๐ = ๐ด โง ๐ = ๐) โ (๐ โ โ โฆ if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐, 0, if((๐ mod 8) โ {1, 7}, 1, -1)), ((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1)) = (๐ โ โ โฆ if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1))) |
25 | | lgsval.1 |
. . . . . . 7
โข ๐น = (๐ โ โ โฆ if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐ด, 0, if((๐ด mod 8) โ {1, 7}, 1, -1)), ((((๐ดโ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1)) |
26 | 24, 25 | eqtr4di 2795 |
. . . . . 6
โข ((๐ = ๐ด โง ๐ = ๐) โ (๐ โ โ โฆ if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐, 0, if((๐ mod 8) โ {1, 7}, 1, -1)), ((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1)) = ๐น) |
27 | 26 | seqeq3d 13921 |
. . . . 5
โข ((๐ = ๐ด โง ๐ = ๐) โ seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐, 0, if((๐ mod 8) โ {1, 7}, 1, -1)), ((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1))) = seq1( ยท , ๐น)) |
28 | 1 | fveq2d 6851 |
. . . . 5
โข ((๐ = ๐ด โง ๐ = ๐) โ (absโ๐) = (absโ๐)) |
29 | 27, 28 | fveq12d 6854 |
. . . 4
โข ((๐ = ๐ด โง ๐ = ๐) โ (seq1( ยท , (๐ โ โ โฆ if(๐ โ โ, (if(๐ = 2, if(2 โฅ ๐, 0, if((๐ mod 8) โ {1, 7}, 1, -1)), ((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1)))โ(absโ๐)) = (seq1( ยท , ๐น)โ(absโ๐))) |
30 | 10, 29 | oveq12d 7380 |
. . 3
โข ((๐ = ๐ด โง ๐ = ๐) โ (if((๐ < 0 โง ๐ < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
(if(๐ = 2, if(2 โฅ
๐, 0, if((๐ mod 8) โ {1, 7}, 1, -1)),
((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1)))โ(absโ๐))) = (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท (seq1( ยท ,
๐น)โ(absโ๐)))) |
31 | 2, 6, 30 | ifbieq12d 4519 |
. 2
โข ((๐ = ๐ด โง ๐ = ๐) โ if(๐ = 0, if((๐โ2) = 1, 1, 0), (if((๐ < 0 โง ๐ < 0), -1, 1) ยท (seq1( ยท ,
(๐ โ โ โฆ
if(๐ โ โ,
(if(๐ = 2, if(2 โฅ
๐, 0, if((๐ mod 8) โ {1, 7}, 1, -1)),
((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1)))โ(absโ๐)))) = if(๐ = 0, if((๐ดโ2) = 1, 1, 0), (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท (seq1( ยท ,
๐น)โ(absโ๐))))) |
32 | | df-lgs 26659 |
. 2
โข
/L = (๐
โ โค, ๐ โ
โค โฆ if(๐ = 0,
if((๐โ2) = 1, 1, 0),
(if((๐ < 0 โง ๐ < 0), -1, 1) ยท (seq1(
ยท , (๐ โ
โ โฆ if(๐ โ
โ, (if(๐ = 2, if(2
โฅ ๐, 0, if((๐ mod 8) โ {1, 7}, 1, -1)),
((((๐โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1))โ(๐ pCnt ๐)), 1)))โ(absโ๐))))) |
33 | | 1nn0 12436 |
. . . . 5
โข 1 โ
โ0 |
34 | | 0nn0 12435 |
. . . . 5
โข 0 โ
โ0 |
35 | 33, 34 | ifcli 4538 |
. . . 4
โข if((๐ดโ2) = 1, 1, 0) โ
โ0 |
36 | 35 | elexi 3467 |
. . 3
โข if((๐ดโ2) = 1, 1, 0) โ
V |
37 | | ovex 7395 |
. . 3
โข
(if((๐ < 0 โง
๐ด < 0), -1, 1) ยท
(seq1( ยท , ๐น)โ(absโ๐))) โ V |
38 | 36, 37 | ifex 4541 |
. 2
โข if(๐ = 0, if((๐ดโ2) = 1, 1, 0), (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท (seq1( ยท ,
๐น)โ(absโ๐)))) โ V |
39 | 31, 32, 38 | ovmpoa 7515 |
1
โข ((๐ด โ โค โง ๐ โ โค) โ (๐ด /L ๐) = if(๐ = 0, if((๐ดโ2) = 1, 1, 0), (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท (seq1( ยท ,
๐น)โ(absโ๐))))) |