Step | Hyp | Ref
| Expression |
1 | | prmz 12113 |
. . 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 14490 |
. . 3
β’ ((π΄ β β€ β§ π β β€) β (π΄ /L π) = if(π = 0, if((π΄β2) = 1, 1, 0), (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
πΉ)β(absβπ))))) |
4 | 1, 3 | sylan2 286 |
. 2
β’ ((π΄ β β€ β§ π β β) β (π΄ /L π) = if(π = 0, if((π΄β2) = 1, 1, 0), (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
πΉ)β(absβπ))))) |
5 | | prmnn 12112 |
. . . . . 6
β’ (π β β β π β
β) |
6 | 5 | adantl 277 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β π β
β) |
7 | 6 | nnne0d 8966 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β π β 0) |
8 | 7 | neneqd 2368 |
. . 3
β’ ((π΄ β β€ β§ π β β) β Β¬
π = 0) |
9 | 8 | iffalsed 3546 |
. 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 9231 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β π β
β0) |
11 | 10 | nn0ge0d 9234 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β 0 β€
π) |
12 | | 0re 7959 |
. . . . . . . 8
β’ 0 β
β |
13 | 6 | nnred 8934 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β π β
β) |
14 | | lenlt 8035 |
. . . . . . . 8
β’ ((0
β β β§ π
β β) β (0 β€ π β Β¬ π < 0)) |
15 | 12, 13, 14 | sylancr 414 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β (0 β€
π β Β¬ π < 0)) |
16 | 11, 15 | mpbid 147 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β Β¬
π < 0) |
17 | 16 | intnanrd 932 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β Β¬
(π < 0 β§ π΄ < 0)) |
18 | 17 | iffalsed 3546 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β
if((π < 0 β§ π΄ < 0), -1, 1) =
1) |
19 | 13, 11 | absidd 11178 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β
(absβπ) = π) |
20 | 19 | fveq2d 5521 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)β(absβπ)) = (seq1( Β· , πΉ)βπ)) |
21 | | 1zzd 9282 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β 1 β
β€) |
22 | | prmuz2 12133 |
. . . . . . . . 9
β’ (π β β β π β
(β€β₯β2)) |
23 | 22 | adantl 277 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β π β
(β€β₯β2)) |
24 | | df-2 8980 |
. . . . . . . . 9
β’ 2 = (1 +
1) |
25 | 24 | fveq2i 5520 |
. . . . . . . 8
β’
(β€β₯β2) = (β€β₯β(1 +
1)) |
26 | 23, 25 | eleqtrdi 2270 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β π β
(β€β₯β(1 + 1))) |
27 | | simpll 527 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β) β§ π β
(β€β₯β1)) β π΄ β β€) |
28 | 1 | ad2antlr 489 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β) β§ π β
(β€β₯β1)) β π β β€) |
29 | 7 | adantr 276 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β) β§ π β
(β€β₯β1)) β π β 0) |
30 | 2 | lgsfcl 14494 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β πΉ:ββΆβ€) |
31 | 27, 28, 29, 30 | syl3anc 1238 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β) β§ π β
(β€β₯β1)) β πΉ:ββΆβ€) |
32 | | elnnuz 9566 |
. . . . . . . . . 10
β’ (π β β β π β
(β€β₯β1)) |
33 | 32 | biimpri 133 |
. . . . . . . . 9
β’ (π β
(β€β₯β1) β π β β) |
34 | 33 | adantl 277 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β) β§ π β
(β€β₯β1)) β π β β) |
35 | 31, 34 | ffvelcdmd 5654 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β) β§ π β
(β€β₯β1)) β (πΉβπ) β β€) |
36 | | zmulcl 9308 |
. . . . . . . 8
β’ ((π β β€ β§ π£ β β€) β (π Β· π£) β β€) |
37 | 36 | adantl 277 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β) β§ (π β β€ β§ π£ β β€)) β (π Β· π£) β β€) |
38 | 21, 26, 35, 37 | seq3m1 10470 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)βπ) = ((seq1( Β· , πΉ)β(π β 1)) Β· (πΉβπ))) |
39 | | 1t1e1 9073 |
. . . . . . . . 9
β’ (1
Β· 1) = 1 |
40 | 39 | a1i 9 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β (1
Β· 1) = 1) |
41 | | uz2m1nn 9607 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β (π β 1) β β) |
42 | 23, 41 | syl 14 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β) β (π β 1) β
β) |
43 | | nnuz 9565 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
44 | 42, 43 | eleqtrdi 2270 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β (π β 1) β
(β€β₯β1)) |
45 | | simpll 527 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β π΄ β β€) |
46 | 6 | adantr 276 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β π β β) |
47 | | elfznn 10056 |
. . . . . . . . . . 11
β’ (π₯ β (1...(π β 1)) β π₯ β β) |
48 | 47 | adantl 277 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β π₯ β β) |
49 | 2 | lgsfvalg 14491 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ π β β β§ π₯ β β) β (πΉβπ₯) = if(π₯ β β, (if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1))β(π₯ pCnt π)), 1)) |
50 | 45, 46, 48, 49 | syl3anc 1238 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β (πΉβπ₯) = if(π₯ β β, (if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1))β(π₯ pCnt π)), 1)) |
51 | | elfzelz 10027 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...(π β 1)) β π β β€) |
52 | 51 | zred 9377 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...(π β 1)) β π β β) |
53 | 52 | ltm1d 8891 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...(π β 1)) β (π β 1) < π) |
54 | | peano2rem 8226 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (π β 1) β
β) |
55 | 52, 54 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...(π β 1)) β (π β 1) β β) |
56 | | elfzle2 10030 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...(π β 1)) β π β€ (π β 1)) |
57 | 52, 55, 56 | lensymd 8081 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...(π β 1)) β Β¬ (π β 1) < π) |
58 | 53, 57 | pm2.65i 639 |
. . . . . . . . . . . . . . . . 17
β’ Β¬
π β (1...(π β 1)) |
59 | | eleq1 2240 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (π₯ β (1...(π β 1)) β π β (1...(π β 1)))) |
60 | 58, 59 | mtbiri 675 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β Β¬ π₯ β (1...(π β 1))) |
61 | 60 | con2i 627 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (1...(π β 1)) β Β¬ π₯ = π) |
62 | 61 | ad2antlr 489 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β Β¬ π₯ = π) |
63 | | prmuz2 12133 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β π₯ β
(β€β₯β2)) |
64 | | simpllr 534 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β π β β) |
65 | | dvdsprm 12139 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β
(β€β₯β2) β§ π β β) β (π₯ β₯ π β π₯ = π)) |
66 | 63, 64, 65 | syl2an2 594 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β (π₯ β₯ π β π₯ = π)) |
67 | 62, 66 | mtbird 673 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β Β¬ π₯ β₯ π) |
68 | | simpr 110 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β π₯ β β) |
69 | 6 | ad2antrr 488 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β π β β) |
70 | | pceq0 12323 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π β β) β ((π₯ pCnt π) = 0 β Β¬ π₯ β₯ π)) |
71 | 68, 69, 70 | syl2anc 411 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β ((π₯ pCnt π) = 0 β Β¬ π₯ β₯ π)) |
72 | 67, 71 | mpbird 167 |
. . . . . . . . . . . 12
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β (π₯ pCnt π) = 0) |
73 | 72 | oveq2d 5893 |
. . . . . . . . . . 11
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (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)) |
74 | | 0zd 9267 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β€ β 0 β
β€) |
75 | | 1zzd 9282 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β€ β 1 β
β€) |
76 | | neg1z 9287 |
. . . . . . . . . . . . . . . . . . 19
β’ -1 β
β€ |
77 | 76 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β€ β -1 β
β€) |
78 | | id 19 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π΄ β β€ β π΄ β
β€) |
79 | | 8nn 9088 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 8 β
β |
80 | 79 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π΄ β β€ β 8 β
β) |
81 | 78, 80 | zmodcld 10347 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄ β β€ β (π΄ mod 8) β
β0) |
82 | 81 | nn0zd 9375 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄ β β€ β (π΄ mod 8) β
β€) |
83 | | zdceq 9330 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄ mod 8) β β€ β§ 1
β β€) β DECID (π΄ mod 8) = 1) |
84 | 82, 75, 83 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β β€ β
DECID (π΄ mod
8) = 1) |
85 | | 7nn 9087 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 7 β
β |
86 | 85 | nnzi 9276 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 7 β
β€ |
87 | | zdceq 9330 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄ mod 8) β β€ β§ 7
β β€) β DECID (π΄ mod 8) = 7) |
88 | 82, 86, 87 | sylancl 413 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β β€ β
DECID (π΄ mod
8) = 7) |
89 | | dcor 935 |
. . . . . . . . . . . . . . . . . . . 20
β’
(DECID (π΄ mod 8) = 1 β (DECID
(π΄ mod 8) = 7 β
DECID ((π΄
mod 8) = 1 β¨ (π΄ mod 8) =
7))) |
90 | 84, 88, 89 | sylc 62 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β€ β
DECID ((π΄
mod 8) = 1 β¨ (π΄ mod 8) =
7)) |
91 | | elprg 3614 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ mod 8) β
β0 β ((π΄ mod 8) β {1, 7} β ((π΄ mod 8) = 1 β¨ (π΄ mod 8) = 7))) |
92 | 81, 91 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β β€ β ((π΄ mod 8) β {1, 7} β
((π΄ mod 8) = 1 β¨ (π΄ mod 8) = 7))) |
93 | 92 | dcbid 838 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β β€ β
(DECID (π΄
mod 8) β {1, 7} β DECID ((π΄ mod 8) = 1 β¨ (π΄ mod 8) = 7))) |
94 | 90, 93 | mpbird 167 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β€ β
DECID (π΄ mod
8) β {1, 7}) |
95 | 75, 77, 94 | ifcldcd 3572 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β€ β if((π΄ mod 8) β {1, 7}, 1, -1)
β β€) |
96 | | 2nn 9082 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
β |
97 | | dvdsdc 11807 |
. . . . . . . . . . . . . . . . . 18
β’ ((2
β β β§ π΄
β β€) β DECID 2 β₯ π΄) |
98 | 96, 97 | mpan 424 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β€ β
DECID 2 β₯ π΄) |
99 | 74, 95, 98 | ifcldcd 3572 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β€ β if(2
β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1))
β β€) |
100 | 99 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ π₯ = 2) β if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)) β
β€) |
101 | | simpl 109 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ β β€ β§ π β β) β π΄ β
β€) |
102 | 101 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β π΄ β
β€) |
103 | | simplr 528 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β π₯ β
β) |
104 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β Β¬ π₯ = 2) |
105 | 104 | neqned 2354 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β π₯ β 2) |
106 | | eldifsn 3721 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ β (β β {2})
β (π₯ β β
β§ π₯ β
2)) |
107 | 103, 105,
106 | sylanbrc 417 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β π₯ β (β β
{2})) |
108 | | oddprm 12261 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (β β {2})
β ((π₯ β 1) / 2)
β β) |
109 | 107, 108 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β ((π₯ β 1) / 2) β
β) |
110 | 109 | nnnn0d 9231 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β ((π₯ β 1) / 2) β
β0) |
111 | | zexpcl 10537 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β β€ β§ ((π₯ β 1) / 2) β
β0) β (π΄β((π₯ β 1) / 2)) β
β€) |
112 | 102, 110,
111 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β (π΄β((π₯ β 1) / 2)) β
β€) |
113 | 112 | peano2zd 9380 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β ((π΄β((π₯ β 1) / 2)) + 1) β
β€) |
114 | | prmnn 12112 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β π₯ β
β) |
115 | 114 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β π₯ β
β) |
116 | 113, 115 | zmodcld 10347 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β (((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β
β0) |
117 | 116 | nn0zd 9375 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β (((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β β€) |
118 | | peano2zm 9293 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β β€ β ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1) β β€) |
119 | 117, 118 | syl 14 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β β) β§ Β¬
π₯ = 2) β ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1) β β€) |
120 | | prmz 12113 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β π₯ β
β€) |
121 | | 2z 9283 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β€ |
122 | 121 | a1i 9 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β€ β§ π β β) β§ π₯ β β) β 2 β
β€) |
123 | | zdceq 9330 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β€ β§ 2 β
β€) β DECID π₯ = 2) |
124 | 120, 122,
123 | syl2an2 594 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β€ β§ π β β) β§ π₯ β β) β
DECID π₯ =
2) |
125 | 100, 119,
124 | ifcldadc 3565 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β€ β§ π β β) β§ π₯ β β) β if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1)) β
β€) |
126 | 125 | zcnd 9378 |
. . . . . . . . . . . . 13
β’ (((π΄ β β€ β§ π β β) β§ π₯ β β) β if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1)) β
β) |
127 | 126 | adantlr 477 |
. . . . . . . . . . . 12
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1)) β
β) |
128 | 127 | exp0d 10650 |
. . . . . . . . . . 11
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β (if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1))β0) = 1) |
129 | 73, 128 | eqtrd 2210 |
. . . . . . . . . 10
β’ ((((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β§ π₯ β β) β (if(π₯ = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1))β(π₯ pCnt π)) = 1) |
130 | | prmdc 12132 |
. . . . . . . . . . 11
β’ (π₯ β β β
DECID π₯
β β) |
131 | 48, 130 | syl 14 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β DECID
π₯ β
β) |
132 | 129, 131 | ifeq1dadc 3566 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (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)) |
133 | | ifiddc 3570 |
. . . . . . . . . 10
β’
(DECID π₯ β β β if(π₯ β β, 1, 1) = 1) |
134 | 131, 133 | syl 14 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β if(π₯ β β, 1, 1) = 1) |
135 | 50, 132, 134 | 3eqtrd 2214 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β) β§ π₯ β (1...(π β 1))) β (πΉβπ₯) = 1) |
136 | | simpll 527 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β) β§ π₯ β
(β€β₯β1)) β π΄ β β€) |
137 | 1 | ad2antlr 489 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β) β§ π₯ β
(β€β₯β1)) β π β β€) |
138 | 7 | adantr 276 |
. . . . . . . . . 10
β’ (((π΄ β β€ β§ π β β) β§ π₯ β
(β€β₯β1)) β π β 0) |
139 | 136, 137,
138, 30 | syl3anc 1238 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β) β§ π₯ β
(β€β₯β1)) β πΉ:ββΆβ€) |
140 | | elnnuz 9566 |
. . . . . . . . . . 11
β’ (π₯ β β β π₯ β
(β€β₯β1)) |
141 | 140 | biimpri 133 |
. . . . . . . . . 10
β’ (π₯ β
(β€β₯β1) β π₯ β β) |
142 | 141 | adantl 277 |
. . . . . . . . 9
β’ (((π΄ β β€ β§ π β β) β§ π₯ β
(β€β₯β1)) β π₯ β β) |
143 | 139, 142 | ffvelcdmd 5654 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β) β§ π₯ β
(β€β₯β1)) β (πΉβπ₯) β β€) |
144 | | zmulcl 9308 |
. . . . . . . . 9
β’ ((π₯ β β€ β§ π¦ β β€) β (π₯ Β· π¦) β β€) |
145 | 144 | adantl 277 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β) β§ (π₯ β β€ β§ π¦ β β€)) β (π₯ Β· π¦) β β€) |
146 | 40, 44, 135, 21, 143, 145 | seq3id3 10509 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)β(π β 1)) =
1) |
147 | 146 | oveq1d 5892 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β ((seq1(
Β· , πΉ)β(π β 1)) Β· (πΉβπ)) = (1 Β· (πΉβπ))) |
148 | 1 | adantl 277 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ π β β) β π β
β€) |
149 | 101, 148,
7, 30 | syl3anc 1238 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β) β πΉ:ββΆβ€) |
150 | 149, 6 | ffvelcdmd 5654 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β (πΉβπ) β β€) |
151 | 150 | zcnd 9378 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β (πΉβπ) β β) |
152 | 151 | mulid2d 7978 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β (1
Β· (πΉβπ)) = (πΉβπ)) |
153 | 38, 147, 152 | 3eqtrd 2214 |
. . . . 5
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)βπ) = (πΉβπ)) |
154 | 20, 153 | eqtrd 2210 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β (seq1(
Β· , πΉ)β(absβπ)) = (πΉβπ)) |
155 | 18, 154 | oveq12d 5895 |
. . 3
β’ ((π΄ β β€ β§ π β β) β
(if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1(
Β· , πΉ)β(absβπ))) = (1 Β· (πΉβπ))) |
156 | 2 | lgsfvalg 14491 |
. . . . 5
β’ ((π΄ β β€ β§ π β β β§ π β β) β (πΉβπ) = if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) |
157 | 101, 6, 6, 156 | syl3anc 1238 |
. . . 4
β’ ((π΄ β β€ β§ π β β) β (πΉβπ) = if(π β β, (if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))β(π pCnt π)), 1)) |
158 | | iftrue 3541 |
. . . . 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 π))) |
159 | 158 | adantl 277 |
. . . 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 π))) |
160 | 6 | nncnd 8935 |
. . . . . . . . 9
β’ ((π΄ β β€ β§ π β β) β π β
β) |
161 | 160 | exp1d 10651 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β (πβ1) = π) |
162 | 161 | oveq2d 5893 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β (π pCnt (πβ1)) = (π pCnt π)) |
163 | | simpr 110 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β) β π β
β) |
164 | | 1z 9281 |
. . . . . . . 8
β’ 1 β
β€ |
165 | | pcid 12325 |
. . . . . . . 8
β’ ((π β β β§ 1 β
β€) β (π pCnt
(πβ1)) =
1) |
166 | 163, 164,
165 | sylancl 413 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β (π pCnt (πβ1)) = 1) |
167 | 162, 166 | eqtr3d 2212 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β (π pCnt π) = 1) |
168 | 167 | oveq2d 5893 |
. . . . 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)) |
169 | | eqeq1 2184 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ = 2 β π = 2)) |
170 | | oveq1 5884 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π₯ β 1) = (π β 1)) |
171 | 170 | oveq1d 5892 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((π₯ β 1) / 2) = ((π β 1) / 2)) |
172 | 171 | oveq2d 5893 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π΄β((π₯ β 1) / 2)) = (π΄β((π β 1) / 2))) |
173 | 172 | oveq1d 5892 |
. . . . . . . . . . 11
β’ (π₯ = π β ((π΄β((π₯ β 1) / 2)) + 1) = ((π΄β((π β 1) / 2)) + 1)) |
174 | | id 19 |
. . . . . . . . . . 11
β’ (π₯ = π β π₯ = π) |
175 | 173, 174 | oveq12d 5895 |
. . . . . . . . . 10
β’ (π₯ = π β (((π΄β((π₯ β 1) / 2)) + 1) mod π₯) = (((π΄β((π β 1) / 2)) + 1) mod π)) |
176 | 175 | oveq1d 5892 |
. . . . . . . . 9
β’ (π₯ = π β ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1) = ((((π΄β((π β 1) / 2)) + 1) mod π) β 1)) |
177 | 169, 176 | ifbieq2d 3560 |
. . . . . . . 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))) |
178 | 177 | eleq1d 2246 |
. . . . . . 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)) β
β)) |
179 | 126 | ralrimiva 2550 |
. . . . . . 7
β’ ((π΄ β β€ β§ π β β) β
βπ₯ β β
if(π₯ = 2, if(2 β₯
π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π₯ β 1) / 2)) + 1) mod π₯) β 1)) β
β) |
180 | 178, 179,
163 | rspcdva 2848 |
. . . . . 6
β’ ((π΄ β β€ β§ π β β) β if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1)) β
β) |
181 | 180 | exp1d 10651 |
. . . . 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))) |
182 | 168, 181 | eqtrd 2210 |
. . . 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))) |
183 | 157, 159,
182 | 3eqtrd 2214 |
. . 3
β’ ((π΄ β β€ β§ π β β) β (πΉβπ) = if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))) |
184 | 155, 152,
183 | 3eqtrd 2214 |
. 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))) |
185 | 4, 9, 184 | 3eqtrd 2214 |
1
β’ ((π΄ β β€ β§ π β β) β (π΄ /L π) = if(π = 2, if(2 β₯ π΄, 0, if((π΄ mod 8) β {1, 7}, 1, -1)), ((((π΄β((π β 1) / 2)) + 1) mod π) β 1))) |