Metamath Proof Explorer

Theorem gausslemma2d

Description: Gauss' Lemma (see also theorem 9.6 in ApostolNT p. 182) for integer 2 : Let p be an odd prime. Let S={2,4,6,...,(p-1)}. Let n denote the number of elements of S whose least positive residue modulo p is greater than p/2. Then ( 2 | p ) = (-1)^n. (Contributed by AV, 14-Jul-2021)

Ref Expression
Hypotheses gausslemma2d.p 
|- ( ph -> P e. ( Prime \ { 2 } ) )
gausslemma2d.h 
|- H = ( ( P - 1 ) / 2 )
gausslemma2d.r 
|- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )
gausslemma2d.m 
|- M = ( |_ ` ( P / 4 ) )
gausslemma2d.n 
|- N = ( H - M )
Assertion gausslemma2d 
|- ( ph -> ( 2 /L P ) = ( -u 1 ^ N ) )

Proof

Step Hyp Ref Expression
1 gausslemma2d.p 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 gausslemma2d.h 
 |-  H = ( ( P - 1 ) / 2 )
3 gausslemma2d.r 
 |-  R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )
4 gausslemma2d.m 
 |-  M = ( |_ ` ( P / 4 ) )
5 gausslemma2d.n 
 |-  N = ( H - M )
6 1 2 3 4 5 gausslemma2dlem7 
 |-  ( ph -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = 1 )
7 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
8 prmnn 
 |-  ( P e. Prime -> P e. NN )
9 8 nnred 
 |-  ( P e. Prime -> P e. RR )
10 prmgt1 
 |-  ( P e. Prime -> 1 < P )
11 9 10 jca 
 |-  ( P e. Prime -> ( P e. RR /\ 1 < P ) )
12 1 7 11 3syl 
 |-  ( ph -> ( P e. RR /\ 1 < P ) )
13 1mod 
 |-  ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 )
14 12 13 syl 
 |-  ( ph -> ( 1 mod P ) = 1 )
15 14 eqcomd 
 |-  ( ph -> 1 = ( 1 mod P ) )
16 15 eqeq2d 
 |-  ( ph -> ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = 1 <-> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = ( 1 mod P ) ) )
17 neg1z 
 |-  -u 1 e. ZZ
18 1 4 2 5 gausslemma2dlem0h 
 |-  ( ph -> N e. NN0 )
19 zexpcl 
 |-  ( ( -u 1 e. ZZ /\ N e. NN0 ) -> ( -u 1 ^ N ) e. ZZ )
20 17 18 19 sylancr 
 |-  ( ph -> ( -u 1 ^ N ) e. ZZ )
21 2nn 
 |-  2 e. NN
22 21 a1i 
 |-  ( ph -> 2 e. NN )
23 1 2 gausslemma2dlem0b 
 |-  ( ph -> H e. NN )
24 23 nnnn0d 
 |-  ( ph -> H e. NN0 )
25 22 24 nnexpcld 
 |-  ( ph -> ( 2 ^ H ) e. NN )
26 25 nnzd 
 |-  ( ph -> ( 2 ^ H ) e. ZZ )
27 20 26 zmulcld 
 |-  ( ph -> ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) e. ZZ )
28 27 zred 
 |-  ( ph -> ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) e. RR )
29 1red 
 |-  ( ph -> 1 e. RR )
30 28 29 jca 
 |-  ( ph -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) e. RR /\ 1 e. RR ) )
31 30 adantr 
 |-  ( ( ph /\ ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = ( 1 mod P ) ) -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) e. RR /\ 1 e. RR ) )
32 1 gausslemma2dlem0a 
 |-  ( ph -> P e. NN )
33 32 nnrpd 
 |-  ( ph -> P e. RR+ )
34 20 33 jca 
 |-  ( ph -> ( ( -u 1 ^ N ) e. ZZ /\ P e. RR+ ) )
35 34 adantr 
 |-  ( ( ph /\ ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = ( 1 mod P ) ) -> ( ( -u 1 ^ N ) e. ZZ /\ P e. RR+ ) )
36 simpr 
 |-  ( ( ph /\ ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = ( 1 mod P ) ) -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = ( 1 mod P ) )
37 modmul1 
 |-  ( ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) e. RR /\ 1 e. RR ) /\ ( ( -u 1 ^ N ) e. ZZ /\ P e. RR+ ) /\ ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = ( 1 mod P ) ) -> ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( -u 1 ^ N ) ) mod P ) = ( ( 1 x. ( -u 1 ^ N ) ) mod P ) )
38 31 35 36 37 syl3anc 
 |-  ( ( ph /\ ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = ( 1 mod P ) ) -> ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( -u 1 ^ N ) ) mod P ) = ( ( 1 x. ( -u 1 ^ N ) ) mod P ) )
39 38 ex 
 |-  ( ph -> ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = ( 1 mod P ) -> ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( -u 1 ^ N ) ) mod P ) = ( ( 1 x. ( -u 1 ^ N ) ) mod P ) ) )
40 20 zcnd 
 |-  ( ph -> ( -u 1 ^ N ) e. CC )
41 25 nncnd 
 |-  ( ph -> ( 2 ^ H ) e. CC )
42 40 41 40 mul32d 
 |-  ( ph -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( -u 1 ^ N ) ) = ( ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) x. ( 2 ^ H ) ) )
43 18 nn0cnd 
 |-  ( ph -> N e. CC )
44 43 2timesd 
 |-  ( ph -> ( 2 x. N ) = ( N + N ) )
45 44 eqcomd 
 |-  ( ph -> ( N + N ) = ( 2 x. N ) )
46 45 oveq2d 
 |-  ( ph -> ( -u 1 ^ ( N + N ) ) = ( -u 1 ^ ( 2 x. N ) ) )
47 neg1cn 
 |-  -u 1 e. CC
48 47 a1i 
 |-  ( ph -> -u 1 e. CC )
49 48 18 18 expaddd 
 |-  ( ph -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) )
50 18 nn0zd 
 |-  ( ph -> N e. ZZ )
51 m1expeven 
 |-  ( N e. ZZ -> ( -u 1 ^ ( 2 x. N ) ) = 1 )
52 50 51 syl 
 |-  ( ph -> ( -u 1 ^ ( 2 x. N ) ) = 1 )
53 46 49 52 3eqtr3d 
 |-  ( ph -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 )
54 53 oveq1d 
 |-  ( ph -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) x. ( 2 ^ H ) ) = ( 1 x. ( 2 ^ H ) ) )
55 41 mulid2d 
 |-  ( ph -> ( 1 x. ( 2 ^ H ) ) = ( 2 ^ H ) )
56 42 54 55 3eqtrd 
 |-  ( ph -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( -u 1 ^ N ) ) = ( 2 ^ H ) )
57 56 oveq1d 
 |-  ( ph -> ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( -u 1 ^ N ) ) mod P ) = ( ( 2 ^ H ) mod P ) )
58 40 mulid2d 
 |-  ( ph -> ( 1 x. ( -u 1 ^ N ) ) = ( -u 1 ^ N ) )
59 58 oveq1d 
 |-  ( ph -> ( ( 1 x. ( -u 1 ^ N ) ) mod P ) = ( ( -u 1 ^ N ) mod P ) )
60 57 59 eqeq12d 
 |-  ( ph -> ( ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( -u 1 ^ N ) ) mod P ) = ( ( 1 x. ( -u 1 ^ N ) ) mod P ) <-> ( ( 2 ^ H ) mod P ) = ( ( -u 1 ^ N ) mod P ) ) )
61 2 oveq2i 
 |-  ( 2 ^ H ) = ( 2 ^ ( ( P - 1 ) / 2 ) )
62 61 oveq1i 
 |-  ( ( 2 ^ H ) mod P ) = ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P )
63 62 eqeq1i 
 |-  ( ( ( 2 ^ H ) mod P ) = ( ( -u 1 ^ N ) mod P ) <-> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ N ) mod P ) )
64 2z 
 |-  2 e. ZZ
65 lgsvalmod 
 |-  ( ( 2 e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( 2 /L P ) mod P ) = ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) )
66 64 1 65 sylancr 
 |-  ( ph -> ( ( 2 /L P ) mod P ) = ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) )
67 66 eqcomd 
 |-  ( ph -> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( 2 /L P ) mod P ) )
68 67 eqeq1d 
 |-  ( ph -> ( ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ N ) mod P ) <-> ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) ) )
69 1 4 2 5 gausslemma2dlem0i 
 |-  ( ph -> ( ( ( 2 /L P ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) )
70 68 69 sylbid 
 |-  ( ph -> ( ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) )
71 63 70 syl5bi 
 |-  ( ph -> ( ( ( 2 ^ H ) mod P ) = ( ( -u 1 ^ N ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) )
72 60 71 sylbid 
 |-  ( ph -> ( ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( -u 1 ^ N ) ) mod P ) = ( ( 1 x. ( -u 1 ^ N ) ) mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) )
73 39 72 syld 
 |-  ( ph -> ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = ( 1 mod P ) -> ( 2 /L P ) = ( -u 1 ^ N ) ) )
74 16 73 sylbid 
 |-  ( ph -> ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = 1 -> ( 2 /L P ) = ( -u 1 ^ N ) ) )
75 6 74 mpd 
 |-  ( ph -> ( 2 /L P ) = ( -u 1 ^ N ) )