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