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