Metamath Proof Explorer

Theorem gausslemma2dlem7

Description: Lemma 7 for gausslemma2d . (Contributed by AV, 13-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 ) )
gausslemma2d.n 
|- N = ( H - M )
Assertion gausslemma2dlem7 
|- ( ph -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = 1 )

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 gausslemma2d.n 
 |-  N = ( H - M )
6 1 2 3 4 5 gausslemma2dlem6 
 |-  ( ph -> ( ( ! ` H ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) )
7 1 2 gausslemma2dlem0b 
 |-  ( ph -> H e. NN )
8 7 nnnn0d 
 |-  ( ph -> H e. NN0 )
9 8 faccld 
 |-  ( ph -> ( ! ` H ) e. NN )
10 9 nncnd 
 |-  ( ph -> ( ! ` H ) e. CC )
11 10 mulid2d 
 |-  ( ph -> ( 1 x. ( ! ` H ) ) = ( ! ` H ) )
12 11 eqcomd 
 |-  ( ph -> ( ! ` H ) = ( 1 x. ( ! ` H ) ) )
13 12 oveq1d 
 |-  ( ph -> ( ( ! ` H ) mod P ) = ( ( 1 x. ( ! ` H ) ) mod P ) )
14 13 eqeq1d 
 |-  ( ph -> ( ( ( ! ` H ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) <-> ( ( 1 x. ( ! ` H ) ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) ) )
15 1zzd 
 |-  ( ph -> 1 e. ZZ )
16 neg1z 
 |-  -u 1 e. ZZ
17 1 4 2 5 gausslemma2dlem0h 
 |-  ( ph -> N e. NN0 )
18 zexpcl 
 |-  ( ( -u 1 e. ZZ /\ N e. NN0 ) -> ( -u 1 ^ N ) e. ZZ )
19 16 17 18 sylancr 
 |-  ( ph -> ( -u 1 ^ N ) e. ZZ )
20 2z 
 |-  2 e. ZZ
21 zexpcl 
 |-  ( ( 2 e. ZZ /\ H e. NN0 ) -> ( 2 ^ H ) e. ZZ )
22 20 8 21 sylancr 
 |-  ( ph -> ( 2 ^ H ) e. ZZ )
23 19 22 zmulcld 
 |-  ( ph -> ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) e. ZZ )
24 9 nnzd 
 |-  ( ph -> ( ! ` H ) e. ZZ )
25 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
26 prmnn 
 |-  ( P e. Prime -> P e. NN )
27 1 25 26 3syl 
 |-  ( ph -> P e. NN )
28 1 2 gausslemma2dlem0c 
 |-  ( ph -> ( ( ! ` H ) gcd P ) = 1 )
29 cncongrcoprm 
 |-  ( ( ( 1 e. ZZ /\ ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) e. ZZ /\ ( ! ` H ) e. ZZ ) /\ ( P e. NN /\ ( ( ! ` H ) gcd P ) = 1 ) ) -> ( ( ( 1 x. ( ! ` H ) ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) <-> ( 1 mod P ) = ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) ) )
30 15 23 24 27 28 29 syl32anc 
 |-  ( ph -> ( ( ( 1 x. ( ! ` H ) ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) <-> ( 1 mod P ) = ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) ) )
31 14 30 bitrd 
 |-  ( ph -> ( ( ( ! ` H ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) <-> ( 1 mod P ) = ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) ) )
32 simpr 
 |-  ( ( ph /\ ( 1 mod P ) = ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) ) -> ( 1 mod P ) = ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) )
33 26 nnred 
 |-  ( P e. Prime -> P e. RR )
34 prmgt1 
 |-  ( P e. Prime -> 1 < P )
35 33 34 jca 
 |-  ( P e. Prime -> ( P e. RR /\ 1 < P ) )
36 25 35 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. RR /\ 1 < P ) )
37 1mod 
 |-  ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 )
38 1 36 37 3syl 
 |-  ( ph -> ( 1 mod P ) = 1 )
39 38 adantr 
 |-  ( ( ph /\ ( 1 mod P ) = ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) ) -> ( 1 mod P ) = 1 )
40 32 39 eqtr3d 
 |-  ( ( ph /\ ( 1 mod P ) = ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) ) -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = 1 )
41 40 ex 
 |-  ( ph -> ( ( 1 mod P ) = ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = 1 ) )
42 31 41 sylbid 
 |-  ( ph -> ( ( ( ! ` H ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = 1 ) )
43 6 42 mpd 
 |-  ( ph -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) mod P ) = 1 )