Metamath Proof Explorer


Theorem lgsval2lem

Description: Lemma for lgsval2 . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis lgsval.1 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
Assertion lgsval2lem ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝐴 /L 𝑁 ) = if ( 𝑁 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) mod 𝑁 ) − 1 ) ) )

Proof

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 ) ) )