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 ) )