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