Metamath Proof Explorer

Theorem lgsmod

Description: The Legendre (Jacobi) symbol is preserved under reduction mod n when n is odd. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsmod 
|- ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( ( A mod N ) /L N ) = ( A /L N ) )

Proof

Step Hyp Ref Expression
1 zmodcl 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( A mod N ) e. NN0 )
2 1 3adant3 
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( A mod N ) e. NN0 )
3 2 nn0zd 
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( A mod N ) e. ZZ )
4 3 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( A mod N ) e. ZZ )
5 simpr 
 |-  ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) -> n e. Prime )
6 5 adantr 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> n e. Prime )
7 simpl3 
 |-  ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) -> -. 2 || N )
8 breq1 
 |-  ( n = 2 -> ( n || N <-> 2 || N ) )
9 8 notbid 
 |-  ( n = 2 -> ( -. n || N <-> -. 2 || N ) )
10 7 9 syl5ibrcom 
 |-  ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) -> ( n = 2 -> -. n || N ) )
11 10 necon2ad 
 |-  ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) -> ( n || N -> n =/= 2 ) )
12 11 imp 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> n =/= 2 )
13 eldifsn 
 |-  ( n e. ( Prime \ { 2 } ) <-> ( n e. Prime /\ n =/= 2 ) )
14 6 12 13 sylanbrc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> n e. ( Prime \ { 2 } ) )
15 oddprm 
 |-  ( n e. ( Prime \ { 2 } ) -> ( ( n - 1 ) / 2 ) e. NN )
16 14 15 syl 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( n - 1 ) / 2 ) e. NN )
17 16 nnnn0d 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( n - 1 ) / 2 ) e. NN0 )
18 zexpcl 
 |-  ( ( ( A mod N ) e. ZZ /\ ( ( n - 1 ) / 2 ) e. NN0 ) -> ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) e. ZZ )
19 4 17 18 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) e. ZZ )
20 19 zred 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) e. RR )
21 simpll1 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> A e. ZZ )
22 zexpcl 
 |-  ( ( A e. ZZ /\ ( ( n - 1 ) / 2 ) e. NN0 ) -> ( A ^ ( ( n - 1 ) / 2 ) ) e. ZZ )
23 21 17 22 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( A ^ ( ( n - 1 ) / 2 ) ) e. ZZ )
24 23 zred 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( A ^ ( ( n - 1 ) / 2 ) ) e. RR )
25 1red 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> 1 e. RR )
26 prmnn 
 |-  ( n e. Prime -> n e. NN )
27 26 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> n e. NN )
28 27 nnrpd 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> n e. RR+ )
29 prmz 
 |-  ( n e. Prime -> n e. ZZ )
30 29 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> n e. ZZ )
31 simp2 
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> N e. NN )
32 31 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> N e. NN )
33 32 nnzd 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> N e. ZZ )
34 4 21 zsubcld 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( A mod N ) - A ) e. ZZ )
35 simpr 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> n || N )
36 21 zred 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> A e. RR )
37 32 nnrpd 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> N e. RR+ )
38 modabs2 
 |-  ( ( A e. RR /\ N e. RR+ ) -> ( ( A mod N ) mod N ) = ( A mod N ) )
39 36 37 38 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( A mod N ) mod N ) = ( A mod N ) )
40 moddvds 
 |-  ( ( N e. NN /\ ( A mod N ) e. ZZ /\ A e. ZZ ) -> ( ( ( A mod N ) mod N ) = ( A mod N ) <-> N || ( ( A mod N ) - A ) ) )
41 32 4 21 40 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( ( A mod N ) mod N ) = ( A mod N ) <-> N || ( ( A mod N ) - A ) ) )
42 39 41 mpbid 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> N || ( ( A mod N ) - A ) )
43 30 33 34 35 42 dvdstrd 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> n || ( ( A mod N ) - A ) )
44 moddvds 
 |-  ( ( n e. NN /\ ( A mod N ) e. ZZ /\ A e. ZZ ) -> ( ( ( A mod N ) mod n ) = ( A mod n ) <-> n || ( ( A mod N ) - A ) ) )
45 27 4 21 44 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( ( A mod N ) mod n ) = ( A mod n ) <-> n || ( ( A mod N ) - A ) ) )
46 43 45 mpbird 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( A mod N ) mod n ) = ( A mod n ) )
47 modexp 
 |-  ( ( ( ( A mod N ) e. ZZ /\ A e. ZZ ) /\ ( ( ( n - 1 ) / 2 ) e. NN0 /\ n e. RR+ ) /\ ( ( A mod N ) mod n ) = ( A mod n ) ) -> ( ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) mod n ) = ( ( A ^ ( ( n - 1 ) / 2 ) ) mod n ) )
48 4 21 17 28 46 47 syl221anc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) mod n ) = ( ( A ^ ( ( n - 1 ) / 2 ) ) mod n ) )
49 modadd1 
 |-  ( ( ( ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) e. RR /\ ( A ^ ( ( n - 1 ) / 2 ) ) e. RR ) /\ ( 1 e. RR /\ n e. RR+ ) /\ ( ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) mod n ) = ( ( A ^ ( ( n - 1 ) / 2 ) ) mod n ) ) -> ( ( ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) = ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) )
50 20 24 25 28 48 49 syl221anc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) = ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) )
51 50 oveq1d 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( ( ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) = ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) )
52 lgsval3 
 |-  ( ( ( A mod N ) e. ZZ /\ n e. ( Prime \ { 2 } ) ) -> ( ( A mod N ) /L n ) = ( ( ( ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) )
53 4 14 52 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( A mod N ) /L n ) = ( ( ( ( ( A mod N ) ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) )
54 lgsval3 
 |-  ( ( A e. ZZ /\ n e. ( Prime \ { 2 } ) ) -> ( A /L n ) = ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) )
55 21 14 54 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( A /L n ) = ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) )
56 51 53 55 3eqtr4d 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( A mod N ) /L n ) = ( A /L n ) )
57 56 oveq1d 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ n || N ) -> ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) = ( ( A /L n ) ^ ( n pCnt N ) ) )
58 3 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( A mod N ) e. ZZ )
59 29 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> n e. ZZ )
60 lgscl 
 |-  ( ( ( A mod N ) e. ZZ /\ n e. ZZ ) -> ( ( A mod N ) /L n ) e. ZZ )
61 58 59 60 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( ( A mod N ) /L n ) e. ZZ )
62 61 zcnd 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( ( A mod N ) /L n ) e. CC )
63 62 exp0d 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( ( ( A mod N ) /L n ) ^ 0 ) = 1 )
64 simpll1 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> A e. ZZ )
65 lgscl 
 |-  ( ( A e. ZZ /\ n e. ZZ ) -> ( A /L n ) e. ZZ )
66 64 59 65 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( A /L n ) e. ZZ )
67 66 zcnd 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( A /L n ) e. CC )
68 67 exp0d 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( ( A /L n ) ^ 0 ) = 1 )
69 63 68 eqtr4d 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( ( ( A mod N ) /L n ) ^ 0 ) = ( ( A /L n ) ^ 0 ) )
70 31 adantr 
 |-  ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) -> N e. NN )
71 pceq0 
 |-  ( ( n e. Prime /\ N e. NN ) -> ( ( n pCnt N ) = 0 <-> -. n || N ) )
72 5 70 71 syl2anc 
 |-  ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) -> ( ( n pCnt N ) = 0 <-> -. n || N ) )
73 72 biimpar 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( n pCnt N ) = 0 )
74 73 oveq2d 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) = ( ( ( A mod N ) /L n ) ^ 0 ) )
75 73 oveq2d 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( ( A /L n ) ^ ( n pCnt N ) ) = ( ( A /L n ) ^ 0 ) )
76 69 74 75 3eqtr4d 
 |-  ( ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) /\ -. n || N ) -> ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) = ( ( A /L n ) ^ ( n pCnt N ) ) )
77 57 76 pm2.61dan 
 |-  ( ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) /\ n e. Prime ) -> ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) = ( ( A /L n ) ^ ( n pCnt N ) ) )
78 77 ifeq1da 
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> if ( n e. Prime , ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) , 1 ) = if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) )
79 78 mpteq2dv 
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( n e. NN |-> if ( n e. Prime , ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) )
80 79 seqeq3d 
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) = seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) )
81 80 fveq1d 
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` N ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` N ) )
82 eqid 
 |-  ( n e. NN |-> if ( n e. Prime , ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) , 1 ) )
83 82 lgsval4a 
 |-  ( ( ( A mod N ) e. ZZ /\ N e. NN ) -> ( ( A mod N ) /L N ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` N ) )
84 3 31 83 syl2anc 
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( ( A mod N ) /L N ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( ( A mod N ) /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` N ) )
85 eqid 
 |-  ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) )
86 85 lgsval4a 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( A /L N ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` N ) )
87 86 3adant3 
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( A /L N ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) ) ` N ) )
88 81 84 87 3eqtr4d 
 |-  ( ( A e. ZZ /\ N e. NN /\ -. 2 || N ) -> ( ( A mod N ) /L N ) = ( A /L N ) )