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