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 ffvelcdmd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℤ )
101 100 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
102 101 mullidd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ ) → ( 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 ) ) )