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