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