Metamath Proof Explorer

Theorem lgscllem

Description: The Legendre symbol is an element of Z . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypotheses 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 ) )
lgsfcl2.z 
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }
Assertion lgscllem 
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. Z )

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