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