Metamath Proof Explorer

Theorem lgsquadlem1

Description: Lemma for lgsquad . Count the members of S with odd coordinates. (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses lgseisen.1 
|- ( ph -> P e. ( Prime \ { 2 } ) )
lgseisen.2 
|- ( ph -> Q e. ( Prime \ { 2 } ) )
lgseisen.3 
|- ( ph -> P =/= Q )
lgsquad.4 
|- M = ( ( P - 1 ) / 2 )
lgsquad.5 
|- N = ( ( Q - 1 ) / 2 )
lgsquad.6 
|- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }
Assertion lgsquadlem1 
|- ( ph -> ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) )

Proof

Step Hyp Ref Expression
1 lgseisen.1 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 lgseisen.2 
 |-  ( ph -> Q e. ( Prime \ { 2 } ) )
3 lgseisen.3 
 |-  ( ph -> P =/= Q )
4 lgsquad.4 
 |-  M = ( ( P - 1 ) / 2 )
5 lgsquad.5 
 |-  N = ( ( Q - 1 ) / 2 )
6 lgsquad.6 
 |-  S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }
7 neg1cn 
 |-  -u 1 e. CC
8 7 a1i 
 |-  ( ph -> -u 1 e. CC )
9 neg1ne0 
 |-  -u 1 =/= 0
10 9 a1i 
 |-  ( ph -> -u 1 =/= 0 )
11 fzfid 
 |-  ( ph -> ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) e. Fin )
12 2 gausslemma2dlem0a 
 |-  ( ph -> Q e. NN )
13 12 nnred 
 |-  ( ph -> Q e. RR )
14 1 gausslemma2dlem0a 
 |-  ( ph -> P e. NN )
15 13 14 nndivred 
 |-  ( ph -> ( Q / P ) e. RR )
16 15 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q / P ) e. RR )
17 2z 
 |-  2 e. ZZ
18 elfzelz 
 |-  ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) -> u e. ZZ )
19 18 adantl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u e. ZZ )
20 zmulcl 
 |-  ( ( 2 e. ZZ /\ u e. ZZ ) -> ( 2 x. u ) e. ZZ )
21 17 19 20 sylancr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) e. ZZ )
22 21 zred 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) e. RR )
23 16 22 remulcld 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / P ) x. ( 2 x. u ) ) e. RR )
24 23 flcld 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ )
25 11 24 fsumzcl 
 |-  ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ )
26 8 10 25 expclzd 
 |-  ( ph -> ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. CC )
27 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
28 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
29 xpfi 
 |-  ( ( ( 1 ... M ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( 1 ... M ) X. ( 1 ... N ) ) e. Fin )
30 27 28 29 syl2anc 
 |-  ( ph -> ( ( 1 ... M ) X. ( 1 ... N ) ) e. Fin )
31 opabssxp 
 |-  { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } C_ ( ( 1 ... M ) X. ( 1 ... N ) )
32 6 31 eqsstri 
 |-  S C_ ( ( 1 ... M ) X. ( 1 ... N ) )
33 ssfi 
 |-  ( ( ( ( 1 ... M ) X. ( 1 ... N ) ) e. Fin /\ S C_ ( ( 1 ... M ) X. ( 1 ... N ) ) ) -> S e. Fin )
34 30 32 33 sylancl 
 |-  ( ph -> S e. Fin )
35 ssrab2 
 |-  { z e. S | -. 2 || ( 1st ` z ) } C_ S
36 ssfi 
 |-  ( ( S e. Fin /\ { z e. S | -. 2 || ( 1st ` z ) } C_ S ) -> { z e. S | -. 2 || ( 1st ` z ) } e. Fin )
37 34 35 36 sylancl 
 |-  ( ph -> { z e. S | -. 2 || ( 1st ` z ) } e. Fin )
38 hashcl 
 |-  ( { z e. S | -. 2 || ( 1st ` z ) } e. Fin -> ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) e. NN0 )
39 37 38 syl 
 |-  ( ph -> ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) e. NN0 )
40 expcl 
 |-  ( ( -u 1 e. CC /\ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) e. NN0 ) -> ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) e. CC )
41 7 39 40 sylancr 
 |-  ( ph -> ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) e. CC )
42 39 nn0zd 
 |-  ( ph -> ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) e. ZZ )
43 8 10 42 expne0d 
 |-  ( ph -> ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) =/= 0 )
44 41 43 recidd 
 |-  ( ph -> ( ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) x. ( 1 / ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) ) = 1 )
45 1div1e1 
 |-  ( 1 / 1 ) = 1
46 45 negeqi 
 |-  -u ( 1 / 1 ) = -u 1
47 ax-1cn 
 |-  1 e. CC
48 ax-1ne0 
 |-  1 =/= 0
49 divneg2 
 |-  ( ( 1 e. CC /\ 1 e. CC /\ 1 =/= 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) )
50 47 47 48 49 mp3an 
 |-  -u ( 1 / 1 ) = ( 1 / -u 1 )
51 46 50 eqtr3i 
 |-  -u 1 = ( 1 / -u 1 )
52 51 oveq1i 
 |-  ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( ( 1 / -u 1 ) ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) )
53 8 10 42 exprecd 
 |-  ( ph -> ( ( 1 / -u 1 ) ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( 1 / ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
54 52 53 eqtrid 
 |-  ( ph -> ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( 1 / ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
55 54 oveq2d 
 |-  ( ph -> ( ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) x. ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) x. ( 1 / ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) ) )
56 34 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> S e. Fin )
57 ssrab2 
 |-  { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } C_ S
58 ssfi 
 |-  ( ( S e. Fin /\ { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } C_ S ) -> { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } e. Fin )
59 56 57 58 sylancl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } e. Fin )
60 fveqeq2 
 |-  ( z = v -> ( ( 1st ` z ) = ( P - ( 2 x. u ) ) <-> ( 1st ` v ) = ( P - ( 2 x. u ) ) ) )
61 60 elrab 
 |-  ( v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } <-> ( v e. S /\ ( 1st ` v ) = ( P - ( 2 x. u ) ) ) )
62 61 simprbi 
 |-  ( v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } -> ( 1st ` v ) = ( P - ( 2 x. u ) ) )
63 62 ad2antll 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( 1st ` v ) = ( P - ( 2 x. u ) ) )
64 63 oveq2d 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( P - ( 1st ` v ) ) = ( P - ( P - ( 2 x. u ) ) ) )
65 14 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. NN )
66 65 nncnd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. CC )
67 66 adantrr 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> P e. CC )
68 21 zcnd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) e. CC )
69 68 adantrr 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( 2 x. u ) e. CC )
70 67 69 nncand 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( P - ( P - ( 2 x. u ) ) ) = ( 2 x. u ) )
71 64 70 eqtrd 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( P - ( 1st ` v ) ) = ( 2 x. u ) )
72 71 oveq1d 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( ( P - ( 1st ` v ) ) / 2 ) = ( ( 2 x. u ) / 2 ) )
73 19 zcnd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u e. CC )
74 73 adantrr 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> u e. CC )
75 2cnd 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> 2 e. CC )
76 2ne0 
 |-  2 =/= 0
77 76 a1i 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> 2 =/= 0 )
78 74 75 77 divcan3d 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( ( 2 x. u ) / 2 ) = u )
79 72 78 eqtrd 
 |-  ( ( ph /\ ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) ) -> ( ( P - ( 1st ` v ) ) / 2 ) = u )
80 79 ralrimivva 
 |-  ( ph -> A. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) A. v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ( ( P - ( 1st ` v ) ) / 2 ) = u )
81 invdisj 
 |-  ( A. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) A. v e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ( ( P - ( 1st ` v ) ) / 2 ) = u -> Disj_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } )
82 80 81 syl 
 |-  ( ph -> Disj_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } )
83 11 59 82 hashiun 
 |-  ( ph -> ( # ` U_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) = sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( # ` { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) )
84 iunrab 
 |-  U_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } = { z e. S | E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) }
85 1 eldifsnbd 
 |-  ( ph -> P =/= 2 )
86 85 necomd 
 |-  ( ph -> 2 =/= P )
87 86 neneqd 
 |-  ( ph -> -. 2 = P )
88 87 ad2antrr 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> -. 2 = P )
89 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
90 17 89 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
91 1 eldifad 
 |-  ( ph -> P e. Prime )
92 91 ad2antrr 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. Prime )
93 dvdsprm 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( 2 || P <-> 2 = P ) )
94 90 92 93 sylancr 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 || P <-> 2 = P ) )
95 88 94 mtbird 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> -. 2 || P )
96 14 ad2antrr 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. NN )
97 96 nncnd 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. CC )
98 21 adantlr 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) e. ZZ )
99 98 zcnd 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) e. CC )
100 97 99 npcand 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) = P )
101 100 breq2d 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 || ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) <-> 2 || P ) )
102 95 101 mtbird 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> -. 2 || ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) )
103 18 adantl 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u e. ZZ )
104 dvdsmul1 
 |-  ( ( 2 e. ZZ /\ u e. ZZ ) -> 2 || ( 2 x. u ) )
105 17 103 104 sylancr 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 2 || ( 2 x. u ) )
106 17 a1i 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 2 e. ZZ )
107 96 nnzd 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. ZZ )
108 107 98 zsubcld 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - ( 2 x. u ) ) e. ZZ )
109 dvds2add 
 |-  ( ( 2 e. ZZ /\ ( P - ( 2 x. u ) ) e. ZZ /\ ( 2 x. u ) e. ZZ ) -> ( ( 2 || ( P - ( 2 x. u ) ) /\ 2 || ( 2 x. u ) ) -> 2 || ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) ) )
110 106 108 98 109 syl3anc 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 || ( P - ( 2 x. u ) ) /\ 2 || ( 2 x. u ) ) -> 2 || ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) ) )
111 105 110 mpan2d 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 || ( P - ( 2 x. u ) ) -> 2 || ( ( P - ( 2 x. u ) ) + ( 2 x. u ) ) ) )
112 102 111 mtod 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> -. 2 || ( P - ( 2 x. u ) ) )
113 breq2 
 |-  ( ( 1st ` z ) = ( P - ( 2 x. u ) ) -> ( 2 || ( 1st ` z ) <-> 2 || ( P - ( 2 x. u ) ) ) )
114 113 notbid 
 |-  ( ( 1st ` z ) = ( P - ( 2 x. u ) ) -> ( -. 2 || ( 1st ` z ) <-> -. 2 || ( P - ( 2 x. u ) ) ) )
115 112 114 syl5ibrcom 
 |-  ( ( ( ph /\ z e. S ) /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 1st ` z ) = ( P - ( 2 x. u ) ) -> -. 2 || ( 1st ` z ) ) )
116 115 rexlimdva 
 |-  ( ( ph /\ z e. S ) -> ( E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) -> -. 2 || ( 1st ` z ) ) )
117 simpr 
 |-  ( ( ph /\ z e. S ) -> z e. S )
118 32 117 sselid 
 |-  ( ( ph /\ z e. S ) -> z e. ( ( 1 ... M ) X. ( 1 ... N ) ) )
119 xp1st 
 |-  ( z e. ( ( 1 ... M ) X. ( 1 ... N ) ) -> ( 1st ` z ) e. ( 1 ... M ) )
120 118 119 syl 
 |-  ( ( ph /\ z e. S ) -> ( 1st ` z ) e. ( 1 ... M ) )
121 elfzelz 
 |-  ( ( 1st ` z ) e. ( 1 ... M ) -> ( 1st ` z ) e. ZZ )
122 odd2np1 
 |-  ( ( 1st ` z ) e. ZZ -> ( -. 2 || ( 1st ` z ) <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) )
123 120 121 122 3syl 
 |-  ( ( ph /\ z e. S ) -> ( -. 2 || ( 1st ` z ) <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) )
124 1 4 gausslemma2dlem0b 
 |-  ( ph -> M e. NN )
125 124 nnred 
 |-  ( ph -> M e. RR )
126 125 ad2antrr 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> M e. RR )
127 126 rehalfcld 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M / 2 ) e. RR )
128 127 flcld 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( |_ ` ( M / 2 ) ) e. ZZ )
129 128 peano2zd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( |_ ` ( M / 2 ) ) + 1 ) e. ZZ )
130 124 ad2antrr 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> M e. NN )
131 130 nnzd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> M e. ZZ )
132 simprl 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> n e. ZZ )
133 131 132 zsubcld 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M - n ) e. ZZ )
134 reflcl 
 |-  ( ( M / 2 ) e. RR -> ( |_ ` ( M / 2 ) ) e. RR )
135 127 134 syl 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( |_ ` ( M / 2 ) ) e. RR )
136 133 zred 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M - n ) e. RR )
137 flle 
 |-  ( ( M / 2 ) e. RR -> ( |_ ` ( M / 2 ) ) <_ ( M / 2 ) )
138 127 137 syl 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( |_ ` ( M / 2 ) ) <_ ( M / 2 ) )
139 zre 
 |-  ( n e. ZZ -> n e. RR )
140 139 ad2antrl 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> n e. RR )
141 simprr 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) + 1 ) = ( 1st ` z ) )
142 120 adantr 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 1st ` z ) e. ( 1 ... M ) )
143 141 142 eqeltrd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) + 1 ) e. ( 1 ... M ) )
144 elfzle2 
 |-  ( ( ( 2 x. n ) + 1 ) e. ( 1 ... M ) -> ( ( 2 x. n ) + 1 ) <_ M )
145 143 144 syl 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) + 1 ) <_ M )
146 zmulcl 
 |-  ( ( 2 e. ZZ /\ n e. ZZ ) -> ( 2 x. n ) e. ZZ )
147 17 132 146 sylancr 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. n ) e. ZZ )
148 147 131 zltp1led 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) < M <-> ( ( 2 x. n ) + 1 ) <_ M ) )
149 145 148 mpbird 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. n ) < M )
150 2re 
 |-  2 e. RR
151 150 a1i 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 2 e. RR )
152 2pos 
 |-  0 < 2
153 152 a1i 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 0 < 2 )
154 ltmuldiv2 
 |-  ( ( n e. RR /\ M e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. n ) < M <-> n < ( M / 2 ) ) )
155 140 126 151 153 154 syl112anc 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) < M <-> n < ( M / 2 ) ) )
156 149 155 mpbid 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> n < ( M / 2 ) )
157 127 recnd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M / 2 ) e. CC )
158 124 nncnd 
 |-  ( ph -> M e. CC )
159 158 ad2antrr 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> M e. CC )
160 159 2halvesd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( M / 2 ) + ( M / 2 ) ) = M )
161 157 157 160 mvlraddd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M / 2 ) = ( M - ( M / 2 ) ) )
162 156 161 breqtrd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> n < ( M - ( M / 2 ) ) )
163 140 126 127 162 ltsub13d 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M / 2 ) < ( M - n ) )
164 135 127 136 138 163 lelttrd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( |_ ` ( M / 2 ) ) < ( M - n ) )
165 128 133 zltp1led 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( |_ ` ( M / 2 ) ) < ( M - n ) <-> ( ( |_ ` ( M / 2 ) ) + 1 ) <_ ( M - n ) ) )
166 164 165 mpbid 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( |_ ` ( M / 2 ) ) + 1 ) <_ ( M - n ) )
167 2t0e0 
 |-  ( 2 x. 0 ) = 0
168 2cn 
 |-  2 e. CC
169 zcn 
 |-  ( n e. ZZ -> n e. CC )
170 169 ad2antrl 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> n e. CC )
171 mulcl 
 |-  ( ( 2 e. CC /\ n e. CC ) -> ( 2 x. n ) e. CC )
172 168 170 171 sylancr 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. n ) e. CC )
173 pncan 
 |-  ( ( ( 2 x. n ) e. CC /\ 1 e. CC ) -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
174 172 47 173 sylancl 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
175 elfznn 
 |-  ( ( ( 2 x. n ) + 1 ) e. ( 1 ... M ) -> ( ( 2 x. n ) + 1 ) e. NN )
176 nnm1nn0 
 |-  ( ( ( 2 x. n ) + 1 ) e. NN -> ( ( ( 2 x. n ) + 1 ) - 1 ) e. NN0 )
177 143 175 176 3syl 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( ( 2 x. n ) + 1 ) - 1 ) e. NN0 )
178 174 177 eqeltrrd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. n ) e. NN0 )
179 178 nn0ge0d 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 0 <_ ( 2 x. n ) )
180 167 179 eqbrtrid 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. 0 ) <_ ( 2 x. n ) )
181 0red 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 0 e. RR )
182 lemul2 
 |-  ( ( 0 e. RR /\ n e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 0 <_ n <-> ( 2 x. 0 ) <_ ( 2 x. n ) ) )
183 181 140 151 153 182 syl112anc 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 0 <_ n <-> ( 2 x. 0 ) <_ ( 2 x. n ) ) )
184 180 183 mpbird 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 0 <_ n )
185 126 140 subge02d 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 0 <_ n <-> ( M - n ) <_ M ) )
186 184 185 mpbid 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M - n ) <_ M )
187 129 131 133 166 186 elfzd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( M - n ) e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) )
188 91 ad2antrr 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> P e. Prime )
189 prmnn 
 |-  ( P e. Prime -> P e. NN )
190 188 189 syl 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> P e. NN )
191 190 nncnd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> P e. CC )
192 peano2cn 
 |-  ( ( 2 x. n ) e. CC -> ( ( 2 x. n ) + 1 ) e. CC )
193 172 192 syl 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. n ) + 1 ) e. CC )
194 191 193 nncand 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( P - ( P - ( ( 2 x. n ) + 1 ) ) ) = ( ( 2 x. n ) + 1 ) )
195 1cnd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 1 e. CC )
196 191 172 195 sub32d 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( P - ( 2 x. n ) ) - 1 ) = ( ( P - 1 ) - ( 2 x. n ) ) )
197 191 172 195 subsub4d 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( P - ( 2 x. n ) ) - 1 ) = ( P - ( ( 2 x. n ) + 1 ) ) )
198 2cnd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 2 e. CC )
199 198 159 170 subdid 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. ( M - n ) ) = ( ( 2 x. M ) - ( 2 x. n ) ) )
200 4 oveq2i 
 |-  ( 2 x. M ) = ( 2 x. ( ( P - 1 ) / 2 ) )
201 14 nnzd 
 |-  ( ph -> P e. ZZ )
202 201 ad2antrr 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> P e. ZZ )
203 peano2zm 
 |-  ( P e. ZZ -> ( P - 1 ) e. ZZ )
204 202 203 syl 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( P - 1 ) e. ZZ )
205 204 zcnd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( P - 1 ) e. CC )
206 76 a1i 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> 2 =/= 0 )
207 205 198 206 divcan2d 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. ( ( P - 1 ) / 2 ) ) = ( P - 1 ) )
208 200 207 eqtrid 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 2 x. M ) = ( P - 1 ) )
209 208 oveq1d 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( 2 x. M ) - ( 2 x. n ) ) = ( ( P - 1 ) - ( 2 x. n ) ) )
210 199 209 eqtr2d 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( ( P - 1 ) - ( 2 x. n ) ) = ( 2 x. ( M - n ) ) )
211 196 197 210 3eqtr3d 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( P - ( ( 2 x. n ) + 1 ) ) = ( 2 x. ( M - n ) ) )
212 211 oveq2d 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( P - ( P - ( ( 2 x. n ) + 1 ) ) ) = ( P - ( 2 x. ( M - n ) ) ) )
213 194 212 141 3eqtr3rd 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> ( 1st ` z ) = ( P - ( 2 x. ( M - n ) ) ) )
214 oveq2 
 |-  ( u = ( M - n ) -> ( 2 x. u ) = ( 2 x. ( M - n ) ) )
215 214 oveq2d 
 |-  ( u = ( M - n ) -> ( P - ( 2 x. u ) ) = ( P - ( 2 x. ( M - n ) ) ) )
216 215 rspceeqv 
 |-  ( ( ( M - n ) e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) /\ ( 1st ` z ) = ( P - ( 2 x. ( M - n ) ) ) ) -> E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) )
217 187 213 216 syl2anc 
 |-  ( ( ( ph /\ z e. S ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) ) ) -> E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) )
218 217 rexlimdvaa 
 |-  ( ( ph /\ z e. S ) -> ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = ( 1st ` z ) -> E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) ) )
219 123 218 sylbid 
 |-  ( ( ph /\ z e. S ) -> ( -. 2 || ( 1st ` z ) -> E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) ) )
220 116 219 impbid 
 |-  ( ( ph /\ z e. S ) -> ( E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) <-> -. 2 || ( 1st ` z ) ) )
221 220 rabbidva 
 |-  ( ph -> { z e. S | E. u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 1st ` z ) = ( P - ( 2 x. u ) ) } = { z e. S | -. 2 || ( 1st ` z ) } )
222 84 221 eqtrid 
 |-  ( ph -> U_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } = { z e. S | -. 2 || ( 1st ` z ) } )
223 222 fveq2d 
 |-  ( ph -> ( # ` U_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) = ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) )
224 6 relopabiv 
 |-  Rel S
225 relss 
 |-  ( { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } C_ S -> ( Rel S -> Rel { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) )
226 57 224 225 mp2 
 |-  Rel { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) }
227 relxp 
 |-  Rel ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
228 6 eleq2i 
 |-  ( <. x , y >. e. S <-> <. x , y >. e. { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } )
229 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } <-> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) )
230 228 229 bitri 
 |-  ( <. x , y >. e. S <-> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) )
231 anass 
 |-  ( ( ( y e. NN /\ y <_ N ) /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) <-> ( y e. NN /\ ( y <_ N /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) ) )
232 24 peano2zd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) e. ZZ )
233 232 zred 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) e. RR )
234 233 adantr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) e. RR )
235 13 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> Q e. RR )
236 nnre 
 |-  ( y e. NN -> y e. RR )
237 236 adantl 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> y e. RR )
238 lesub 
 |-  ( ( ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) e. RR /\ Q e. RR /\ y e. RR ) -> ( ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) <_ ( Q - y ) <-> y <_ ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) ) )
239 234 235 237 238 syl3anc 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) <_ ( Q - y ) <-> y <_ ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) ) )
240 13 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> Q e. RR )
241 240 recnd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> Q e. CC )
242 66 241 mulcomd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P x. Q ) = ( Q x. P ) )
243 68 241 mulcomd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. u ) x. Q ) = ( Q x. ( 2 x. u ) ) )
244 65 nnne0d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P =/= 0 )
245 241 66 244 divcan1d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / P ) x. P ) = Q )
246 245 oveq1d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( Q / P ) x. P ) x. ( 2 x. u ) ) = ( Q x. ( 2 x. u ) ) )
247 16 recnd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q / P ) e. CC )
248 247 66 68 mul32d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( Q / P ) x. P ) x. ( 2 x. u ) ) = ( ( ( Q / P ) x. ( 2 x. u ) ) x. P ) )
249 243 246 248 3eqtr2d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. u ) x. Q ) = ( ( ( Q / P ) x. ( 2 x. u ) ) x. P ) )
250 242 249 oveq12d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P x. Q ) - ( ( 2 x. u ) x. Q ) ) = ( ( Q x. P ) - ( ( ( Q / P ) x. ( 2 x. u ) ) x. P ) ) )
251 66 68 241 subdird 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) x. Q ) = ( ( P x. Q ) - ( ( 2 x. u ) x. Q ) ) )
252 23 recnd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / P ) x. ( 2 x. u ) ) e. CC )
253 241 252 66 subdird 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) = ( ( Q x. P ) - ( ( ( Q / P ) x. ( 2 x. u ) ) x. P ) ) )
254 250 251 253 3eqtr4d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) x. Q ) = ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) )
255 254 adantr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( P - ( 2 x. u ) ) x. Q ) = ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) )
256 255 breq2d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) <-> ( y x. P ) < ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) ) )
257 23 adantr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( Q / P ) x. ( 2 x. u ) ) e. RR )
258 235 257 resubcld 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) e. RR )
259 65 adantr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> P e. NN )
260 259 nnred 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> P e. RR )
261 259 nngt0d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> 0 < P )
262 ltmul1 
 |-  ( ( y e. RR /\ ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( y < ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) <-> ( y x. P ) < ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) ) )
263 237 258 260 261 262 syl112anc 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( y < ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) <-> ( y x. P ) < ( ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) x. P ) ) )
264 ltsub13 
 |-  ( ( y e. RR /\ Q e. RR /\ ( ( Q / P ) x. ( 2 x. u ) ) e. RR ) -> ( y < ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) <-> ( ( Q / P ) x. ( 2 x. u ) ) < ( Q - y ) ) )
265 237 235 257 264 syl3anc 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( y < ( Q - ( ( Q / P ) x. ( 2 x. u ) ) ) <-> ( ( Q / P ) x. ( 2 x. u ) ) < ( Q - y ) ) )
266 256 263 265 3bitr2d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) <-> ( ( Q / P ) x. ( 2 x. u ) ) < ( Q - y ) ) )
267 12 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> Q e. NN )
268 267 nnzd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> Q e. ZZ )
269 nnz 
 |-  ( y e. NN -> y e. ZZ )
270 zsubcl 
 |-  ( ( Q e. ZZ /\ y e. ZZ ) -> ( Q - y ) e. ZZ )
271 268 269 270 syl2an 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( Q - y ) e. ZZ )
272 fllt 
 |-  ( ( ( ( Q / P ) x. ( 2 x. u ) ) e. RR /\ ( Q - y ) e. ZZ ) -> ( ( ( Q / P ) x. ( 2 x. u ) ) < ( Q - y ) <-> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < ( Q - y ) ) )
273 257 271 272 syl2anc 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( ( Q / P ) x. ( 2 x. u ) ) < ( Q - y ) <-> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < ( Q - y ) ) )
274 24 adantr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ )
275 274 271 zltp1led 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < ( Q - y ) <-> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) <_ ( Q - y ) ) )
276 266 273 275 3bitrd 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) <-> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) <_ ( Q - y ) ) )
277 5 oveq2i 
 |-  ( 2 x. N ) = ( 2 x. ( ( Q - 1 ) / 2 ) )
278 peano2rem 
 |-  ( Q e. RR -> ( Q - 1 ) e. RR )
279 240 278 syl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q - 1 ) e. RR )
280 279 recnd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q - 1 ) e. CC )
281 2cnd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 2 e. CC )
282 76 a1i 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 2 =/= 0 )
283 280 281 282 divcan2d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. ( ( Q - 1 ) / 2 ) ) = ( Q - 1 ) )
284 277 283 eqtrid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) = ( Q - 1 ) )
285 284 oveq1d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( ( Q - 1 ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
286 1cnd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 1 e. CC )
287 24 zcnd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. CC )
288 241 286 287 sub32d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q - 1 ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( ( Q - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) - 1 ) )
289 241 287 286 subsub4d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) - 1 ) = ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) )
290 285 288 289 3eqtrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) )
291 290 adantr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) )
292 291 breq2d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <-> y <_ ( Q - ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + 1 ) ) ) )
293 239 276 292 3bitr4d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) <-> y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
294 293 anbi2d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y <_ N /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) <-> ( y <_ N /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
295 2nn 
 |-  2 e. NN
296 2 5 gausslemma2dlem0b 
 |-  ( ph -> N e. NN )
297 nnmulcl 
 |-  ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
298 295 296 297 sylancr 
 |-  ( ph -> ( 2 x. N ) e. NN )
299 298 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) e. NN )
300 299 nnred 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) e. RR )
301 296 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N e. NN )
302 301 nnred 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N e. RR )
303 24 zred 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. RR )
304 296 nncnd 
 |-  ( ph -> N e. CC )
305 304 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N e. CC )
306 305 2timesd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) = ( N + N ) )
307 305 305 306 mvrladdd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - N ) = N )
308 240 rehalfcld 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q / 2 ) e. RR )
309 240 ltm1d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q - 1 ) < Q )
310 150 a1i 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 2 e. RR )
311 152 a1i 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 0 < 2 )
312 ltdiv1 
 |-  ( ( ( Q - 1 ) e. RR /\ Q e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( Q - 1 ) < Q <-> ( ( Q - 1 ) / 2 ) < ( Q / 2 ) ) )
313 279 240 310 311 312 syl112anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q - 1 ) < Q <-> ( ( Q - 1 ) / 2 ) < ( Q / 2 ) ) )
314 309 313 mpbid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q - 1 ) / 2 ) < ( Q / 2 ) )
315 5 314 eqbrtrid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N < ( Q / 2 ) )
316 302 308 315 ltled 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N <_ ( Q / 2 ) )
317 241 281 66 282 div32d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / 2 ) x. P ) = ( Q x. ( P / 2 ) ) )
318 125 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> M e. RR )
319 318 rehalfcld 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( M / 2 ) e. RR )
320 peano2re 
 |-  ( ( |_ ` ( M / 2 ) ) e. RR -> ( ( |_ ` ( M / 2 ) ) + 1 ) e. RR )
321 319 134 320 3syl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( |_ ` ( M / 2 ) ) + 1 ) e. RR )
322 19 zred 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u e. RR )
323 flltp1 
 |-  ( ( M / 2 ) e. RR -> ( M / 2 ) < ( ( |_ ` ( M / 2 ) ) + 1 ) )
324 319 323 syl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( M / 2 ) < ( ( |_ ` ( M / 2 ) ) + 1 ) )
325 elfzle1 
 |-  ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) -> ( ( |_ ` ( M / 2 ) ) + 1 ) <_ u )
326 325 adantl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( |_ ` ( M / 2 ) ) + 1 ) <_ u )
327 319 321 322 324 326 ltletrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( M / 2 ) < u )
328 ltdivmul 
 |-  ( ( M e. RR /\ u e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( M / 2 ) < u <-> M < ( 2 x. u ) ) )
329 318 322 310 311 328 syl112anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( M / 2 ) < u <-> M < ( 2 x. u ) ) )
330 327 329 mpbid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> M < ( 2 x. u ) )
331 4 330 eqbrtrrid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - 1 ) / 2 ) < ( 2 x. u ) )
332 65 nnred 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. RR )
333 peano2rem 
 |-  ( P e. RR -> ( P - 1 ) e. RR )
334 332 333 syl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - 1 ) e. RR )
335 ltdivmul 
 |-  ( ( ( P - 1 ) e. RR /\ ( 2 x. u ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( P - 1 ) / 2 ) < ( 2 x. u ) <-> ( P - 1 ) < ( 2 x. ( 2 x. u ) ) ) )
336 334 22 310 311 335 syl112anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( P - 1 ) / 2 ) < ( 2 x. u ) <-> ( P - 1 ) < ( 2 x. ( 2 x. u ) ) ) )
337 331 336 mpbid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - 1 ) < ( 2 x. ( 2 x. u ) ) )
338 201 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. ZZ )
339 zmulcl 
 |-  ( ( 2 e. ZZ /\ ( 2 x. u ) e. ZZ ) -> ( 2 x. ( 2 x. u ) ) e. ZZ )
340 17 21 339 sylancr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. ( 2 x. u ) ) e. ZZ )
341 zlem1lt 
 |-  ( ( P e. ZZ /\ ( 2 x. ( 2 x. u ) ) e. ZZ ) -> ( P <_ ( 2 x. ( 2 x. u ) ) <-> ( P - 1 ) < ( 2 x. ( 2 x. u ) ) ) )
342 338 340 341 syl2anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P <_ ( 2 x. ( 2 x. u ) ) <-> ( P - 1 ) < ( 2 x. ( 2 x. u ) ) ) )
343 337 342 mpbird 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P <_ ( 2 x. ( 2 x. u ) ) )
344 ledivmul 
 |-  ( ( P e. RR /\ ( 2 x. u ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( P / 2 ) <_ ( 2 x. u ) <-> P <_ ( 2 x. ( 2 x. u ) ) ) )
345 332 22 310 311 344 syl112anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P / 2 ) <_ ( 2 x. u ) <-> P <_ ( 2 x. ( 2 x. u ) ) ) )
346 343 345 mpbird 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P / 2 ) <_ ( 2 x. u ) )
347 332 rehalfcld 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P / 2 ) e. RR )
348 267 nngt0d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 0 < Q )
349 lemul2 
 |-  ( ( ( P / 2 ) e. RR /\ ( 2 x. u ) e. RR /\ ( Q e. RR /\ 0 < Q ) ) -> ( ( P / 2 ) <_ ( 2 x. u ) <-> ( Q x. ( P / 2 ) ) <_ ( Q x. ( 2 x. u ) ) ) )
350 347 22 240 348 349 syl112anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P / 2 ) <_ ( 2 x. u ) <-> ( Q x. ( P / 2 ) ) <_ ( Q x. ( 2 x. u ) ) ) )
351 346 350 mpbid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q x. ( P / 2 ) ) <_ ( Q x. ( 2 x. u ) ) )
352 317 351 eqbrtrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / 2 ) x. P ) <_ ( Q x. ( 2 x. u ) ) )
353 240 22 remulcld 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q x. ( 2 x. u ) ) e. RR )
354 65 nngt0d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 0 < P )
355 lemuldiv 
 |-  ( ( ( Q / 2 ) e. RR /\ ( Q x. ( 2 x. u ) ) e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( ( ( Q / 2 ) x. P ) <_ ( Q x. ( 2 x. u ) ) <-> ( Q / 2 ) <_ ( ( Q x. ( 2 x. u ) ) / P ) ) )
356 308 353 332 354 355 syl112anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( Q / 2 ) x. P ) <_ ( Q x. ( 2 x. u ) ) <-> ( Q / 2 ) <_ ( ( Q x. ( 2 x. u ) ) / P ) ) )
357 352 356 mpbid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q / 2 ) <_ ( ( Q x. ( 2 x. u ) ) / P ) )
358 241 68 66 244 div23d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q x. ( 2 x. u ) ) / P ) = ( ( Q / P ) x. ( 2 x. u ) ) )
359 357 358 breqtrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q / 2 ) <_ ( ( Q / P ) x. ( 2 x. u ) ) )
360 302 308 23 316 359 letrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N <_ ( ( Q / P ) x. ( 2 x. u ) ) )
361 296 nnzd 
 |-  ( ph -> N e. ZZ )
362 361 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N e. ZZ )
363 flge 
 |-  ( ( ( ( Q / P ) x. ( 2 x. u ) ) e. RR /\ N e. ZZ ) -> ( N <_ ( ( Q / P ) x. ( 2 x. u ) ) <-> N <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
364 23 362 363 syl2anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( N <_ ( ( Q / P ) x. ( 2 x. u ) ) <-> N <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
365 360 364 mpbid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> N <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) )
366 307 365 eqbrtrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - N ) <_ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) )
367 300 302 303 366 subled 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <_ N )
368 367 adantr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <_ N )
369 299 nnzd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) e. ZZ )
370 369 24 zsubcld 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. ZZ )
371 370 adantr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. ZZ )
372 371 zred 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. RR )
373 296 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> N e. NN )
374 373 nnred 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> N e. RR )
375 letr 
 |-  ( ( y e. RR /\ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. RR /\ N e. RR ) -> ( ( y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) /\ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <_ N ) -> y <_ N ) )
376 237 372 374 375 syl3anc 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) /\ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <_ N ) -> y <_ N ) )
377 368 376 mpan2d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) -> y <_ N ) )
378 377 pm4.71rd 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <-> ( y <_ N /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
379 294 378 bitr4d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ y e. NN ) -> ( ( y <_ N /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) <-> y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
380 379 pm5.32da 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( y e. NN /\ ( y <_ N /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) ) <-> ( y e. NN /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
381 380 adantr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( y e. NN /\ ( y <_ N /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) ) <-> ( y e. NN /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
382 231 381 bitrid 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( ( y e. NN /\ y <_ N ) /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) <-> ( y e. NN /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
383 simpr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> x = ( P - ( 2 x. u ) ) )
384 338 21 zsubcld 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - ( 2 x. u ) ) e. ZZ )
385 elfzle2 
 |-  ( u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) -> u <_ M )
386 385 adantl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u <_ M )
387 386 4 breqtrdi 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> u <_ ( ( P - 1 ) / 2 ) )
388 lemuldiv2 
 |-  ( ( u e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. u ) <_ ( P - 1 ) <-> u <_ ( ( P - 1 ) / 2 ) ) )
389 322 334 310 311 388 syl112anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. u ) <_ ( P - 1 ) <-> u <_ ( ( P - 1 ) / 2 ) ) )
390 387 389 mpbird 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) <_ ( P - 1 ) )
391 332 ltm1d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - 1 ) < P )
392 22 334 332 390 391 lelttrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. u ) < P )
393 22 332 posdifd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. u ) < P <-> 0 < ( P - ( 2 x. u ) ) ) )
394 392 393 mpbid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> 0 < ( P - ( 2 x. u ) ) )
395 elnnz 
 |-  ( ( P - ( 2 x. u ) ) e. NN <-> ( ( P - ( 2 x. u ) ) e. ZZ /\ 0 < ( P - ( 2 x. u ) ) ) )
396 384 394 395 sylanbrc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - ( 2 x. u ) ) e. NN )
397 66 68 286 sub32d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) - 1 ) = ( ( P - 1 ) - ( 2 x. u ) ) )
398 158 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> M e. CC )
399 4 4 oveq12i 
 |-  ( M + M ) = ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) )
400 65 nnzd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> P e. ZZ )
401 400 203 syl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - 1 ) e. ZZ )
402 401 zcnd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - 1 ) e. CC )
403 402 2halvesd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) ) = ( P - 1 ) )
404 399 403 eqtrid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( M + M ) = ( P - 1 ) )
405 398 398 404 mvlladdcd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - 1 ) - M ) = M )
406 405 330 eqbrtrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - 1 ) - M ) < ( 2 x. u ) )
407 334 318 22 406 ltsub23d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - 1 ) - ( 2 x. u ) ) < M )
408 397 407 eqbrtrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) - 1 ) < M )
409 124 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> M e. NN )
410 409 nnzd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> M e. ZZ )
411 zlem1lt 
 |-  ( ( ( P - ( 2 x. u ) ) e. ZZ /\ M e. ZZ ) -> ( ( P - ( 2 x. u ) ) <_ M <-> ( ( P - ( 2 x. u ) ) - 1 ) < M ) )
412 384 410 411 syl2anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) <_ M <-> ( ( P - ( 2 x. u ) ) - 1 ) < M ) )
413 408 412 mpbird 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - ( 2 x. u ) ) <_ M )
414 fznn 
 |-  ( M e. ZZ -> ( ( P - ( 2 x. u ) ) e. ( 1 ... M ) <-> ( ( P - ( 2 x. u ) ) e. NN /\ ( P - ( 2 x. u ) ) <_ M ) ) )
415 410 414 syl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( P - ( 2 x. u ) ) e. ( 1 ... M ) <-> ( ( P - ( 2 x. u ) ) e. NN /\ ( P - ( 2 x. u ) ) <_ M ) ) )
416 396 413 415 mpbir2and 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( P - ( 2 x. u ) ) e. ( 1 ... M ) )
417 416 adantr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( P - ( 2 x. u ) ) e. ( 1 ... M ) )
418 383 417 eqeltrd 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> x e. ( 1 ... M ) )
419 418 biantrurd 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( y e. ( 1 ... N ) <-> ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) )
420 361 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> N e. ZZ )
421 fznn 
 |-  ( N e. ZZ -> ( y e. ( 1 ... N ) <-> ( y e. NN /\ y <_ N ) ) )
422 420 421 syl 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( y e. ( 1 ... N ) <-> ( y e. NN /\ y <_ N ) ) )
423 419 422 bitr3d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) <-> ( y e. NN /\ y <_ N ) ) )
424 383 oveq1d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( x x. Q ) = ( ( P - ( 2 x. u ) ) x. Q ) )
425 424 breq2d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( y x. P ) < ( x x. Q ) <-> ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) )
426 423 425 anbi12d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) <-> ( ( y e. NN /\ y <_ N ) /\ ( y x. P ) < ( ( P - ( 2 x. u ) ) x. Q ) ) ) )
427 370 adantr 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. ZZ )
428 fznn 
 |-  ( ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. ZZ -> ( y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) <-> ( y e. NN /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
429 427 428 syl 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) <-> ( y e. NN /\ y <_ ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
430 382 426 429 3bitr4d 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) <-> y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
431 230 430 bitrid 
 |-  ( ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) /\ x = ( P - ( 2 x. u ) ) ) -> ( <. x , y >. e. S <-> y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
432 431 pm5.32da 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( x = ( P - ( 2 x. u ) ) /\ <. x , y >. e. S ) <-> ( x = ( P - ( 2 x. u ) ) /\ y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ) )
433 vex 
 |-  x e. _V
434 vex 
 |-  y e. _V
435 433 434 op1std 
 |-  ( z = <. x , y >. -> ( 1st ` z ) = x )
436 435 eqeq1d 
 |-  ( z = <. x , y >. -> ( ( 1st ` z ) = ( P - ( 2 x. u ) ) <-> x = ( P - ( 2 x. u ) ) ) )
437 436 elrab 
 |-  ( <. x , y >. e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } <-> ( <. x , y >. e. S /\ x = ( P - ( 2 x. u ) ) ) )
438 437 biancomi 
 |-  ( <. x , y >. e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } <-> ( x = ( P - ( 2 x. u ) ) /\ <. x , y >. e. S ) )
439 opelxp 
 |-  ( <. x , y >. e. ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) <-> ( x e. { ( P - ( 2 x. u ) ) } /\ y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
440 velsn 
 |-  ( x e. { ( P - ( 2 x. u ) ) } <-> x = ( P - ( 2 x. u ) ) )
441 439 440 bianbi 
 |-  ( <. x , y >. e. ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) <-> ( x = ( P - ( 2 x. u ) ) /\ y e. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
442 432 438 441 3bitr4g 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( <. x , y >. e. { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } <-> <. x , y >. e. ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ) )
443 226 227 442 eqrelrdv 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } = ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
444 443 fveq2d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( # ` { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) = ( # ` ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ) )
445 fzfid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) e. Fin )
446 xpsnen2g 
 |-  ( ( ( P - ( 2 x. u ) ) e. ZZ /\ ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) e. Fin ) -> ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ~~ ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
447 384 445 446 syl2anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ~~ ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
448 hasheni 
 |-  ( ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ~~ ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) -> ( # ` ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ) = ( # ` ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
449 447 448 syl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( # ` ( { ( P - ( 2 x. u ) ) } X. ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) ) = ( # ` ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) )
450 ltmul2 
 |-  ( ( ( 2 x. u ) e. RR /\ P e. RR /\ ( Q e. RR /\ 0 < Q ) ) -> ( ( 2 x. u ) < P <-> ( Q x. ( 2 x. u ) ) < ( Q x. P ) ) )
451 22 332 240 348 450 syl112anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( 2 x. u ) < P <-> ( Q x. ( 2 x. u ) ) < ( Q x. P ) ) )
452 392 451 mpbid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( Q x. ( 2 x. u ) ) < ( Q x. P ) )
453 ltdivmul2 
 |-  ( ( ( Q x. ( 2 x. u ) ) e. RR /\ Q e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( ( ( Q x. ( 2 x. u ) ) / P ) < Q <-> ( Q x. ( 2 x. u ) ) < ( Q x. P ) ) )
454 353 240 332 354 453 syl112anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( Q x. ( 2 x. u ) ) / P ) < Q <-> ( Q x. ( 2 x. u ) ) < ( Q x. P ) ) )
455 452 454 mpbird 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q x. ( 2 x. u ) ) / P ) < Q )
456 358 455 eqbrtrrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( Q / P ) x. ( 2 x. u ) ) < Q )
457 fllt 
 |-  ( ( ( ( Q / P ) x. ( 2 x. u ) ) e. RR /\ Q e. ZZ ) -> ( ( ( Q / P ) x. ( 2 x. u ) ) < Q <-> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < Q ) )
458 23 268 457 syl2anc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( ( Q / P ) x. ( 2 x. u ) ) < Q <-> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < Q ) )
459 456 458 mpbid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < Q )
460 24 268 zltlem1d 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) < Q <-> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) <_ ( Q - 1 ) ) )
461 459 460 mpbid 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) <_ ( Q - 1 ) )
462 461 284 breqtrrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) <_ ( 2 x. N ) )
463 eluz2 
 |-  ( ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) <-> ( ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ /\ ( 2 x. N ) e. ZZ /\ ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) <_ ( 2 x. N ) ) )
464 24 369 462 463 syl3anbrc 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
465 uznn0sub 
 |-  ( ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) -> ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. NN0 )
466 hashfz1 
 |-  ( ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) e. NN0 -> ( # ` ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) = ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
467 464 465 466 3syl 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( # ` ( 1 ... ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) ) = ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
468 444 449 467 3eqtrd 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( # ` { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) = ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
469 468 sumeq2dv 
 |-  ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( # ` { z e. S | ( 1st ` z ) = ( P - ( 2 x. u ) ) } ) = sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
470 83 223 469 3eqtr3rd 
 |-  ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) )
471 298 nncnd 
 |-  ( ph -> ( 2 x. N ) e. CC )
472 471 adantr 
 |-  ( ( ph /\ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) -> ( 2 x. N ) e. CC )
473 11 472 287 fsumsub 
 |-  ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( ( 2 x. N ) - ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) - sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
474 470 473 eqtr3d 
 |-  ( ph -> ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) = ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) - sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) )
475 474 oveq2d 
 |-  ( ph -> ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) - sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) )
476 25 zcnd 
 |-  ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. CC )
477 11 369 fsumzcl 
 |-  ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) e. ZZ )
478 477 zcnd 
 |-  ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) e. CC )
479 476 478 pncan3d 
 |-  ( ph -> ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) - sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) ) = sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) )
480 fsumconst 
 |-  ( ( ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) e. Fin /\ ( 2 x. N ) e. CC ) -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) = ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. ( 2 x. N ) ) )
481 11 471 480 syl2anc 
 |-  ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) = ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. ( 2 x. N ) ) )
482 hashcl 
 |-  ( ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) e. Fin -> ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) e. NN0 )
483 11 482 syl 
 |-  ( ph -> ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) e. NN0 )
484 483 nn0cnd 
 |-  ( ph -> ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) e. CC )
485 2cnd 
 |-  ( ph -> 2 e. CC )
486 484 485 304 mul12d 
 |-  ( ph -> ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. ( 2 x. N ) ) = ( 2 x. ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) )
487 481 486 eqtrd 
 |-  ( ph -> sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( 2 x. N ) = ( 2 x. ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) )
488 475 479 487 3eqtrd 
 |-  ( ph -> ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) = ( 2 x. ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) )
489 488 oveq2d 
 |-  ( ph -> ( -u 1 ^ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( -u 1 ^ ( 2 x. ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) ) )
490 17 a1i 
 |-  ( ph -> 2 e. ZZ )
491 483 nn0zd 
 |-  ( ph -> ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) e. ZZ )
492 491 361 zmulcld 
 |-  ( ph -> ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) e. ZZ )
493 expmulz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( 2 e. ZZ /\ ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) e. ZZ ) ) -> ( -u 1 ^ ( 2 x. ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) ) = ( ( -u 1 ^ 2 ) ^ ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) )
494 8 10 490 492 493 syl22anc 
 |-  ( ph -> ( -u 1 ^ ( 2 x. ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) ) = ( ( -u 1 ^ 2 ) ^ ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) )
495 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
496 495 oveq1i 
 |-  ( ( -u 1 ^ 2 ) ^ ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) = ( 1 ^ ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) )
497 1exp 
 |-  ( ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) e. ZZ -> ( 1 ^ ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) = 1 )
498 492 497 syl 
 |-  ( ph -> ( 1 ^ ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) = 1 )
499 496 498 eqtrid 
 |-  ( ph -> ( ( -u 1 ^ 2 ) ^ ( ( # ` ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ) x. N ) ) = 1 )
500 489 494 499 3eqtrd 
 |-  ( ph -> ( -u 1 ^ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = 1 )
501 44 55 500 3eqtr4d 
 |-  ( ph -> ( ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) x. ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( -u 1 ^ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
502 expaddz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) e. ZZ /\ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) e. ZZ ) ) -> ( -u 1 ^ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) x. ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
503 8 10 25 42 502 syl22anc 
 |-  ( ph -> ( -u 1 ^ ( sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) + ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) x. ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
504 501 503 eqtr2d 
 |-  ( ph -> ( ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) x. ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) = ( ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) x. ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) ) )
505 26 41 41 43 504 mulcan2ad 
 |-  ( ph -> ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = ( -u 1 ^ ( # ` { z e. S | -. 2 || ( 1st ` z ) } ) ) )