Step |
Hyp |
Ref |
Expression |
1 |
|
lgsval.1 |
⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) |
2 |
|
prmz |
⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℤ ) |
3 |
1
|
lgsval |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) = if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ) ) |
4 |
2 3
|
sylan2 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝐴 /L 𝑁 ) = if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ) ) |
5 |
|
prmnn |
⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℕ ) |
6 |
5
|
adantl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ℕ ) |
7 |
6
|
nnne0d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 𝑁 ≠ 0 ) |
8 |
7
|
neneqd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ¬ 𝑁 = 0 ) |
9 |
8
|
iffalsed |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → if ( 𝑁 = 0 , if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) , ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) ) |
10 |
6
|
nnnn0d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ℕ0 ) |
11 |
10
|
nn0ge0d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 0 ≤ 𝑁 ) |
12 |
|
0re |
⊢ 0 ∈ ℝ |
13 |
6
|
nnred |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ℝ ) |
14 |
|
lenlt |
⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 ≤ 𝑁 ↔ ¬ 𝑁 < 0 ) ) |
15 |
12 13 14
|
sylancr |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 0 ≤ 𝑁 ↔ ¬ 𝑁 < 0 ) ) |
16 |
11 15
|
mpbid |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ¬ 𝑁 < 0 ) |
17 |
16
|
intnanrd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ¬ ( 𝑁 < 0 ∧ 𝐴 < 0 ) ) |
18 |
17
|
iffalsed |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) = 1 ) |
19 |
13 11
|
absidd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( abs ‘ 𝑁 ) = 𝑁 ) |
20 |
19
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) |
21 |
|
1z |
⊢ 1 ∈ ℤ |
22 |
|
prmuz2 |
⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) |
23 |
22
|
adantl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) |
24 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
25 |
24
|
fveq2i |
⊢ ( ℤ≥ ‘ 2 ) = ( ℤ≥ ‘ ( 1 + 1 ) ) |
26 |
23 25
|
eleqtrdi |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) |
27 |
|
seqm1 |
⊢ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) = ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑁 − 1 ) ) · ( 𝐹 ‘ 𝑁 ) ) ) |
28 |
21 26 27
|
sylancr |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) = ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑁 − 1 ) ) · ( 𝐹 ‘ 𝑁 ) ) ) |
29 |
|
1t1e1 |
⊢ ( 1 · 1 ) = 1 |
30 |
29
|
a1i |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 1 · 1 ) = 1 ) |
31 |
|
uz2m1nn |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℕ ) |
32 |
23 31
|
syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝑁 − 1 ) ∈ ℕ ) |
33 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
34 |
32 33
|
eleqtrdi |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 1 ) ) |
35 |
|
elfznn |
⊢ ( 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑥 ∈ ℕ ) |
36 |
35
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑥 ∈ ℕ ) |
37 |
1
|
lgsfval |
⊢ ( 𝑥 ∈ ℕ → ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ℙ , ( if ( 𝑥 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) − 1 ) ) ↑ ( 𝑥 pCnt 𝑁 ) ) , 1 ) ) |
38 |
36 37
|
syl |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ℙ , ( if ( 𝑥 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) − 1 ) ) ↑ ( 𝑥 pCnt 𝑁 ) ) , 1 ) ) |
39 |
|
elfzelz |
⊢ ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑁 ∈ ℤ ) |
40 |
39
|
zred |
⊢ ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑁 ∈ ℝ ) |
41 |
40
|
ltm1d |
⊢ ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) < 𝑁 ) |
42 |
|
peano2rem |
⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ ) |
43 |
40 42
|
syl |
⊢ ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ℝ ) |
44 |
|
elfzle2 |
⊢ ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑁 ≤ ( 𝑁 − 1 ) ) |
45 |
40 43 44
|
lensymd |
⊢ ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ¬ ( 𝑁 − 1 ) < 𝑁 ) |
46 |
41 45
|
pm2.65i |
⊢ ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) |
47 |
|
eleq1 |
⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) |
48 |
46 47
|
mtbiri |
⊢ ( 𝑥 = 𝑁 → ¬ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) |
49 |
48
|
con2i |
⊢ ( 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ¬ 𝑥 = 𝑁 ) |
50 |
49
|
ad2antlr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 ∈ ℙ ) → ¬ 𝑥 = 𝑁 ) |
51 |
|
prmuz2 |
⊢ ( 𝑥 ∈ ℙ → 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) |
52 |
|
simpllr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 ∈ ℙ ) → 𝑁 ∈ ℙ ) |
53 |
|
dvdsprm |
⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℙ ) → ( 𝑥 ∥ 𝑁 ↔ 𝑥 = 𝑁 ) ) |
54 |
51 52 53
|
syl2an2 |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 ∈ ℙ ) → ( 𝑥 ∥ 𝑁 ↔ 𝑥 = 𝑁 ) ) |
55 |
50 54
|
mtbird |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 ∈ ℙ ) → ¬ 𝑥 ∥ 𝑁 ) |
56 |
|
simpr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 ∈ ℙ ) → 𝑥 ∈ ℙ ) |
57 |
6
|
ad2antrr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 ∈ ℙ ) → 𝑁 ∈ ℕ ) |
58 |
|
pceq0 |
⊢ ( ( 𝑥 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑥 pCnt 𝑁 ) = 0 ↔ ¬ 𝑥 ∥ 𝑁 ) ) |
59 |
56 57 58
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 ∈ ℙ ) → ( ( 𝑥 pCnt 𝑁 ) = 0 ↔ ¬ 𝑥 ∥ 𝑁 ) ) |
60 |
55 59
|
mpbird |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 ∈ ℙ ) → ( 𝑥 pCnt 𝑁 ) = 0 ) |
61 |
60
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 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 |
⊢ 0 ∈ ℤ |
63 |
|
neg1z |
⊢ - 1 ∈ ℤ |
64 |
21 63
|
ifcli |
⊢ if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ∈ ℤ |
65 |
62 64
|
ifcli |
⊢ if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) ∈ ℤ |
66 |
65
|
a1i |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ 𝑥 = 2 ) → if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) ∈ ℤ ) |
67 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 𝐴 ∈ ℤ ) |
68 |
67
|
ad2antrr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → 𝐴 ∈ ℤ ) |
69 |
|
simplr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → 𝑥 ∈ ℙ ) |
70 |
|
simpr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → ¬ 𝑥 = 2 ) |
71 |
70
|
neqned |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → 𝑥 ≠ 2 ) |
72 |
|
eldifsn |
⊢ ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑥 ∈ ℙ ∧ 𝑥 ≠ 2 ) ) |
73 |
69 71 72
|
sylanbrc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → 𝑥 ∈ ( ℙ ∖ { 2 } ) ) |
74 |
|
oddprm |
⊢ ( 𝑥 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑥 − 1 ) / 2 ) ∈ ℕ ) |
75 |
73 74
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → ( ( 𝑥 − 1 ) / 2 ) ∈ ℕ ) |
76 |
75
|
nnnn0d |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → ( ( 𝑥 − 1 ) / 2 ) ∈ ℕ0 ) |
77 |
|
zexpcl |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝑥 − 1 ) / 2 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) ∈ ℤ ) |
78 |
68 76 77
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) ∈ ℤ ) |
79 |
78
|
peano2zd |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) ∈ ℤ ) |
80 |
|
prmnn |
⊢ ( 𝑥 ∈ ℙ → 𝑥 ∈ ℕ ) |
81 |
80
|
ad2antlr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → 𝑥 ∈ ℕ ) |
82 |
79 81
|
zmodcld |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) ∈ ℕ0 ) |
83 |
82
|
nn0zd |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) ∈ ℤ ) |
84 |
|
peano2zm |
⊢ ( ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) ∈ ℤ → ( ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) − 1 ) ∈ ℤ ) |
85 |
83 84
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) ∧ ¬ 𝑥 = 2 ) → ( ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) − 1 ) ∈ ℤ ) |
86 |
66 85
|
ifclda |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) → if ( 𝑥 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) − 1 ) ) ∈ ℤ ) |
87 |
86
|
zcnd |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ℙ ) → if ( 𝑥 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) − 1 ) ) ∈ ℂ ) |
88 |
87
|
adantlr |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 ∈ ℙ ) → if ( 𝑥 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) − 1 ) ) ∈ ℂ ) |
89 |
88
|
exp0d |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 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 |
⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 ∈ ℙ ) → ( if ( 𝑥 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) − 1 ) ) ↑ ( 𝑥 pCnt 𝑁 ) ) = 1 ) |
91 |
90
|
ifeq1da |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 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 |
⊢ if ( 𝑥 ∈ ℙ , 1 , 1 ) = 1 |
93 |
91 92
|
eqtrdi |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 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 |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 𝑥 ) = 1 ) |
95 |
30 34 94
|
seqid3 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑁 − 1 ) ) = 1 ) |
96 |
95
|
oveq1d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑁 − 1 ) ) · ( 𝐹 ‘ 𝑁 ) ) = ( 1 · ( 𝐹 ‘ 𝑁 ) ) ) |
97 |
2
|
adantl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ℤ ) |
98 |
1
|
lgsfcl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → 𝐹 : ℕ ⟶ ℤ ) |
99 |
67 97 7 98
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 𝐹 : ℕ ⟶ ℤ ) |
100 |
99 6
|
ffvelrnd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℤ ) |
101 |
100
|
zcnd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℂ ) |
102 |
101
|
mulid2d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 1 · ( 𝐹 ‘ 𝑁 ) ) = ( 𝐹 ‘ 𝑁 ) ) |
103 |
28 96 102
|
3eqtrd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) = ( 𝐹 ‘ 𝑁 ) ) |
104 |
20 103
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) = ( 𝐹 ‘ 𝑁 ) ) |
105 |
18 104
|
oveq12d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) = ( 1 · ( 𝐹 ‘ 𝑁 ) ) ) |
106 |
1
|
lgsfval |
⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) = if ( 𝑁 ∈ ℙ , ( if ( 𝑁 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) mod 𝑁 ) − 1 ) ) ↑ ( 𝑁 pCnt 𝑁 ) ) , 1 ) ) |
107 |
6 106
|
syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝐹 ‘ 𝑁 ) = if ( 𝑁 ∈ ℙ , ( if ( 𝑁 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) mod 𝑁 ) − 1 ) ) ↑ ( 𝑁 pCnt 𝑁 ) ) , 1 ) ) |
108 |
|
iftrue |
⊢ ( 𝑁 ∈ ℙ → 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 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 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 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ℂ ) |
111 |
110
|
exp1d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝑁 ↑ 1 ) = 𝑁 ) |
112 |
111
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝑁 pCnt ( 𝑁 ↑ 1 ) ) = ( 𝑁 pCnt 𝑁 ) ) |
113 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ℙ ) |
114 |
|
pcid |
⊢ ( ( 𝑁 ∈ ℙ ∧ 1 ∈ ℤ ) → ( 𝑁 pCnt ( 𝑁 ↑ 1 ) ) = 1 ) |
115 |
113 21 114
|
sylancl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝑁 pCnt ( 𝑁 ↑ 1 ) ) = 1 ) |
116 |
112 115
|
eqtr3d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝑁 pCnt 𝑁 ) = 1 ) |
117 |
116
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 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 |
⊢ ( 𝑥 = 𝑁 → ( 𝑥 = 2 ↔ 𝑁 = 2 ) ) |
119 |
|
oveq1 |
⊢ ( 𝑥 = 𝑁 → ( 𝑥 − 1 ) = ( 𝑁 − 1 ) ) |
120 |
119
|
oveq1d |
⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 − 1 ) / 2 ) = ( ( 𝑁 − 1 ) / 2 ) ) |
121 |
120
|
oveq2d |
⊢ ( 𝑥 = 𝑁 → ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) = ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 2 ) ) ) |
122 |
121
|
oveq1d |
⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) = ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) |
123 |
|
id |
⊢ ( 𝑥 = 𝑁 → 𝑥 = 𝑁 ) |
124 |
122 123
|
oveq12d |
⊢ ( 𝑥 = 𝑁 → ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) = ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) mod 𝑁 ) ) |
125 |
124
|
oveq1d |
⊢ ( 𝑥 = 𝑁 → ( ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) − 1 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) mod 𝑁 ) − 1 ) ) |
126 |
118 125
|
ifbieq2d |
⊢ ( 𝑥 = 𝑁 → 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 |
⊢ ( 𝑥 = 𝑁 → ( 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 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ∀ 𝑥 ∈ ℙ if ( 𝑥 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑥 − 1 ) / 2 ) ) + 1 ) mod 𝑥 ) − 1 ) ) ∈ ℂ ) |
129 |
127 128 113
|
rspcdva |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → if ( 𝑁 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) mod 𝑁 ) − 1 ) ) ∈ ℂ ) |
130 |
129
|
exp1d |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 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 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 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 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝐹 ‘ 𝑁 ) = if ( 𝑁 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) mod 𝑁 ) − 1 ) ) ) |
133 |
105 102 132
|
3eqtrd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · ( seq 1 ( · , 𝐹 ) ‘ ( abs ‘ 𝑁 ) ) ) = if ( 𝑁 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) mod 𝑁 ) − 1 ) ) ) |
134 |
4 9 133
|
3eqtrd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝐴 /L 𝑁 ) = if ( 𝑁 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) mod 𝑁 ) − 1 ) ) ) |