Metamath Proof Explorer

Theorem gausslemma2dlem5

Description: Lemma 5 for gausslemma2d . (Contributed by AV, 9-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 gausslemma2dlem5 
|- ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) = ( ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) mod P ) )

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 gausslemma2dlem5a 
 |-  ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) = ( prod_ k e. ( ( M + 1 ) ... H ) ( -u 1 x. ( k x. 2 ) ) mod P ) )
7 fzfi 
 |-  ( ( M + 1 ) ... H ) e. Fin
8 7 a1i 
 |-  ( ph -> ( ( M + 1 ) ... H ) e. Fin )
9 neg1cn 
 |-  -u 1 e. CC
10 9 a1i 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> -u 1 e. CC )
11 elfzelz 
 |-  ( k e. ( ( M + 1 ) ... H ) -> k e. ZZ )
12 2z 
 |-  2 e. ZZ
13 12 a1i 
 |-  ( k e. ( ( M + 1 ) ... H ) -> 2 e. ZZ )
14 11 13 zmulcld 
 |-  ( k e. ( ( M + 1 ) ... H ) -> ( k x. 2 ) e. ZZ )
15 14 zcnd 
 |-  ( k e. ( ( M + 1 ) ... H ) -> ( k x. 2 ) e. CC )
16 15 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> ( k x. 2 ) e. CC )
17 8 10 16 fprodmul 
 |-  ( ph -> prod_ k e. ( ( M + 1 ) ... H ) ( -u 1 x. ( k x. 2 ) ) = ( prod_ k e. ( ( M + 1 ) ... H ) -u 1 x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) )
18 7 9 pm3.2i 
 |-  ( ( ( M + 1 ) ... H ) e. Fin /\ -u 1 e. CC )
19 fprodconst 
 |-  ( ( ( ( M + 1 ) ... H ) e. Fin /\ -u 1 e. CC ) -> prod_ k e. ( ( M + 1 ) ... H ) -u 1 = ( -u 1 ^ ( # ` ( ( M + 1 ) ... H ) ) ) )
20 18 19 mp1i 
 |-  ( ph -> prod_ k e. ( ( M + 1 ) ... H ) -u 1 = ( -u 1 ^ ( # ` ( ( M + 1 ) ... H ) ) ) )
21 nnoddn2prm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. NN /\ -. 2 || P ) )
22 nnre 
 |-  ( P e. NN -> P e. RR )
23 22 adantr 
 |-  ( ( P e. NN /\ -. 2 || P ) -> P e. RR )
24 1 21 23 3syl 
 |-  ( ph -> P e. RR )
25 4re 
 |-  4 e. RR
26 25 a1i 
 |-  ( ph -> 4 e. RR )
27 4ne0 
 |-  4 =/= 0
28 27 a1i 
 |-  ( ph -> 4 =/= 0 )
29 24 26 28 redivcld 
 |-  ( ph -> ( P / 4 ) e. RR )
30 29 flcld 
 |-  ( ph -> ( |_ ` ( P / 4 ) ) e. ZZ )
31 4 30 eqeltrid 
 |-  ( ph -> M e. ZZ )
32 31 peano2zd 
 |-  ( ph -> ( M + 1 ) e. ZZ )
33 nnz 
 |-  ( P e. NN -> P e. ZZ )
34 oddm1d2 
 |-  ( P e. ZZ -> ( -. 2 || P <-> ( ( P - 1 ) / 2 ) e. ZZ ) )
35 33 34 syl 
 |-  ( P e. NN -> ( -. 2 || P <-> ( ( P - 1 ) / 2 ) e. ZZ ) )
36 35 biimpa 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( ( P - 1 ) / 2 ) e. ZZ )
37 1 21 36 3syl 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. ZZ )
38 2 37 eqeltrid 
 |-  ( ph -> H e. ZZ )
39 1 4 2 gausslemma2dlem0f 
 |-  ( ph -> ( M + 1 ) <_ H )
40 eluz2 
 |-  ( H e. ( ZZ>= ` ( M + 1 ) ) <-> ( ( M + 1 ) e. ZZ /\ H e. ZZ /\ ( M + 1 ) <_ H ) )
41 32 38 39 40 syl3anbrc 
 |-  ( ph -> H e. ( ZZ>= ` ( M + 1 ) ) )
42 hashfz 
 |-  ( H e. ( ZZ>= ` ( M + 1 ) ) -> ( # ` ( ( M + 1 ) ... H ) ) = ( ( H - ( M + 1 ) ) + 1 ) )
43 41 42 syl 
 |-  ( ph -> ( # ` ( ( M + 1 ) ... H ) ) = ( ( H - ( M + 1 ) ) + 1 ) )
44 38 zcnd 
 |-  ( ph -> H e. CC )
45 31 zcnd 
 |-  ( ph -> M e. CC )
46 1cnd 
 |-  ( ph -> 1 e. CC )
47 44 45 46 nppcan2d 
 |-  ( ph -> ( ( H - ( M + 1 ) ) + 1 ) = ( H - M ) )
48 47 5 eqtr4di 
 |-  ( ph -> ( ( H - ( M + 1 ) ) + 1 ) = N )
49 43 48 eqtrd 
 |-  ( ph -> ( # ` ( ( M + 1 ) ... H ) ) = N )
50 49 oveq2d 
 |-  ( ph -> ( -u 1 ^ ( # ` ( ( M + 1 ) ... H ) ) ) = ( -u 1 ^ N ) )
51 20 50 eqtrd 
 |-  ( ph -> prod_ k e. ( ( M + 1 ) ... H ) -u 1 = ( -u 1 ^ N ) )
52 51 oveq1d 
 |-  ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) -u 1 x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) = ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) )
53 17 52 eqtrd 
 |-  ( ph -> prod_ k e. ( ( M + 1 ) ... H ) ( -u 1 x. ( k x. 2 ) ) = ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) )
54 53 oveq1d 
 |-  ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) ( -u 1 x. ( k x. 2 ) ) mod P ) = ( ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) mod P ) )
55 6 54 eqtrd 
 |-  ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) = ( ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) mod P ) )