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 |
|
lgsfcl2.z |
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 } |
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
|
lgslem2 |
|- ( -u 1 e. Z /\ 0 e. Z /\ 1 e. Z ) |
5 |
4
|
simp3i |
|- 1 e. Z |
6 |
4
|
simp2i |
|- 0 e. Z |
7 |
5 6
|
ifcli |
|- if ( ( A ^ 2 ) = 1 , 1 , 0 ) e. Z |
8 |
7
|
a1i |
|- ( ( ( A e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> if ( ( A ^ 2 ) = 1 , 1 , 0 ) e. Z ) |
9 |
4
|
simp1i |
|- -u 1 e. Z |
10 |
9 5
|
ifcli |
|- if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) e. Z |
11 |
|
simplr |
|- ( ( ( A e. ZZ /\ N e. ZZ ) /\ -. N = 0 ) -> N e. ZZ ) |
12 |
|
simpr |
|- ( ( ( A e. ZZ /\ N e. ZZ ) /\ -. N = 0 ) -> -. N = 0 ) |
13 |
12
|
neqned |
|- ( ( ( A e. ZZ /\ N e. ZZ ) /\ -. N = 0 ) -> N =/= 0 ) |
14 |
|
nnabscl |
|- ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN ) |
15 |
11 13 14
|
syl2anc |
|- ( ( ( A e. ZZ /\ N e. ZZ ) /\ -. N = 0 ) -> ( abs ` N ) e. NN ) |
16 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
17 |
15 16
|
eleqtrdi |
|- ( ( ( A e. ZZ /\ N e. ZZ ) /\ -. N = 0 ) -> ( abs ` N ) e. ( ZZ>= ` 1 ) ) |
18 |
|
df-ne |
|- ( N =/= 0 <-> -. N = 0 ) |
19 |
1 2
|
lgsfcl2 |
|- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F : NN --> Z ) |
20 |
19
|
3expa |
|- ( ( ( A e. ZZ /\ N e. ZZ ) /\ N =/= 0 ) -> F : NN --> Z ) |
21 |
18 20
|
sylan2br |
|- ( ( ( A e. ZZ /\ N e. ZZ ) /\ -. N = 0 ) -> F : NN --> Z ) |
22 |
|
elfznn |
|- ( y e. ( 1 ... ( abs ` N ) ) -> y e. NN ) |
23 |
|
ffvelrn |
|- ( ( F : NN --> Z /\ y e. NN ) -> ( F ` y ) e. Z ) |
24 |
21 22 23
|
syl2an |
|- ( ( ( ( A e. ZZ /\ N e. ZZ ) /\ -. N = 0 ) /\ y e. ( 1 ... ( abs ` N ) ) ) -> ( F ` y ) e. Z ) |
25 |
2
|
lgslem3 |
|- ( ( y e. Z /\ z e. Z ) -> ( y x. z ) e. Z ) |
26 |
25
|
adantl |
|- ( ( ( ( A e. ZZ /\ N e. ZZ ) /\ -. N = 0 ) /\ ( y e. Z /\ z e. Z ) ) -> ( y x. z ) e. Z ) |
27 |
17 24 26
|
seqcl |
|- ( ( ( A e. ZZ /\ N e. ZZ ) /\ -. N = 0 ) -> ( seq 1 ( x. , F ) ` ( abs ` N ) ) e. Z ) |
28 |
2
|
lgslem3 |
|- ( ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) e. Z /\ ( seq 1 ( x. , F ) ` ( abs ` N ) ) e. Z ) -> ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , F ) ` ( abs ` N ) ) ) e. Z ) |
29 |
10 27 28
|
sylancr |
|- ( ( ( A e. ZZ /\ N e. ZZ ) /\ -. N = 0 ) -> ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , F ) ` ( abs ` N ) ) ) e. Z ) |
30 |
8 29
|
ifclda |
|- ( ( A e. ZZ /\ N e. ZZ ) -> if ( N = 0 , if ( ( A ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , F ) ` ( abs ` N ) ) ) ) e. Z ) |
31 |
3 30
|
eqeltrd |
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. Z ) |