Metamath Proof Explorer

Theorem gausslemma2dlem1

Description: Lemma 1 for gausslemma2d . (Contributed by AV, 5-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 ) ) ) )
Assertion gausslemma2dlem1 
|- ( ph -> ( ! ` H ) = prod_ k e. ( 1 ... H ) ( R ` k ) )

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 1 2 gausslemma2dlem0b 
 |-  ( ph -> H e. NN )
5 4 nnnn0d 
 |-  ( ph -> H e. NN0 )
6 fprodfac 
 |-  ( H e. NN0 -> ( ! ` H ) = prod_ l e. ( 1 ... H ) l )
7 5 6 syl 
 |-  ( ph -> ( ! ` H ) = prod_ l e. ( 1 ... H ) l )
8 id 
 |-  ( l = ( R ` k ) -> l = ( R ` k ) )
9 fzfid 
 |-  ( ph -> ( 1 ... H ) e. Fin )
10 fzfi 
 |-  ( 1 ... H ) e. Fin
11 ovex 
 |-  ( x x. 2 ) e. _V
12 ovex 
 |-  ( P - ( x x. 2 ) ) e. _V
13 11 12 ifex 
 |-  if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) e. _V
14 13 3 fnmpti 
 |-  R Fn ( 1 ... H )
15 1 2 3 gausslemma2dlem1a 
 |-  ( ph -> ran R = ( 1 ... H ) )
16 rneqdmfinf1o 
 |-  ( ( ( 1 ... H ) e. Fin /\ R Fn ( 1 ... H ) /\ ran R = ( 1 ... H ) ) -> R : ( 1 ... H ) -1-1-onto-> ( 1 ... H ) )
17 10 14 15 16 mp3an12i 
 |-  ( ph -> R : ( 1 ... H ) -1-1-onto-> ( 1 ... H ) )
18 eqidd 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> ( R ` k ) = ( R ` k ) )
19 elfzelz 
 |-  ( l e. ( 1 ... H ) -> l e. ZZ )
20 19 zcnd 
 |-  ( l e. ( 1 ... H ) -> l e. CC )
21 20 adantl 
 |-  ( ( ph /\ l e. ( 1 ... H ) ) -> l e. CC )
22 8 9 17 18 21 fprodf1o 
 |-  ( ph -> prod_ l e. ( 1 ... H ) l = prod_ k e. ( 1 ... H ) ( R ` k ) )
23 7 22 eqtrd 
 |-  ( ph -> ( ! ` H ) = prod_ k e. ( 1 ... H ) ( R ` k ) )