Metamath Proof Explorer

Theorem gausslemma2dlem6

Description: Lemma 6 for gausslemma2d . (Contributed by AV, 16-Jun-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 gausslemma2dlem6 
|- ( ph -> ( ( ! ` H ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) 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 gausslemma2d.n 
 |-  N = ( H - M )
6 1 2 3 4 gausslemma2dlem4 
 |-  ( ph -> ( ! ` H ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )
7 6 oveq1d 
 |-  ( ph -> ( ( ! ` H ) mod P ) = ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) mod P ) )
8 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
9 1 2 3 4 gausslemma2dlem2 
 |-  ( ph -> A. k e. ( 1 ... M ) ( R ` k ) = ( k x. 2 ) )
10 9 adantr 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> A. k e. ( 1 ... M ) ( R ` k ) = ( k x. 2 ) )
11 rspa 
 |-  ( ( A. k e. ( 1 ... M ) ( R ` k ) = ( k x. 2 ) /\ k e. ( 1 ... M ) ) -> ( R ` k ) = ( k x. 2 ) )
12 11 expcom 
 |-  ( k e. ( 1 ... M ) -> ( A. k e. ( 1 ... M ) ( R ` k ) = ( k x. 2 ) -> ( R ` k ) = ( k x. 2 ) ) )
13 12 adantl 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( A. k e. ( 1 ... M ) ( R ` k ) = ( k x. 2 ) -> ( R ` k ) = ( k x. 2 ) ) )
14 elfzelz 
 |-  ( k e. ( 1 ... M ) -> k e. ZZ )
15 2z 
 |-  2 e. ZZ
16 15 a1i 
 |-  ( k e. ( 1 ... M ) -> 2 e. ZZ )
17 14 16 zmulcld 
 |-  ( k e. ( 1 ... M ) -> ( k x. 2 ) e. ZZ )
18 17 adantl 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( k x. 2 ) e. ZZ )
19 eleq1 
 |-  ( ( R ` k ) = ( k x. 2 ) -> ( ( R ` k ) e. ZZ <-> ( k x. 2 ) e. ZZ ) )
20 18 19 syl5ibrcom 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( ( R ` k ) = ( k x. 2 ) -> ( R ` k ) e. ZZ ) )
21 13 20 syld 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( A. k e. ( 1 ... M ) ( R ` k ) = ( k x. 2 ) -> ( R ` k ) e. ZZ ) )
22 10 21 mpd 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( R ` k ) e. ZZ )
23 8 22 fprodzcl 
 |-  ( ph -> prod_ k e. ( 1 ... M ) ( R ` k ) e. ZZ )
24 fzfid 
 |-  ( ph -> ( ( M + 1 ) ... H ) e. Fin )
25 1 2 3 4 gausslemma2dlem3 
 |-  ( ph -> A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) )
26 25 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) )
27 rspa 
 |-  ( ( A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) /\ k e. ( ( M + 1 ) ... H ) ) -> ( R ` k ) = ( P - ( k x. 2 ) ) )
28 27 expcom 
 |-  ( k e. ( ( M + 1 ) ... H ) -> ( A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) -> ( R ` k ) = ( P - ( k x. 2 ) ) ) )
29 28 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> ( A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) -> ( R ` k ) = ( P - ( k x. 2 ) ) ) )
30 1 gausslemma2dlem0a 
 |-  ( ph -> P e. NN )
31 30 nnzd 
 |-  ( ph -> P e. ZZ )
32 elfzelz 
 |-  ( k e. ( ( M + 1 ) ... H ) -> k e. ZZ )
33 15 a1i 
 |-  ( k e. ( ( M + 1 ) ... H ) -> 2 e. ZZ )
34 32 33 zmulcld 
 |-  ( k e. ( ( M + 1 ) ... H ) -> ( k x. 2 ) e. ZZ )
35 zsubcl 
 |-  ( ( P e. ZZ /\ ( k x. 2 ) e. ZZ ) -> ( P - ( k x. 2 ) ) e. ZZ )
36 31 34 35 syl2an 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> ( P - ( k x. 2 ) ) e. ZZ )
37 eleq1 
 |-  ( ( R ` k ) = ( P - ( k x. 2 ) ) -> ( ( R ` k ) e. ZZ <-> ( P - ( k x. 2 ) ) e. ZZ ) )
38 36 37 syl5ibrcom 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> ( ( R ` k ) = ( P - ( k x. 2 ) ) -> ( R ` k ) e. ZZ ) )
39 29 38 syld 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> ( A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) -> ( R ` k ) e. ZZ ) )
40 26 39 mpd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> ( R ` k ) e. ZZ )
41 24 40 fprodzcl 
 |-  ( ph -> prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) e. ZZ )
42 41 zred 
 |-  ( ph -> prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) e. RR )
43 nnoddn2prm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. NN /\ -. 2 || P ) )
44 nnrp 
 |-  ( P e. NN -> P e. RR+ )
45 44 adantr 
 |-  ( ( P e. NN /\ -. 2 || P ) -> P e. RR+ )
46 1 43 45 3syl 
 |-  ( ph -> P e. RR+ )
47 modmulmodr 
 |-  ( ( prod_ k e. ( 1 ... M ) ( R ` k ) e. ZZ /\ prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) e. RR /\ P e. RR+ ) -> ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) ) mod P ) = ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) mod P ) )
48 47 eqcomd 
 |-  ( ( prod_ k e. ( 1 ... M ) ( R ` k ) e. ZZ /\ prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) e. RR /\ P e. RR+ ) -> ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) mod P ) = ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) ) mod P ) )
49 23 42 46 48 syl3anc 
 |-  ( ph -> ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) mod P ) = ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) ) mod P ) )
50 1 2 3 4 5 gausslemma2dlem5 
 |-  ( ph -> ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) = ( ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) mod P ) )
51 50 oveq2d 
 |-  ( ph -> ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) mod P ) ) )
52 51 oveq1d 
 |-  ( ph -> ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) ) mod P ) = ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) mod P ) ) mod P ) )
53 neg1rr 
 |-  -u 1 e. RR
54 53 a1i 
 |-  ( ph -> -u 1 e. RR )
55 1 4 2 5 gausslemma2dlem0h 
 |-  ( ph -> N e. NN0 )
56 54 55 reexpcld 
 |-  ( ph -> ( -u 1 ^ N ) e. RR )
57 32 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> k e. ZZ )
58 15 a1i 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> 2 e. ZZ )
59 57 58 zmulcld 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> ( k x. 2 ) e. ZZ )
60 24 59 fprodzcl 
 |-  ( ph -> prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) e. ZZ )
61 60 zred 
 |-  ( ph -> prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) e. RR )
62 56 61 remulcld 
 |-  ( ph -> ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) e. RR )
63 modmulmodr 
 |-  ( ( prod_ k e. ( 1 ... M ) ( R ` k ) e. ZZ /\ ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) e. RR /\ P e. RR+ ) -> ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) mod P ) ) mod P ) = ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) ) mod P ) )
64 23 62 46 63 syl3anc 
 |-  ( ph -> ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) mod P ) ) mod P ) = ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) ) mod P ) )
65 9 prodeq2d 
 |-  ( ph -> prod_ k e. ( 1 ... M ) ( R ` k ) = prod_ k e. ( 1 ... M ) ( k x. 2 ) )
66 65 oveq1d 
 |-  ( ph -> ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) = ( prod_ k e. ( 1 ... M ) ( k x. 2 ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) )
67 fzfid 
 |-  ( ph -> ( 1 ... H ) e. Fin )
68 elfzelz 
 |-  ( k e. ( 1 ... H ) -> k e. ZZ )
69 68 zcnd 
 |-  ( k e. ( 1 ... H ) -> k e. CC )
70 69 adantl 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> k e. CC )
71 2cn 
 |-  2 e. CC
72 71 a1i 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> 2 e. CC )
73 67 70 72 fprodmul 
 |-  ( ph -> prod_ k e. ( 1 ... H ) ( k x. 2 ) = ( prod_ k e. ( 1 ... H ) k x. prod_ k e. ( 1 ... H ) 2 ) )
74 1 4 gausslemma2dlem0d 
 |-  ( ph -> M e. NN0 )
75 74 nn0red 
 |-  ( ph -> M e. RR )
76 75 ltp1d 
 |-  ( ph -> M < ( M + 1 ) )
77 fzdisj 
 |-  ( M < ( M + 1 ) -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... H ) ) = (/) )
78 76 77 syl 
 |-  ( ph -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... H ) ) = (/) )
79 1zzd 
 |-  ( ph -> 1 e. ZZ )
80 nn0pzuz 
 |-  ( ( M e. NN0 /\ 1 e. ZZ ) -> ( M + 1 ) e. ( ZZ>= ` 1 ) )
81 74 79 80 syl2anc 
 |-  ( ph -> ( M + 1 ) e. ( ZZ>= ` 1 ) )
82 74 nn0zd 
 |-  ( ph -> M e. ZZ )
83 1 2 gausslemma2dlem0b 
 |-  ( ph -> H e. NN )
84 83 nnzd 
 |-  ( ph -> H e. ZZ )
85 1 4 2 gausslemma2dlem0g 
 |-  ( ph -> M <_ H )
86 eluz2 
 |-  ( H e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ H e. ZZ /\ M <_ H ) )
87 82 84 85 86 syl3anbrc 
 |-  ( ph -> H e. ( ZZ>= ` M ) )
88 fzsplit2 
 |-  ( ( ( M + 1 ) e. ( ZZ>= ` 1 ) /\ H e. ( ZZ>= ` M ) ) -> ( 1 ... H ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... H ) ) )
89 81 87 88 syl2anc 
 |-  ( ph -> ( 1 ... H ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... H ) ) )
90 15 a1i 
 |-  ( k e. ( 1 ... H ) -> 2 e. ZZ )
91 68 90 zmulcld 
 |-  ( k e. ( 1 ... H ) -> ( k x. 2 ) e. ZZ )
92 91 adantl 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> ( k x. 2 ) e. ZZ )
93 92 zcnd 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> ( k x. 2 ) e. CC )
94 78 89 67 93 fprodsplit 
 |-  ( ph -> prod_ k e. ( 1 ... H ) ( k x. 2 ) = ( prod_ k e. ( 1 ... M ) ( k x. 2 ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) )
95 nnnn0 
 |-  ( P e. NN -> P e. NN0 )
96 95 anim1i 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( P e. NN0 /\ -. 2 || P ) )
97 43 96 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. NN0 /\ -. 2 || P ) )
98 nn0oddm1d2 
 |-  ( P e. NN0 -> ( -. 2 || P <-> ( ( P - 1 ) / 2 ) e. NN0 ) )
99 98 biimpa 
 |-  ( ( P e. NN0 /\ -. 2 || P ) -> ( ( P - 1 ) / 2 ) e. NN0 )
100 2 99 eqeltrid 
 |-  ( ( P e. NN0 /\ -. 2 || P ) -> H e. NN0 )
101 1 97 100 3syl 
 |-  ( ph -> H e. NN0 )
102 fprodfac 
 |-  ( H e. NN0 -> ( ! ` H ) = prod_ k e. ( 1 ... H ) k )
103 101 102 syl 
 |-  ( ph -> ( ! ` H ) = prod_ k e. ( 1 ... H ) k )
104 103 eqcomd 
 |-  ( ph -> prod_ k e. ( 1 ... H ) k = ( ! ` H ) )
105 fzfi 
 |-  ( 1 ... H ) e. Fin
106 105 71 pm3.2i 
 |-  ( ( 1 ... H ) e. Fin /\ 2 e. CC )
107 fprodconst 
 |-  ( ( ( 1 ... H ) e. Fin /\ 2 e. CC ) -> prod_ k e. ( 1 ... H ) 2 = ( 2 ^ ( # ` ( 1 ... H ) ) ) )
108 106 107 mp1i 
 |-  ( ph -> prod_ k e. ( 1 ... H ) 2 = ( 2 ^ ( # ` ( 1 ... H ) ) ) )
109 104 108 oveq12d 
 |-  ( ph -> ( prod_ k e. ( 1 ... H ) k x. prod_ k e. ( 1 ... H ) 2 ) = ( ( ! ` H ) x. ( 2 ^ ( # ` ( 1 ... H ) ) ) ) )
110 hashfz1 
 |-  ( H e. NN0 -> ( # ` ( 1 ... H ) ) = H )
111 101 110 syl 
 |-  ( ph -> ( # ` ( 1 ... H ) ) = H )
112 111 oveq2d 
 |-  ( ph -> ( 2 ^ ( # ` ( 1 ... H ) ) ) = ( 2 ^ H ) )
113 112 oveq2d 
 |-  ( ph -> ( ( ! ` H ) x. ( 2 ^ ( # ` ( 1 ... H ) ) ) ) = ( ( ! ` H ) x. ( 2 ^ H ) ) )
114 101 faccld 
 |-  ( ph -> ( ! ` H ) e. NN )
115 114 nncnd 
 |-  ( ph -> ( ! ` H ) e. CC )
116 2nn0 
 |-  2 e. NN0
117 nn0expcl 
 |-  ( ( 2 e. NN0 /\ H e. NN0 ) -> ( 2 ^ H ) e. NN0 )
118 117 nn0cnd 
 |-  ( ( 2 e. NN0 /\ H e. NN0 ) -> ( 2 ^ H ) e. CC )
119 116 101 118 sylancr 
 |-  ( ph -> ( 2 ^ H ) e. CC )
120 115 119 mulcomd 
 |-  ( ph -> ( ( ! ` H ) x. ( 2 ^ H ) ) = ( ( 2 ^ H ) x. ( ! ` H ) ) )
121 109 113 120 3eqtrd 
 |-  ( ph -> ( prod_ k e. ( 1 ... H ) k x. prod_ k e. ( 1 ... H ) 2 ) = ( ( 2 ^ H ) x. ( ! ` H ) ) )
122 73 94 121 3eqtr3d 
 |-  ( ph -> ( prod_ k e. ( 1 ... M ) ( k x. 2 ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) = ( ( 2 ^ H ) x. ( ! ` H ) ) )
123 66 122 eqtrd 
 |-  ( ph -> ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) = ( ( 2 ^ H ) x. ( ! ` H ) ) )
124 123 oveq2d 
 |-  ( ph -> ( ( -u 1 ^ N ) x. ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) ) = ( ( -u 1 ^ N ) x. ( ( 2 ^ H ) x. ( ! ` H ) ) ) )
125 23 zcnd 
 |-  ( ph -> prod_ k e. ( 1 ... M ) ( R ` k ) e. CC )
126 56 recnd 
 |-  ( ph -> ( -u 1 ^ N ) e. CC )
127 60 zcnd 
 |-  ( ph -> prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) e. CC )
128 125 126 127 mul12d 
 |-  ( ph -> ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) ) = ( ( -u 1 ^ N ) x. ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) ) )
129 126 119 115 mulassd 
 |-  ( ph -> ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) = ( ( -u 1 ^ N ) x. ( ( 2 ^ H ) x. ( ! ` H ) ) ) )
130 124 128 129 3eqtr4d 
 |-  ( ph -> ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) ) = ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) )
131 130 oveq1d 
 |-  ( ph -> ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( ( -u 1 ^ N ) x. prod_ k e. ( ( M + 1 ) ... H ) ( k x. 2 ) ) ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) )
132 52 64 131 3eqtrd 
 |-  ( ph -> ( ( prod_ k e. ( 1 ... M ) ( R ` k ) x. ( prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) mod P ) ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) )
133 7 49 132 3eqtrd 
 |-  ( ph -> ( ( ! ` H ) mod P ) = ( ( ( ( -u 1 ^ N ) x. ( 2 ^ H ) ) x. ( ! ` H ) ) mod P ) )