Step | Hyp | Ref
| Expression |
1 | | prmz 16558 |
. . 3
β’ (π β β β π β
β€) |
2 | | lgsval.1 |
. . . 4
β’ πΉ = (π β β β¦ if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) |
3 | 2 | lgsval 26665 |
. . 3
β’ ((π΄ β β€ β§ π β β€) β (π΄ /L π) = if(π = 0, if((π΄β2) = 1, 1, 0), (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
πΉ)β(absβπ))))) |
4 | 1, 3 | sylan2 594 |
. 2
β’ ((π΄ β β€ β§ π β β) β (π΄ /L π) = if(π = 0, if((π΄β2) = 1, 1, 0), (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
πΉ)β(absβπ))))) |
5 | | prmnn 16557 |
. . . . . 6
β’ (π β β β π β
β) |
6 | 5 | adantl 483 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β π β
β) |
7 | 6 | nnne0d 12210 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β π β 0) |
8 | 7 | neneqd 2949 |
. . 3
β’ ((π΄ β β€ β§ π β β) β Β¬
π = 0) |
9 | 8 | iffalsed 4502 |
. 2
β’ ((π΄ β β€ β§ π β β) β if(π = 0, if((π΄β2) = 1, 1, 0), (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
πΉ)β(absβπ)))) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
πΉ)β(absβπ)))) |
10 | 6 | nnnn0d 12480 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β π β
β0) |
11 | 10 | nn0ge0d 12483 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β 0 β€
π) |
12 | | 0re 11164 |
. . . . . . . 8
β’ 0 β
β |
13 | 6 | nnred 12175 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β π β
β) |
14 | | lenlt 11240 |
. . . . . . . 8
β’ ((0
β β β§ π
β β) β (0 β€ π β Β¬ π < 0)) |
15 | 12, 13, 14 | sylancr 588 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β (0 β€
π β Β¬ π < 0)) |
16 | 11, 15 | mpbid 231 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β Β¬
π < 0) |
17 | 16 | intnanrd 491 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β Β¬
(π < 0 β§ π΄ < 0)) |
18 | 17 | iffalsed 4502 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β
if((π < 0 β§ π΄ < 0), -1, 1) =
1) |
19 | 13, 11 | absidd 15314 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β
(absβπ) = π) |
20 | 19 | fveq2d 6851 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)β(absβπ)) = (seq1( Β· , πΉ)βπ)) |
21 | | 1z 12540 |
. . . . . . 7
β’ 1 β
β€ |
22 | | prmuz2 16579 |
. . . . . . . . 9
β’ (π β β β π β
(β€β₯β2)) |
23 | 22 | adantl 483 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β π β
(β€β₯β2)) |
24 | | df-2 12223 |
. . . . . . . . 9
β’ 2 = (1 +
1) |
25 | 24 | fveq2i 6850 |
. . . . . . . 8
β’
(β€β₯β2) = (β€β₯β(1 +
1)) |
26 | 23, 25 | eleqtrdi 2848 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β π β
(β€β₯β(1 + 1))) |
27 | | seqm1 13932 |
. . . . . . 7
β’ ((1
β β€ β§ π
β (β€β₯β(1 + 1))) β (seq1( Β· , πΉ)βπ) = ((seq1( Β· , πΉ)β(π β 1)) Β· (πΉβπ))) |
28 | 21, 26, 27 | sylancr 588 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)βπ) = ((seq1( Β· , πΉ)β(π β 1)) Β· (πΉβπ))) |
29 | | 1t1e1 12322 |
. . . . . . . . 9
β’ (1
Β· 1) = 1 |
30 | 29 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β (1
Β· 1) = 1) |
31 | | uz2m1nn 12855 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β (π β 1) β β) |
32 | 23, 31 | syl 17 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β) β (π β 1) β
β) |
33 | | nnuz 12813 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
34 | 32, 33 | eleqtrdi 2848 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β (π β 1) β
(β€β₯β1)) |
35 | | elfznn 13477 |
. . . . . . . . . . 11
β’ (π₯ β (1...(π β 1)) β π₯ β β) |
36 | 35 | adantl 483 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β π₯ β β) |
37 | 2 | lgsfval 26666 |
. . . . . . . . . 10
β’ (π₯ β β β (πΉβπ₯) = if(π₯ β β, (if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1))β(π₯ pCnt π)), 1)) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β (πΉβπ₯) = if(π₯ β β, (if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1))β(π₯ pCnt π)), 1)) |
39 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...(π β 1)) β π β β€) |
40 | 39 | zred 12614 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...(π β 1)) β π β β) |
41 | 40 | ltm1d 12094 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...(π β 1)) β (π β 1) < π) |
42 | | peano2rem 11475 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β (π β 1) β
β) |
43 | 40, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...(π β 1)) β (π β 1) β β) |
44 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...(π β 1)) β π β€ (π β 1)) |
45 | 40, 43, 44 | lensymd 11313 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...(π β 1)) β Β¬ (π β 1) < π) |
46 | 41, 45 | pm2.65i 193 |
. . . . . . . . . . . . . . . . . 18
β’ Β¬
π β (1...(π β 1)) |
47 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (π₯ β (1...(π β 1)) β π β (1...(π β 1)))) |
48 | 46, 47 | mtbiri 327 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β Β¬ π₯ β (1...(π β 1))) |
49 | 48 | con2i 139 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (1...(π β 1)) β Β¬ π₯ = π) |
50 | 49 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β Β¬ π₯ = π) |
51 | | prmuz2 16579 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β π₯ β
(β€β₯β2)) |
52 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β π β β) |
53 | | dvdsprm 16586 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β
(β€β₯β2) β§ π β β) β (π₯ β₯ π β π₯ = π)) |
54 | 51, 52, 53 | syl2an2 685 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β (π₯ β₯ π β π₯ = π)) |
55 | 50, 54 | mtbird 325 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β Β¬ π₯ β₯ π) |
56 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β π₯ β β) |
57 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β π β β) |
58 | | pceq0 16750 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π β β) β ((π₯ pCnt π) = 0 β Β¬ π₯ β₯ π)) |
59 | 56, 57, 58 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β ((π₯ pCnt π) = 0 β Β¬ π₯ β₯ π)) |
60 | 55, 59 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β (π₯ pCnt π) = 0) |
61 | 60 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β (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))β0)) |
62 | | 0z 12517 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β
β€ |
63 | | neg1z 12546 |
. . . . . . . . . . . . . . . . . . 19
β’ -1 β
β€ |
64 | 21, 63 | ifcli 4538 |
. . . . . . . . . . . . . . . . . 18
β’ if((π΄ mod 8) β {1, 7}, 1, -1)
β β€ |
65 | 62, 64 | ifcli 4538 |
. . . . . . . . . . . . . . . . 17
β’ if(2
β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1))
β β€ |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ π₯ = 2) β if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)) β
β€) |
67 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β β€ β§ π β β) β π΄ β
β€) |
68 | 67 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β π΄ β
β€) |
69 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β π₯ β
β) |
70 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β Β¬ π₯ = 2) |
71 | 70 | neqned 2951 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β π₯ β 2) |
72 | | eldifsn 4752 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β (β β {2})
β (π₯ β β
β§ π₯ β
2)) |
73 | 69, 71, 72 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β π₯ β (β β
{2})) |
74 | | oddprm 16689 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ β (β β {2})
β ((π₯ β 1) / 2)
β β) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β ((π₯ β 1) / 2) β
β) |
76 | 75 | nnnn0d 12480 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β ((π₯ β 1) / 2) β
β0) |
77 | | zexpcl 13989 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ β β€ β§ ((π₯ β 1) / 2) β
β0) β (π΄β((π₯ β 1) / 2)) β
β€) |
78 | 68, 76, 77 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β (π΄β((π₯ β 1) / 2)) β
β€) |
79 | 78 | peano2zd 12617 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β ((π΄β((π₯ β 1) / 2)) + 1) β
β€) |
80 | | prmnn 16557 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β β π₯ β
β) |
81 | 80 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β π₯ β
β) |
82 | 79, 81 | zmodcld 13804 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β (((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β
β0) |
83 | 82 | nn0zd 12532 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β (((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β β€) |
84 | | peano2zm 12553 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β β€ β ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1) β β€) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1) β β€) |
86 | 66, 85 | ifclda 4526 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β€ β§ π β β) β§ π₯ β β) β if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1)) β
β€) |
87 | 86 | zcnd 12615 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β€ β§ π β β) β§ π₯ β β) β if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1)) β
β) |
88 | 87 | adantlr 714 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1)) β
β) |
89 | 88 | exp0d 14052 |
. . . . . . . . . . . 12
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β (if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1))β0) = 1) |
90 | 61, 89 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β (if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1))β(π₯ pCnt π)) = 1) |
91 | 90 | ifeq1da 4522 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β if(π₯ β β, (if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1))β(π₯ pCnt π)), 1) = if(π₯ β β, 1, 1)) |
92 | | ifid 4531 |
. . . . . . . . . 10
β’ if(π₯ β β, 1, 1) =
1 |
93 | 91, 92 | eqtrdi 2793 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β if(π₯ β β, (if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1))β(π₯ pCnt π)), 1) = 1) |
94 | 38, 93 | eqtrd 2777 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β (πΉβπ₯) = 1) |
95 | 30, 34, 94 | seqid3 13959 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)β(π β 1)) =
1) |
96 | 95 | oveq1d 7377 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β ((seq1(
Β· , πΉ)β(π β 1)) Β· (πΉβπ)) = (1 Β· (πΉβπ))) |
97 | 1 | adantl 483 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ π β β) β π β
β€) |
98 | 2 | lgsfcl 26669 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β πΉ:ββΆβ€) |
99 | 67, 97, 7, 98 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β) β πΉ:ββΆβ€) |
100 | 99, 6 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β (πΉβπ) β β€) |
101 | 100 | zcnd 12615 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β (πΉβπ) β β) |
102 | 101 | mulid2d 11180 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β (1
Β· (πΉβπ)) = (πΉβπ)) |
103 | 28, 96, 102 | 3eqtrd 2781 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)βπ) = (πΉβπ)) |
104 | 20, 103 | eqtrd 2777 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)β(absβπ)) = (πΉβπ)) |
105 | 18, 104 | oveq12d 7380 |
. . 3
β’ ((π΄ β β€ β§ π β β) β
(if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1(
Β· , πΉ)β(absβπ))) = (1 Β· (πΉβπ))) |
106 | 2 | lgsfval 26666 |
. . . . 5
β’ (π β β β (πΉβπ) = if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) |
107 | 6, 106 | syl 17 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β (πΉβπ) = if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) |
108 | | iftrue 4497 |
. . . . 5
β’ (π β β β if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1) = (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π))) |
109 | 108 | adantl 483 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1) = (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π))) |
110 | 6 | nncnd 12176 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β) β π β
β) |
111 | 110 | exp1d 14053 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β (πβ1) = π) |
112 | 111 | oveq2d 7378 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β (π pCnt (πβ1)) = (π pCnt π)) |
113 | | simpr 486 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β π β
β) |
114 | | pcid 16752 |
. . . . . . . 8
β’ ((π β β β§ 1 β
β€) β (π pCnt
(πβ1)) =
1) |
115 | 113, 21, 114 | sylancl 587 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β (π pCnt (πβ1)) = 1) |
116 | 112, 115 | eqtr3d 2779 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β (π pCnt π) = 1) |
117 | 116 | oveq2d 7378 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β
(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))β1)) |
118 | | eqeq1 2741 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ = 2 β π = 2)) |
119 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π₯ β 1) = (π β 1)) |
120 | 119 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((π₯ β 1) / 2) = ((π β 1) / 2)) |
121 | 120 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π΄β((π₯ β 1) / 2)) = (π΄β((π β 1) / 2))) |
122 | 121 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π₯ = π β ((π΄β((π₯ β 1) / 2)) + 1) = ((π΄β((π β 1) / 2)) + 1)) |
123 | | id 22 |
. . . . . . . . . . 11
β’ (π₯ = π β π₯ = π) |
124 | 122, 123 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π₯ = π β (((π΄β((π₯ β 1) / 2)) + 1) mod π₯) = (((π΄β((π β 1) / 2)) + 1) mod π)) |
125 | 124 | oveq1d 7377 |
. . . . . . . . 9
β’ (π₯ = π β ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1) = ((((π΄β((π β 1) / 2)) + 1) mod π) β 1)) |
126 | 118, 125 | ifbieq2d 4517 |
. . . . . . . 8
β’ (π₯ = π β 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))) |
127 | 126 | eleq1d 2823 |
. . . . . . 7
β’ (π₯ = π β (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)) β
β)) |
128 | 87 | ralrimiva 3144 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β
βπ₯ β β
if(π₯ = 2, if(2 β₯
π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1)) β
β) |
129 | 127, 128,
113 | rspcdva 3585 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1)) β
β) |
130 | 129 | exp1d 14053 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β
(if(π = 2, if(2 β₯
π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β1) = if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))) |
131 | 117, 130 | eqtrd 2777 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β
(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))) |
132 | 107, 109,
131 | 3eqtrd 2781 |
. . 3
β’ ((π΄ β β€ β§ π β β) β (πΉβπ) = if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))) |
133 | 105, 102,
132 | 3eqtrd 2781 |
. 2
β’ ((π΄ β β€ β§ π β β) β
(if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1(
Β· , πΉ)β(absβπ))) = if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))) |
134 | 4, 9, 133 | 3eqtrd 2781 |
1
β’ ((π΄ β β€ β§ π β β) β (π΄ /L π) = if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))) |