Metamath Proof Explorer

Theorem gausslemma2dlem5a

Description: Lemma for gausslemma2dlem5 . (Contributed by AV, 8-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 ) )
Assertion 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 ) )

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 1 2 3 4 gausslemma2dlem3 
 |-  ( ph -> A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) )
6 prodeq2 
 |-  ( A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) -> prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) = prod_ k e. ( ( M + 1 ) ... H ) ( P - ( k x. 2 ) ) )
7 6 oveq1d 
 |-  ( A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) -> ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) = ( prod_ k e. ( ( M + 1 ) ... H ) ( P - ( k x. 2 ) ) mod P ) )
8 5 7 syl 
 |-  ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) = ( prod_ k e. ( ( M + 1 ) ... H ) ( P - ( k x. 2 ) ) mod P ) )
9 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
10 fzfid 
 |-  ( P e. Prime -> ( ( M + 1 ) ... H ) e. Fin )
11 prmz 
 |-  ( P e. Prime -> P e. ZZ )
12 11 adantr 
 |-  ( ( P e. Prime /\ k e. ( ( M + 1 ) ... H ) ) -> P e. ZZ )
13 elfzelz 
 |-  ( k e. ( ( M + 1 ) ... H ) -> k e. ZZ )
14 2z 
 |-  2 e. ZZ
15 14 a1i 
 |-  ( k e. ( ( M + 1 ) ... H ) -> 2 e. ZZ )
16 13 15 zmulcld 
 |-  ( k e. ( ( M + 1 ) ... H ) -> ( k x. 2 ) e. ZZ )
17 16 adantl 
 |-  ( ( P e. Prime /\ k e. ( ( M + 1 ) ... H ) ) -> ( k x. 2 ) e. ZZ )
18 12 17 zsubcld 
 |-  ( ( P e. Prime /\ k e. ( ( M + 1 ) ... H ) ) -> ( P - ( k x. 2 ) ) e. ZZ )
19 neg1z 
 |-  -u 1 e. ZZ
20 19 a1i 
 |-  ( k e. ( ( M + 1 ) ... H ) -> -u 1 e. ZZ )
21 20 16 zmulcld 
 |-  ( k e. ( ( M + 1 ) ... H ) -> ( -u 1 x. ( k x. 2 ) ) e. ZZ )
22 21 adantl 
 |-  ( ( P e. Prime /\ k e. ( ( M + 1 ) ... H ) ) -> ( -u 1 x. ( k x. 2 ) ) e. ZZ )
23 prmnn 
 |-  ( P e. Prime -> P e. NN )
24 16 zcnd 
 |-  ( k e. ( ( M + 1 ) ... H ) -> ( k x. 2 ) e. CC )
25 24 mulm1d 
 |-  ( k e. ( ( M + 1 ) ... H ) -> ( -u 1 x. ( k x. 2 ) ) = -u ( k x. 2 ) )
26 25 adantl 
 |-  ( ( P e. Prime /\ k e. ( ( M + 1 ) ... H ) ) -> ( -u 1 x. ( k x. 2 ) ) = -u ( k x. 2 ) )
27 26 oveq1d 
 |-  ( ( P e. Prime /\ k e. ( ( M + 1 ) ... H ) ) -> ( ( -u 1 x. ( k x. 2 ) ) mod P ) = ( -u ( k x. 2 ) mod P ) )
28 16 zred 
 |-  ( k e. ( ( M + 1 ) ... H ) -> ( k x. 2 ) e. RR )
29 23 nnrpd 
 |-  ( P e. Prime -> P e. RR+ )
30 negmod 
 |-  ( ( ( k x. 2 ) e. RR /\ P e. RR+ ) -> ( -u ( k x. 2 ) mod P ) = ( ( P - ( k x. 2 ) ) mod P ) )
31 28 29 30 syl2anr 
 |-  ( ( P e. Prime /\ k e. ( ( M + 1 ) ... H ) ) -> ( -u ( k x. 2 ) mod P ) = ( ( P - ( k x. 2 ) ) mod P ) )
32 27 31 eqtr2d 
 |-  ( ( P e. Prime /\ k e. ( ( M + 1 ) ... H ) ) -> ( ( P - ( k x. 2 ) ) mod P ) = ( ( -u 1 x. ( k x. 2 ) ) mod P ) )
33 10 18 22 23 32 fprodmodd 
 |-  ( P e. Prime -> ( prod_ k e. ( ( M + 1 ) ... H ) ( P - ( k x. 2 ) ) mod P ) = ( prod_ k e. ( ( M + 1 ) ... H ) ( -u 1 x. ( k x. 2 ) ) mod P ) )
34 1 9 33 3syl 
 |-  ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) ( P - ( k x. 2 ) ) mod P ) = ( prod_ k e. ( ( M + 1 ) ... H ) ( -u 1 x. ( k x. 2 ) ) mod P ) )
35 8 34 eqtrd 
 |-  ( 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 ) )