Metamath Proof Explorer

Theorem lgsval2lem

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

Ref Expression
Hypothesis lgsval.1 
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )
Assertion lgsval2lem 
|- ( ( A e. ZZ /\ N e. Prime ) -> ( A /L N ) = if ( N = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( N - 1 ) / 2 ) ) + 1 ) mod N ) - 1 ) ) )

Proof

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