MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lgsquadlem2 Structured version   Unicode version

Theorem lgsquadlem2 21139
Description: Lemma for lgsquad 21141. Count the members of  S with even coordinates, and combine with lgsquadlem1 21138 to get the total count of lattice points in  S (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015.)
Hypotheses
Ref Expression
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
Ref Expression
lgsquadlem2  |-  ( ph  ->  ( Q  / L P )  =  (
-u 1 ^ ( # `
 S ) ) )
Distinct variable groups:    x, y, P    ph, x, y    y, M    x, N, y    x, Q, y    x, S    x, M    y, S

Proof of Theorem lgsquadlem2
Dummy variables  u  v  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lgseisen.1 . . 3  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
2 lgseisen.2 . . 3  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
3 lgseisen.3 . . 3  |-  ( ph  ->  P  =/=  Q )
41, 2, 3lgseisen 21137 . 2  |-  ( ph  ->  ( Q  / L P )  =  (
-u 1 ^ sum_ u  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) )
5 lgsquad.4 . . . . . 6  |-  M  =  ( ( P  - 
1 )  /  2
)
65oveq2i 6092 . . . . 5  |-  ( 1 ... M )  =  ( 1 ... (
( P  -  1 )  /  2 ) )
76sumeq1i 12492 . . . 4  |-  sum_ u  e.  ( 1 ... M
) ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) )  =  sum_ u  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )
8 oddprm 13189 . . . . . . . . . . . . 13  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
91, 8syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN )
105, 9syl5eqel 2520 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  NN )
1110nnred 10015 . . . . . . . . . 10  |-  ( ph  ->  M  e.  RR )
1211rehalfcld 10214 . . . . . . . . 9  |-  ( ph  ->  ( M  /  2
)  e.  RR )
1312flcld 11207 . . . . . . . 8  |-  ( ph  ->  ( |_ `  ( M  /  2 ) )  e.  ZZ )
1413zred 10375 . . . . . . 7  |-  ( ph  ->  ( |_ `  ( M  /  2 ) )  e.  RR )
1514ltp1d 9941 . . . . . 6  |-  ( ph  ->  ( |_ `  ( M  /  2 ) )  <  ( ( |_
`  ( M  / 
2 ) )  +  1 ) )
16 fzdisj 11078 . . . . . 6  |-  ( ( |_ `  ( M  /  2 ) )  <  ( ( |_
`  ( M  / 
2 ) )  +  1 )  ->  (
( 1 ... ( |_ `  ( M  / 
2 ) ) )  i^i  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M ) )  =  (/) )
1715, 16syl 16 . . . . 5  |-  ( ph  ->  ( ( 1 ... ( |_ `  ( M  /  2 ) ) )  i^i  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M ) )  =  (/) )
1810nnrpd 10647 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR+ )
1918rphalfcld 10660 . . . . . . . . . 10  |-  ( ph  ->  ( M  /  2
)  e.  RR+ )
2019rpge0d 10652 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( M  /  2 ) )
21 flge0nn0 11225 . . . . . . . . 9  |-  ( ( ( M  /  2
)  e.  RR  /\  0  <_  ( M  / 
2 ) )  -> 
( |_ `  ( M  /  2 ) )  e.  NN0 )
2212, 20, 21syl2anc 643 . . . . . . . 8  |-  ( ph  ->  ( |_ `  ( M  /  2 ) )  e.  NN0 )
2310nnnn0d 10274 . . . . . . . 8  |-  ( ph  ->  M  e.  NN0 )
24 rphalflt 10638 . . . . . . . . . . 11  |-  ( M  e.  RR+  ->  ( M  /  2 )  < 
M )
2518, 24syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( M  /  2
)  <  M )
2610nnzd 10374 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ZZ )
27 fllt 11215 . . . . . . . . . . 11  |-  ( ( ( M  /  2
)  e.  RR  /\  M  e.  ZZ )  ->  ( ( M  / 
2 )  <  M  <->  ( |_ `  ( M  /  2 ) )  <  M ) )
2812, 26, 27syl2anc 643 . . . . . . . . . 10  |-  ( ph  ->  ( ( M  / 
2 )  <  M  <->  ( |_ `  ( M  /  2 ) )  <  M ) )
2925, 28mpbid 202 . . . . . . . . 9  |-  ( ph  ->  ( |_ `  ( M  /  2 ) )  <  M )
3014, 11, 29ltled 9221 . . . . . . . 8  |-  ( ph  ->  ( |_ `  ( M  /  2 ) )  <_  M )
31 elfz2nn0 11082 . . . . . . . 8  |-  ( ( |_ `  ( M  /  2 ) )  e.  ( 0 ... M )  <->  ( ( |_ `  ( M  / 
2 ) )  e. 
NN0  /\  M  e.  NN0 
/\  ( |_ `  ( M  /  2
) )  <_  M
) )
3222, 23, 30, 31syl3anbrc 1138 . . . . . . 7  |-  ( ph  ->  ( |_ `  ( M  /  2 ) )  e.  ( 0 ... M ) )
33 nn0uz 10520 . . . . . . . . 9  |-  NN0  =  ( ZZ>= `  0 )
3423, 33syl6eleq 2526 . . . . . . . 8  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
35 elfzp12 11126 . . . . . . . 8  |-  ( M  e.  ( ZZ>= `  0
)  ->  ( ( |_ `  ( M  / 
2 ) )  e.  ( 0 ... M
)  <->  ( ( |_
`  ( M  / 
2 ) )  =  0  \/  ( |_
`  ( M  / 
2 ) )  e.  ( ( 0  +  1 ) ... M
) ) ) )
3634, 35syl 16 . . . . . . 7  |-  ( ph  ->  ( ( |_ `  ( M  /  2
) )  e.  ( 0 ... M )  <-> 
( ( |_ `  ( M  /  2
) )  =  0  \/  ( |_ `  ( M  /  2
) )  e.  ( ( 0  +  1 ) ... M ) ) ) )
3732, 36mpbid 202 . . . . . 6  |-  ( ph  ->  ( ( |_ `  ( M  /  2
) )  =  0  \/  ( |_ `  ( M  /  2
) )  e.  ( ( 0  +  1 ) ... M ) ) )
38 oveq2 6089 . . . . . . . . . 10  |-  ( ( |_ `  ( M  /  2 ) )  =  0  ->  (
1 ... ( |_ `  ( M  /  2
) ) )  =  ( 1 ... 0
) )
39 fz10 11075 . . . . . . . . . 10  |-  ( 1 ... 0 )  =  (/)
4038, 39syl6eq 2484 . . . . . . . . 9  |-  ( ( |_ `  ( M  /  2 ) )  =  0  ->  (
1 ... ( |_ `  ( M  /  2
) ) )  =  (/) )
41 oveq1 6088 . . . . . . . . . . 11  |-  ( ( |_ `  ( M  /  2 ) )  =  0  ->  (
( |_ `  ( M  /  2 ) )  +  1 )  =  ( 0  +  1 ) )
42 0p1e1 10093 . . . . . . . . . . 11  |-  ( 0  +  1 )  =  1
4341, 42syl6eq 2484 . . . . . . . . . 10  |-  ( ( |_ `  ( M  /  2 ) )  =  0  ->  (
( |_ `  ( M  /  2 ) )  +  1 )  =  1 )
4443oveq1d 6096 . . . . . . . . 9  |-  ( ( |_ `  ( M  /  2 ) )  =  0  ->  (
( ( |_ `  ( M  /  2
) )  +  1 ) ... M )  =  ( 1 ... M ) )
4540, 44uneq12d 3502 . . . . . . . 8  |-  ( ( |_ `  ( M  /  2 ) )  =  0  ->  (
( 1 ... ( |_ `  ( M  / 
2 ) ) )  u.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M ) )  =  ( (/)  u.  (
1 ... M ) ) )
46 un0 3652 . . . . . . . . 9  |-  ( ( 1 ... M )  u.  (/) )  =  ( 1 ... M )
47 uncom 3491 . . . . . . . . 9  |-  ( ( 1 ... M )  u.  (/) )  =  (
(/)  u.  ( 1 ... M ) )
4846, 47eqtr3i 2458 . . . . . . . 8  |-  ( 1 ... M )  =  ( (/)  u.  (
1 ... M ) )
4945, 48syl6reqr 2487 . . . . . . 7  |-  ( ( |_ `  ( M  /  2 ) )  =  0  ->  (
1 ... M )  =  ( ( 1 ... ( |_ `  ( M  /  2 ) ) )  u.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M ) ) )
50 fzsplit 11077 . . . . . . . 8  |-  ( ( |_ `  ( M  /  2 ) )  e.  ( 1 ... M )  ->  (
1 ... M )  =  ( ( 1 ... ( |_ `  ( M  /  2 ) ) )  u.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M ) ) )
5142oveq1i 6091 . . . . . . . 8  |-  ( ( 0  +  1 ) ... M )  =  ( 1 ... M
)
5250, 51eleq2s 2528 . . . . . . 7  |-  ( ( |_ `  ( M  /  2 ) )  e.  ( ( 0  +  1 ) ... M )  ->  (
1 ... M )  =  ( ( 1 ... ( |_ `  ( M  /  2 ) ) )  u.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M ) ) )
5349, 52jaoi 369 . . . . . 6  |-  ( ( ( |_ `  ( M  /  2 ) )  =  0  \/  ( |_ `  ( M  / 
2 ) )  e.  ( ( 0  +  1 ) ... M
) )  ->  (
1 ... M )  =  ( ( 1 ... ( |_ `  ( M  /  2 ) ) )  u.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M ) ) )
5437, 53syl 16 . . . . 5  |-  ( ph  ->  ( 1 ... M
)  =  ( ( 1 ... ( |_
`  ( M  / 
2 ) ) )  u.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M ) ) )
55 fzfid 11312 . . . . 5  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
562eldifad 3332 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  Prime )
57 prmnn 13082 . . . . . . . . . . . 12  |-  ( Q  e.  Prime  ->  Q  e.  NN )
5856, 57syl 16 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  NN )
5958nnred 10015 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  RR )
601eldifad 3332 . . . . . . . . . . 11  |-  ( ph  ->  P  e.  Prime )
61 prmnn 13082 . . . . . . . . . . 11  |-  ( P  e.  Prime  ->  P  e.  NN )
6260, 61syl 16 . . . . . . . . . 10  |-  ( ph  ->  P  e.  NN )
6359, 62nndivred 10048 . . . . . . . . 9  |-  ( ph  ->  ( Q  /  P
)  e.  RR )
6463adantr 452 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( 1 ... M
) )  ->  ( Q  /  P )  e.  RR )
65 2nn 10133 . . . . . . . . . 10  |-  2  e.  NN
66 elfznn 11080 . . . . . . . . . . 11  |-  ( u  e.  ( 1 ... M )  ->  u  e.  NN )
6766adantl 453 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( 1 ... M
) )  ->  u  e.  NN )
68 nnmulcl 10023 . . . . . . . . . 10  |-  ( ( 2  e.  NN  /\  u  e.  NN )  ->  ( 2  x.  u
)  e.  NN )
6965, 67, 68sylancr 645 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( 1 ... M
) )  ->  (
2  x.  u )  e.  NN )
7069nnred 10015 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( 1 ... M
) )  ->  (
2  x.  u )  e.  RR )
7164, 70remulcld 9116 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( 1 ... M
) )  ->  (
( Q  /  P
)  x.  ( 2  x.  u ) )  e.  RR )
7258nnrpd 10647 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  RR+ )
7362nnrpd 10647 . . . . . . . . . . 11  |-  ( ph  ->  P  e.  RR+ )
7472, 73rpdivcld 10665 . . . . . . . . . 10  |-  ( ph  ->  ( Q  /  P
)  e.  RR+ )
7574adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( 1 ... M
) )  ->  ( Q  /  P )  e.  RR+ )
7669nnrpd 10647 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( 1 ... M
) )  ->  (
2  x.  u )  e.  RR+ )
7775, 76rpmulcld 10664 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( 1 ... M
) )  ->  (
( Q  /  P
)  x.  ( 2  x.  u ) )  e.  RR+ )
7877rpge0d 10652 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( 1 ... M
) )  ->  0  <_  ( ( Q  /  P )  x.  (
2  x.  u ) ) )
79 flge0nn0 11225 . . . . . . 7  |-  ( ( ( ( Q  /  P )  x.  (
2  x.  u ) )  e.  RR  /\  0  <_  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  -> 
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  e.  NN0 )
8071, 78, 79syl2anc 643 . . . . . 6  |-  ( (
ph  /\  u  e.  ( 1 ... M
) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e. 
NN0 )
8180nn0cnd 10276 . . . . 5  |-  ( (
ph  /\  u  e.  ( 1 ... M
) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e.  CC )
8217, 54, 55, 81fsumsplit 12533 . . . 4  |-  ( ph  -> 
sum_ u  e.  (
1 ... M ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u ) ) )  =  ( sum_ u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  +  sum_ u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) )
837, 82syl5eqr 2482 . . 3  |-  ( ph  -> 
sum_ u  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u ) ) )  =  ( sum_ u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  +  sum_ u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) )
8483oveq2d 6097 . 2  |-  ( ph  ->  ( -u 1 ^
sum_ u  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u ) ) ) )  =  ( -u
1 ^ ( sum_ u  e.  ( 1 ... ( |_ `  ( M  /  2 ) ) ) ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) )  +  sum_ u  e.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) )
85 neg1cn 10067 . . . . 5  |-  -u 1  e.  CC
8685a1i 11 . . . 4  |-  ( ph  -> 
-u 1  e.  CC )
87 fzfid 11312 . . . . 5  |-  ( ph  ->  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  e.  Fin )
88 ssun2 3511 . . . . . . . 8  |-  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M )  C_  (
( 1 ... ( |_ `  ( M  / 
2 ) ) )  u.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M ) )
8988, 54syl5sseqr 3397 . . . . . . 7  |-  ( ph  ->  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  C_  ( 1 ... M ) )
9089sselda 3348 . . . . . 6  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  u  e.  ( 1 ... M
) )
9190, 80syldan 457 . . . . 5  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e. 
NN0 )
9287, 91fsumnn0cl 12530 . . . 4  |-  ( ph  -> 
sum_ u  e.  (
( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  e.  NN0 )
93 fzfid 11312 . . . . 5  |-  ( ph  ->  ( 1 ... ( |_ `  ( M  / 
2 ) ) )  e.  Fin )
94 ssun1 3510 . . . . . . . 8  |-  ( 1 ... ( |_ `  ( M  /  2
) ) )  C_  ( ( 1 ... ( |_ `  ( M  /  2 ) ) )  u.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M ) )
9594, 54syl5sseqr 3397 . . . . . . 7  |-  ( ph  ->  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) 
C_  ( 1 ... M ) )
9695sselda 3348 . . . . . 6  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  u  e.  ( 1 ... M
) )
9796, 80syldan 457 . . . . 5  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) )  e.  NN0 )
9893, 97fsumnn0cl 12530 . . . 4  |-  ( ph  -> 
sum_ u  e.  (
1 ... ( |_ `  ( M  /  2
) ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u ) ) )  e.  NN0 )
9986, 92, 98expaddd 11525 . . 3  |-  ( ph  ->  ( -u 1 ^ ( sum_ u  e.  ( 1 ... ( |_
`  ( M  / 
2 ) ) ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  +  sum_ u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) )  =  ( ( -u
1 ^ sum_ u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) ) )  x.  ( -u 1 ^ sum_ u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) ) )
100 fzfid 11312 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... N
)  e.  Fin )
101 xpfi 7378 . . . . . . . . 9  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ( 1 ... N
)  e.  Fin )  ->  ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin )
10255, 100, 101syl2anc 643 . . . . . . . 8  |-  ( ph  ->  ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin )
103 lgsquad.6 . . . . . . . . 9  |-  S  =  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  <  (
x  x.  Q ) ) }
104 opabssxp 4950 . . . . . . . . 9  |-  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  < 
( x  x.  Q
) ) }  C_  ( ( 1 ... M )  X.  (
1 ... N ) )
105103, 104eqsstri 3378 . . . . . . . 8  |-  S  C_  ( ( 1 ... M )  X.  (
1 ... N ) )
106 ssfi 7329 . . . . . . . 8  |-  ( ( ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin  /\  S  C_  ( ( 1 ... M )  X.  (
1 ... N ) ) )  ->  S  e.  Fin )
107102, 105, 106sylancl 644 . . . . . . 7  |-  ( ph  ->  S  e.  Fin )
108 ssrab2 3428 . . . . . . 7  |-  { z  e.  S  |  -.  2  ||  ( 1st `  z
) }  C_  S
109 ssfi 7329 . . . . . . 7  |-  ( ( S  e.  Fin  /\  { z  e.  S  |  -.  2  ||  ( 1st `  z ) }  C_  S )  ->  { z  e.  S  |  -.  2  ||  ( 1st `  z
) }  e.  Fin )
110107, 108, 109sylancl 644 . . . . . 6  |-  ( ph  ->  { z  e.  S  |  -.  2  ||  ( 1st `  z ) }  e.  Fin )
111 hashcl 11639 . . . . . 6  |-  ( { z  e.  S  |  -.  2  ||  ( 1st `  z ) }  e.  Fin  ->  ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } )  e.  NN0 )
112110, 111syl 16 . . . . 5  |-  ( ph  ->  ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } )  e.  NN0 )
113 ssrab2 3428 . . . . . . 7  |-  { z  e.  S  |  2 
||  ( 1st `  z
) }  C_  S
114 ssfi 7329 . . . . . . 7  |-  ( ( S  e.  Fin  /\  { z  e.  S  | 
2  ||  ( 1st `  z ) }  C_  S )  ->  { z  e.  S  |  2 
||  ( 1st `  z
) }  e.  Fin )
115107, 113, 114sylancl 644 . . . . . 6  |-  ( ph  ->  { z  e.  S  |  2  ||  ( 1st `  z ) }  e.  Fin )
116 hashcl 11639 . . . . . 6  |-  ( { z  e.  S  | 
2  ||  ( 1st `  z ) }  e.  Fin  ->  ( # `  {
z  e.  S  | 
2  ||  ( 1st `  z ) } )  e.  NN0 )
117115, 116syl 16 . . . . 5  |-  ( ph  ->  ( # `  {
z  e.  S  | 
2  ||  ( 1st `  z ) } )  e.  NN0 )
11886, 112, 117expaddd 11525 . . . 4  |-  ( ph  ->  ( -u 1 ^ ( ( # `  {
z  e.  S  | 
2  ||  ( 1st `  z ) } )  +  ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) ) )  =  ( ( -u 1 ^ ( # `  {
z  e.  S  | 
2  ||  ( 1st `  z ) } ) )  x.  ( -u
1 ^ ( # `  { z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) ) ) )
11996, 69syldan 457 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( 2  x.  u )  e.  NN )
120 fzfid 11312 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) )  e. 
Fin )
121 xpsnen2g 7201 . . . . . . . . . . 11  |-  ( ( ( 2  x.  u
)  e.  NN  /\  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) )  e.  Fin )  -> 
( { ( 2  x.  u ) }  X.  ( 1 ... ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) ) ) )  ~~  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) )
122119, 120, 121syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( {
( 2  x.  u
) }  X.  (
1 ... ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) ) 
~~  ( 1 ... ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) ) ) )
123 hasheni 11632 . . . . . . . . . 10  |-  ( ( { ( 2  x.  u ) }  X.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) )  ~~  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) )  -> 
( # `  ( { ( 2  x.  u
) }  X.  (
1 ... ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) ) )  =  ( # `  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) )
124122, 123syl 16 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( # `  ( { ( 2  x.  u ) }  X.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) )  =  (
# `  ( 1 ... ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) ) ) ) )
125 ssrab2 3428 . . . . . . . . . . . . 13  |-  { z  e.  S  |  ( 2  x.  u )  =  ( 1st `  z
) }  C_  S
126103relopabi 5000 . . . . . . . . . . . . 13  |-  Rel  S
127 relss 4963 . . . . . . . . . . . . 13  |-  ( { z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) }  C_  S  ->  ( Rel  S  ->  Rel  { z  e.  S  |  ( 2  x.  u )  =  ( 1st `  z
) } ) )
128125, 126, 127mp2 9 . . . . . . . . . . . 12  |-  Rel  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) }
129 relxp 4983 . . . . . . . . . . . 12  |-  Rel  ( { ( 2  x.  u ) }  X.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) )
130103eleq2i 2500 . . . . . . . . . . . . . . . 16  |-  ( <.
x ,  y >.  e.  S  <->  <. x ,  y
>.  e.  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  < 
( x  x.  Q
) ) } )
131 opabid 4461 . . . . . . . . . . . . . . . 16  |-  ( <.
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 ) ) )
132130, 131bitri 241 . . . . . . . . . . . . . . 15  |-  ( <.
x ,  y >.  e.  S  <->  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) )
133 anass 631 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  NN  /\  y  <_  N )  /\  ( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) ) )  <->  ( y  e.  NN  /\  ( y  <_  N  /\  (
y  x.  P )  <  ( Q  x.  ( 2  x.  u
) ) ) ) )
134 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  y  e.  NN )
13562ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  P  e.  NN )
136134, 135nnmulcld 10047 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
y  x.  P )  e.  NN )
137136nnred 10015 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
y  x.  P )  e.  RR )
13858adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  Q  e.  NN )
139138, 119nnmulcld 10047 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( Q  x.  ( 2  x.  u
) )  e.  NN )
140139adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( Q  x.  ( 2  x.  u ) )  e.  NN )
141140nnred 10015 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( Q  x.  ( 2  x.  u ) )  e.  RR )
142137, 141ltlend 9218 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) )  <->  ( (
y  x.  P )  <_  ( Q  x.  ( 2  x.  u
) )  /\  ( Q  x.  ( 2  x.  u ) )  =/=  ( y  x.  P ) ) ) )
143119adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
2  x.  u )  e.  NN )
144143nnred 10015 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
2  x.  u )  e.  RR )
145135nnred 10015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  P  e.  RR )
146145rehalfcld 10214 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( P  /  2 )  e.  RR )
14711adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  M  e.  RR )
148147adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  M  e.  RR )
149 elfzle2 11061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( u  e.  ( 1 ... ( |_ `  ( M  /  2 ) ) )  ->  u  <_  ( |_ `  ( M  /  2 ) ) )
150149adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  u  <_  ( |_ `  ( M  /  2 ) ) )
151147rehalfcld 10214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( M  /  2 )  e.  RR )
152 elfzelz 11059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( u  e.  ( 1 ... ( |_ `  ( M  /  2 ) ) )  ->  u  e.  ZZ )
153152adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  u  e.  ZZ )
154 flge 11214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( M  /  2
)  e.  RR  /\  u  e.  ZZ )  ->  ( u  <_  ( M  /  2 )  <->  u  <_  ( |_ `  ( M  /  2 ) ) ) )
155151, 153, 154syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( u  <_  ( M  /  2
)  <->  u  <_  ( |_
`  ( M  / 
2 ) ) ) )
156150, 155mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  u  <_  ( M  /  2 ) )
157 elfznn 11080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( u  e.  ( 1 ... ( |_ `  ( M  /  2 ) ) )  ->  u  e.  NN )
158157adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  u  e.  NN )
159158nnred 10015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  u  e.  RR )
160 2re 10069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  2  e.  RR
161160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  2  e.  RR )
162 2pos 10082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  0  <  2
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  0  <  2 )
164 lemuldiv2 9890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( u  e.  RR  /\  M  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( 2  x.  u )  <_  M 
<->  u  <_  ( M  /  2 ) ) )
165159, 147, 161, 163, 164syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( (
2  x.  u )  <_  M  <->  u  <_  ( M  /  2 ) ) )
166156, 165mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( 2  x.  u )  <_  M )
167166adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
2  x.  u )  <_  M )
168145ltm1d 9943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( P  -  1 )  <  P )
169 peano2rem 9367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( P  e.  RR  ->  ( P  -  1 )  e.  RR )
170145, 169syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( P  -  1 )  e.  RR )
171160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  2  e.  RR )
172162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  0  <  2 )
173 ltdiv1 9874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( P  -  1 )  e.  RR  /\  P  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( P  -  1 )  < 
P  <->  ( ( P  -  1 )  / 
2 )  <  ( P  /  2 ) ) )
174170, 145, 171, 172, 173syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( P  -  1 )  <  P  <->  ( ( P  -  1 )  /  2 )  < 
( P  /  2
) ) )
175168, 174mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( P  -  1 )  /  2 )  <  ( P  / 
2 ) )
1765, 175syl5eqbr 4245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  M  <  ( P  /  2
) )
177144, 148, 146, 167, 176lelttrd 9228 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
2  x.  u )  <  ( P  / 
2 ) )
178135nnrpd 10647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  P  e.  RR+ )
179 rphalflt 10638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e.  RR+  ->  ( P  /  2 )  < 
P )
180178, 179syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( P  /  2 )  < 
P )
181144, 146, 145, 177, 180lttrd 9231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
2  x.  u )  <  P )
182144, 145ltnled 9220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( 2  x.  u
)  <  P  <->  -.  P  <_  ( 2  x.  u
) ) )
183181, 182mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  -.  P  <_  ( 2  x.  u ) )
18460ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  P  e.  Prime )
185 prmz 13083 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( P  e.  Prime  ->  P  e.  ZZ )
186184, 185syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  P  e.  ZZ )
187 dvdsle 12895 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( P  e.  ZZ  /\  ( 2  x.  u
)  e.  NN )  ->  ( P  ||  ( 2  x.  u
)  ->  P  <_  ( 2  x.  u ) ) )
188186, 143, 187syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( P  ||  ( 2  x.  u )  ->  P  <_  ( 2  x.  u
) ) )
189183, 188mtod 170 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  -.  P  ||  ( 2  x.  u ) )
190 prmrp 13101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( P  e.  Prime  /\  Q  e.  Prime )  ->  (
( P  gcd  Q
)  =  1  <->  P  =/=  Q ) )
19160, 56, 190syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( ( P  gcd  Q )  =  1  <->  P  =/=  Q ) )
1923, 191mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( P  gcd  Q
)  =  1 )
193192ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( P  gcd  Q )  =  1 )
19456ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  Q  e.  Prime )
195 prmz 13083 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( Q  e.  Prime  ->  Q  e.  ZZ )
196194, 195syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  Q  e.  ZZ )
197143nnzd 10374 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
2  x.  u )  e.  ZZ )
198 coprmdvds 13102 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( P  e.  ZZ  /\  Q  e.  ZZ  /\  (
2  x.  u )  e.  ZZ )  -> 
( ( P  ||  ( Q  x.  (
2  x.  u ) )  /\  ( P  gcd  Q )  =  1 )  ->  P  ||  ( 2  x.  u
) ) )
199186, 196, 197, 198syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( P  ||  ( Q  x.  ( 2  x.  u ) )  /\  ( P  gcd  Q )  =  1 )  ->  P  ||  (
2  x.  u ) ) )
200193, 199mpan2d 656 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( P  ||  ( Q  x.  ( 2  x.  u
) )  ->  P  ||  ( 2  x.  u
) ) )
201189, 200mtod 170 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  -.  P  ||  ( Q  x.  ( 2  x.  u
) ) )
202 nnz 10303 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  e.  NN  ->  y  e.  ZZ )
203202adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  y  e.  ZZ )
204 dvdsmul2 12872 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( y  e.  ZZ  /\  P  e.  ZZ )  ->  P  ||  ( y  x.  P ) )
205203, 186, 204syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  P  ||  ( y  x.  P
) )
206 breq2 4216 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( Q  x.  ( 2  x.  u ) )  =  ( y  x.  P )  ->  ( P  ||  ( Q  x.  ( 2  x.  u
) )  <->  P  ||  (
y  x.  P ) ) )
207205, 206syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( Q  x.  (
2  x.  u ) )  =  ( y  x.  P )  ->  P  ||  ( Q  x.  ( 2  x.  u
) ) ) )
208207necon3bd 2638 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( -.  P  ||  ( Q  x.  ( 2  x.  u ) )  -> 
( Q  x.  (
2  x.  u ) )  =/=  ( y  x.  P ) ) )
209201, 208mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( Q  x.  ( 2  x.  u ) )  =/=  ( y  x.  P ) )
210209biantrud 494 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  x.  P
)  <_  ( Q  x.  ( 2  x.  u
) )  <->  ( (
y  x.  P )  <_  ( Q  x.  ( 2  x.  u
) )  /\  ( Q  x.  ( 2  x.  u ) )  =/=  ( y  x.  P ) ) ) )
211142, 210bitr4d 248 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) )  <->  ( y  x.  P )  <_  ( Q  x.  ( 2  x.  u ) ) ) )
212 nnre 10007 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  NN  ->  y  e.  RR )
213212adantl 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  y  e.  RR )
214135nngt0d 10043 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  0  <  P )
215 lemuldiv 9889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  RR  /\  ( Q  x.  (
2  x.  u ) )  e.  RR  /\  ( P  e.  RR  /\  0  <  P ) )  ->  ( (
y  x.  P )  <_  ( Q  x.  ( 2  x.  u
) )  <->  y  <_  ( ( Q  x.  (
2  x.  u ) )  /  P ) ) )
216213, 141, 145, 214, 215syl112anc 1188 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  x.  P
)  <_  ( Q  x.  ( 2  x.  u
) )  <->  y  <_  ( ( Q  x.  (
2  x.  u ) )  /  P ) ) )
217138adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  Q  e.  NN )
218217nncnd 10016 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  Q  e.  CC )
219143nncnd 10016 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
2  x.  u )  e.  CC )
220135nncnd 10016 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  P  e.  CC )
221135nnne0d 10044 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  P  =/=  0 )
222218, 219, 220, 221div23d 9827 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( Q  x.  (
2  x.  u ) )  /  P )  =  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )
223222breq2d 4224 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
y  <_  ( ( Q  x.  ( 2  x.  u ) )  /  P )  <->  y  <_  ( ( Q  /  P
)  x.  ( 2  x.  u ) ) ) )
224211, 216, 2233bitrd 271 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) )  <->  y  <_  ( ( Q  /  P
)  x.  ( 2  x.  u ) ) ) )
225217nnred 10015 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  Q  e.  RR )
226217nngt0d 10043 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  0  <  Q )
227 ltmul2 9861 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 2  x.  u
)  e.  RR  /\  ( P  /  2
)  e.  RR  /\  ( Q  e.  RR  /\  0  <  Q ) )  ->  ( (
2  x.  u )  <  ( P  / 
2 )  <->  ( Q  x.  ( 2  x.  u
) )  <  ( Q  x.  ( P  /  2 ) ) ) )
228144, 146, 225, 226, 227syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( 2  x.  u
)  <  ( P  /  2 )  <->  ( Q  x.  ( 2  x.  u
) )  <  ( Q  x.  ( P  /  2 ) ) ) )
229177, 228mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( Q  x.  ( 2  x.  u ) )  <  ( Q  x.  ( P  /  2
) ) )
230 2cn 10070 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  e.  CC
231230a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  2  e.  CC )
232 2ne0 10083 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  =/=  0
233232a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  2  =/=  0 )
234 divass 9696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Q  e.  CC  /\  P  e.  CC  /\  (
2  e.  CC  /\  2  =/=  0 ) )  ->  ( ( Q  x.  P )  / 
2 )  =  ( Q  x.  ( P  /  2 ) ) )
235 div23 9697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Q  e.  CC  /\  P  e.  CC  /\  (
2  e.  CC  /\  2  =/=  0 ) )  ->  ( ( Q  x.  P )  / 
2 )  =  ( ( Q  /  2
)  x.  P ) )
236234, 235eqtr3d 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Q  e.  CC  /\  P  e.  CC  /\  (
2  e.  CC  /\  2  =/=  0 ) )  ->  ( Q  x.  ( P  /  2
) )  =  ( ( Q  /  2
)  x.  P ) )
237218, 220, 231, 233, 236syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( Q  x.  ( P  /  2 ) )  =  ( ( Q  /  2 )  x.  P ) )
238229, 237breqtrd 4236 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( Q  x.  ( 2  x.  u ) )  <  ( ( Q  /  2 )  x.  P ) )
239225rehalfcld 10214 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( Q  /  2 )  e.  RR )
240239, 145remulcld 9116 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( Q  /  2
)  x.  P )  e.  RR )
241 lttr 9152 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( y  x.  P
)  e.  RR  /\  ( Q  x.  (
2  x.  u ) )  e.  RR  /\  ( ( Q  / 
2 )  x.  P
)  e.  RR )  ->  ( ( ( y  x.  P )  <  ( Q  x.  ( 2  x.  u
) )  /\  ( Q  x.  ( 2  x.  u ) )  <  ( ( Q  /  2 )  x.  P ) )  -> 
( y  x.  P
)  <  ( ( Q  /  2 )  x.  P ) ) )
242137, 141, 240, 241syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( ( y  x.  P )  <  ( Q  x.  ( 2  x.  u ) )  /\  ( Q  x.  ( 2  x.  u
) )  <  (
( Q  /  2
)  x.  P ) )  ->  ( y  x.  P )  <  (
( Q  /  2
)  x.  P ) ) )
243238, 242mpan2d 656 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) )  ->  (
y  x.  P )  <  ( ( Q  /  2 )  x.  P ) ) )
244 ltmul1 9860 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( y  e.  RR  /\  ( Q  /  2
)  e.  RR  /\  ( P  e.  RR  /\  0  <  P ) )  ->  ( y  <  ( Q  /  2
)  <->  ( y  x.  P )  <  (
( Q  /  2
)  x.  P ) ) )
245213, 239, 145, 214, 244syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
y  <  ( Q  /  2 )  <->  ( y  x.  P )  <  (
( Q  /  2
)  x.  P ) ) )
246243, 245sylibrd 226 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) )  ->  y  <  ( Q  /  2
) ) )
247 peano2rem 9367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Q  e.  RR  ->  ( Q  -  1 )  e.  RR )
248225, 247syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( Q  -  1 )  e.  RR )
249248recnd 9114 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( Q  -  1 )  e.  CC )
250218, 249, 231, 233divsubdird 9829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( Q  -  ( Q  -  1 ) )  /  2 )  =  ( ( Q  /  2 )  -  ( ( Q  - 
1 )  /  2
) ) )
251 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  N  =  ( ( Q  - 
1 )  /  2
)
252251oveq2i 6092 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Q  /  2 )  -  N )  =  ( ( Q  / 
2 )  -  (
( Q  -  1 )  /  2 ) )
253250, 252syl6eqr 2486 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( Q  -  ( Q  -  1 ) )  /  2 )  =  ( ( Q  /  2 )  -  N ) )
254 ax-1cn 9048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  1  e.  CC
255 nncan 9330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( Q  e.  CC  /\  1  e.  CC )  ->  ( Q  -  ( Q  -  1 ) )  =  1 )
256218, 254, 255sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( Q  -  ( Q  -  1 ) )  =  1 )
257256oveq1d 6096 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( Q  -  ( Q  -  1 ) )  /  2 )  =  ( 1  / 
2 ) )
258 halflt1 10189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 1  /  2 )  <  1
259257, 258syl6eqbr 4249 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( Q  -  ( Q  -  1 ) )  /  2 )  <  1 )
260253, 259eqbrtrrd 4234 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( Q  /  2
)  -  N )  <  1 )
261 oddprm 13189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Q  e.  ( Prime  \  {
2 } )  -> 
( ( Q  - 
1 )  /  2
)  e.  NN )
2622, 261syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( ( Q  - 
1 )  /  2
)  e.  NN )
263251, 262syl5eqel 2520 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  N  e.  NN )
264263ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  N  e.  NN )
265264nnred 10015 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  N  e.  RR )
266 1re 9090 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  1  e.  RR
267266a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  1  e.  RR )
268239, 265, 267ltsubadd2d 9624 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( ( Q  / 
2 )  -  N
)  <  1  <->  ( Q  /  2 )  < 
( N  +  1 ) ) )
269260, 268mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( Q  /  2 )  < 
( N  +  1 ) )
270 peano2re 9239 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
271265, 270syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  ( N  +  1 )  e.  RR )
272 lttr 9152 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( y  e.  RR  /\  ( Q  /  2
)  e.  RR  /\  ( N  +  1
)  e.  RR )  ->  ( ( y  <  ( Q  / 
2 )  /\  ( Q  /  2 )  < 
( N  +  1 ) )  ->  y  <  ( N  +  1 ) ) )
273213, 239, 271, 272syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  <  ( Q  /  2 )  /\  ( Q  /  2
)  <  ( N  +  1 ) )  ->  y  <  ( N  +  1 ) ) )
274269, 273mpan2d 656 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
y  <  ( Q  /  2 )  -> 
y  <  ( N  +  1 ) ) )
275246, 274syld 42 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) )  ->  y  <  ( N  +  1 ) ) )
276 nnleltp1 10329 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  NN  /\  N  e.  NN )  ->  ( y  <_  N  <->  y  <  ( N  + 
1 ) ) )
277134, 264, 276syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
y  <_  N  <->  y  <  ( N  +  1 ) ) )
278275, 277sylibrd 226 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) )  ->  y  <_  N ) )
279278pm4.71rd 617 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) )  <->  ( y  <_  N  /\  ( y  x.  P )  < 
( Q  x.  (
2  x.  u ) ) ) ) )
28096, 71syldan 457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( ( Q  /  P )  x.  ( 2  x.  u
) )  e.  RR )
281 flge 11214 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( Q  /  P )  x.  (
2  x.  u ) )  e.  RR  /\  y  e.  ZZ )  ->  ( y  <_  (
( Q  /  P
)  x.  ( 2  x.  u ) )  <-> 
y  <_  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) )
282280, 202, 281syl2an 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
y  <_  ( ( Q  /  P )  x.  ( 2  x.  u
) )  <->  y  <_  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u ) ) ) ) )
283224, 279, 2823bitr3d 275 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  y  e.  NN )  ->  (
( y  <_  N  /\  ( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) ) )  <->  y  <_  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u ) ) ) ) )
284283pm5.32da 623 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( (
y  e.  NN  /\  ( y  <_  N  /\  ( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) ) ) )  <-> 
( y  e.  NN  /\  y  <_  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) ) )
285133, 284syl5bb 249 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( (
( y  e.  NN  /\  y  <_  N )  /\  ( y  x.  P
)  <  ( Q  x.  ( 2  x.  u
) ) )  <->  ( y  e.  NN  /\  y  <_ 
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) ) ) ) )
286285adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  (
( ( y  e.  NN  /\  y  <_  N )  /\  (
y  x.  P )  <  ( Q  x.  ( 2  x.  u
) ) )  <->  ( y  e.  NN  /\  y  <_ 
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) ) ) ) )
287 simpr 448 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  x  =  ( 2  x.  u ) )
288 nnuz 10521 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  NN  =  ( ZZ>= `  1 )
289119, 288syl6eleq 2526 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( 2  x.  u )  e.  ( ZZ>= `  1 )
)
29026adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  M  e.  ZZ )
291 elfz5 11051 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 2  x.  u
)  e.  ( ZZ>= ` 
1 )  /\  M  e.  ZZ )  ->  (
( 2  x.  u
)  e.  ( 1 ... M )  <->  ( 2  x.  u )  <_  M ) )
292289, 290, 291syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( (
2  x.  u )  e.  ( 1 ... M )  <->  ( 2  x.  u )  <_  M ) )
293166, 292mpbird 224 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( 2  x.  u )  e.  ( 1 ... M
) )
294293adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  (
2  x.  u )  e.  ( 1 ... M ) )
295287, 294eqeltrd 2510 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  x  e.  ( 1 ... M
) )
296295biantrurd 495 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  (
y  e.  ( 1 ... N )  <->  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) ) )
297263nnzd 10374 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  N  e.  ZZ )
298297ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  N  e.  ZZ )
299 fznn 11115 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ZZ  ->  (
y  e.  ( 1 ... N )  <->  ( y  e.  NN  /\  y  <_  N ) ) )
300298, 299syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  (
y  e.  ( 1 ... N )  <->  ( y  e.  NN  /\  y  <_  N ) ) )
301296, 300bitr3d 247 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  (
( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  <->  ( y  e.  NN  /\  y  <_  N ) ) )
302 oveq1 6088 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( 2  x.  u )  ->  (
x  x.  Q )  =  ( ( 2  x.  u )  x.  Q ) )
303119nncnd 10016 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( 2  x.  u )  e.  CC )
304138nncnd 10016 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  Q  e.  CC )
305303, 304mulcomd 9109 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( (
2  x.  u )  x.  Q )  =  ( Q  x.  (
2  x.  u ) ) )
306302, 305sylan9eqr 2490 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  (
x  x.  Q )  =  ( Q  x.  ( 2  x.  u
) ) )
307306breq2d 4224 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  (
( y  x.  P
)  <  ( x  x.  Q )  <->  ( y  x.  P )  <  ( Q  x.  ( 2  x.  u ) ) ) )
308301, 307anbi12d 692 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 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
)  <  ( Q  x.  ( 2  x.  u
) ) ) ) )
309280flcld 11207 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) )  e.  ZZ )
310 fznn 11115 . . . . . . . . . . . . . . . . . 18  |-  ( ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u ) ) )  e.  ZZ  ->  (
y  e.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) )  <->  ( y  e.  NN  /\  y  <_ 
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) ) ) ) )
311309, 310syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( y  e.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) )  <-> 
( y  e.  NN  /\  y  <_  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) ) )
312311adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  (
y  e.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) )  <->  ( y  e.  NN  /\  y  <_ 
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) ) ) ) )
313286, 308, 3123bitr4d 277 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  (
( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) )  <->  y  e.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) )
314132, 313syl5bb 249 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  /\  x  =  ( 2  x.  u
) )  ->  ( <. x ,  y >.  e.  S  <->  y  e.  ( 1 ... ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) )
315314pm5.32da 623 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( (
x  =  ( 2  x.  u )  /\  <.
x ,  y >.  e.  S )  <->  ( x  =  ( 2  x.  u )  /\  y  e.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) ) )
316 vex 2959 . . . . . . . . . . . . . . . . . 18  |-  x  e. 
_V
317 vex 2959 . . . . . . . . . . . . . . . . . 18  |-  y  e. 
_V
318316, 317op1std 6357 . . . . . . . . . . . . . . . . 17  |-  ( z  =  <. x ,  y
>.  ->  ( 1st `  z
)  =  x )
319318eqeq2d 2447 . . . . . . . . . . . . . . . 16  |-  ( z  =  <. x ,  y
>.  ->  ( ( 2  x.  u )  =  ( 1st `  z
)  <->  ( 2  x.  u )  =  x ) )
320 eqcom 2438 . . . . . . . . . . . . . . . 16  |-  ( ( 2  x.  u )  =  x  <->  x  =  ( 2  x.  u
) )
321319, 320syl6bb 253 . . . . . . . . . . . . . . 15  |-  ( z  =  <. x ,  y
>.  ->  ( ( 2  x.  u )  =  ( 1st `  z
)  <->  x  =  (
2  x.  u ) ) )
322321elrab 3092 . . . . . . . . . . . . . 14  |-  ( <.
x ,  y >.  e.  { z  e.  S  |  ( 2  x.  u )  =  ( 1st `  z ) }  <->  ( <. x ,  y >.  e.  S  /\  x  =  (
2  x.  u ) ) )
323 ancom 438 . . . . . . . . . . . . . 14  |-  ( (
<. x ,  y >.  e.  S  /\  x  =  ( 2  x.  u ) )  <->  ( x  =  ( 2  x.  u )  /\  <. x ,  y >.  e.  S
) )
324322, 323bitri 241 . . . . . . . . . . . . 13  |-  ( <.
x ,  y >.  e.  { z  e.  S  |  ( 2  x.  u )  =  ( 1st `  z ) }  <->  ( x  =  ( 2  x.  u
)  /\  <. x ,  y >.  e.  S
) )
325 opelxp 4908 . . . . . . . . . . . . . 14  |-  ( <.
x ,  y >.  e.  ( { ( 2  x.  u ) }  X.  ( 1 ... ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) ) ) )  <->  ( x  e.  { ( 2  x.  u ) }  /\  y  e.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) ) )
326 elsn 3829 . . . . . . . . . . . . . . 15  |-  ( x  e.  { ( 2  x.  u ) }  <-> 
x  =  ( 2  x.  u ) )
327326anbi1i 677 . . . . . . . . . . . . . 14  |-  ( ( x  e.  { ( 2  x.  u ) }  /\  y  e.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) )  <->  ( x  =  ( 2  x.  u
)  /\  y  e.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) )
328325, 327bitri 241 . . . . . . . . . . . . 13  |-  ( <.
x ,  y >.  e.  ( { ( 2  x.  u ) }  X.  ( 1 ... ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) ) ) )  <->  ( x  =  ( 2  x.  u )  /\  y  e.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) )
329315, 324, 3283bitr4g 280 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( <. x ,  y >.  e.  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) }  <->  <. x ,  y >.  e.  ( { ( 2  x.  u ) }  X.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) ) )
330128, 129, 329eqrelrdv 4972 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  { z  e.  S  |  (
2  x.  u )  =  ( 1st `  z
) }  =  ( { ( 2  x.  u ) }  X.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) )
331330eqcomd 2441 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( {
( 2  x.  u
) }  X.  (
1 ... ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) )  =  { z  e.  S  |  ( 2  x.  u )  =  ( 1st `  z
) } )
332331fveq2d 5732 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( # `  ( { ( 2  x.  u ) }  X.  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) )  =  (
# `  { z  e.  S  |  (
2  x.  u )  =  ( 1st `  z
) } ) )
333 hashfz1 11630 . . . . . . . . . 10  |-  ( ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u ) ) )  e.  NN0  ->  ( # `  ( 1 ... ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) )  =  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) )
33497, 333syl 16 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( # `  (
1 ... ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) ) )  =  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) )
335124, 332, 3343eqtr3rd 2477 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) )  =  (
# `  { z  e.  S  |  (
2  x.  u )  =  ( 1st `  z
) } ) )
336335sumeq2dv 12497 . . . . . . 7  |-  ( ph  -> 
sum_ u  e.  (
1 ... ( |_ `  ( M  /  2
) ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u ) ) )  =  sum_ u  e.  ( 1 ... ( |_
`  ( M  / 
2 ) ) ) ( # `  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) } ) )
337107adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  S  e.  Fin )
338 ssfi 7329 . . . . . . . . 9  |-  ( ( S  e.  Fin  /\  { z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) }  C_  S )  ->  { z  e.  S  |  ( 2  x.  u )  =  ( 1st `  z
) }  e.  Fin )
339337, 125, 338sylancl 644 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  { z  e.  S  |  (
2  x.  u )  =  ( 1st `  z
) }  e.  Fin )
340 fveq2 5728 . . . . . . . . . . . . . . . 16  |-  ( z  =  v  ->  ( 1st `  z )  =  ( 1st `  v
) )
341340eqeq2d 2447 . . . . . . . . . . . . . . 15  |-  ( z  =  v  ->  (
( 2  x.  u
)  =  ( 1st `  z )  <->  ( 2  x.  u )  =  ( 1st `  v
) ) )
342341elrab 3092 . . . . . . . . . . . . . 14  |-  ( v  e.  { z  e.  S  |  ( 2  x.  u )  =  ( 1st `  z
) }  <->  ( v  e.  S  /\  (
2  x.  u )  =  ( 1st `  v
) ) )
343342simprbi 451 . . . . . . . . . . . . 13  |-  ( v  e.  { z  e.  S  |  ( 2  x.  u )  =  ( 1st `  z
) }  ->  (
2  x.  u )  =  ( 1st `  v
) )
344343ad2antll 710 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) )  /\  v  e.  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) } ) )  ->  ( 2  x.  u )  =  ( 1st `  v
) )
345344oveq1d 6096 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) )  /\  v  e.  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) } ) )  ->  ( (
2  x.  u )  /  2 )  =  ( ( 1st `  v
)  /  2 ) )
346158nncnd 10016 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) )  ->  u  e.  CC )
347346adantrr 698 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) )  /\  v  e.  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) } ) )  ->  u  e.  CC )
348230a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) )  /\  v  e.  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) } ) )  ->  2  e.  CC )
349232a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) )  /\  v  e.  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) } ) )  ->  2  =/=  0 )
350347, 348, 349divcan3d 9795 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) )  /\  v  e.  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) } ) )  ->  ( (
2  x.  u )  /  2 )  =  u )
351345, 350eqtr3d 2470 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) )  /\  v  e.  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) } ) )  ->  ( ( 1st `  v )  / 
2 )  =  u )
352351ralrimivva 2798 . . . . . . . . 9  |-  ( ph  ->  A. u  e.  ( 1 ... ( |_
`  ( M  / 
2 ) ) ) A. v  e.  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) }  (
( 1st `  v
)  /  2 )  =  u )
353 invdisj 4201 . . . . . . . . 9  |-  ( A. u  e.  ( 1 ... ( |_ `  ( M  /  2
) ) ) A. v  e.  { z  e.  S  |  (
2  x.  u )  =  ( 1st `  z
) }  ( ( 1st `  v )  /  2 )  =  u  -> Disj  u  e.  ( 1 ... ( |_
`  ( M  / 
2 ) ) ) { z  e.  S  |  ( 2  x.  u )  =  ( 1st `  z ) } )
354352, 353syl 16 . . . . . . . 8  |-  ( ph  -> Disj  u  e.  ( 1 ... ( |_ `  ( M  /  2
) ) ) { z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) } )
35593, 339, 354hashiun 12601 . . . . . . 7  |-  ( ph  ->  ( # `  U_ u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) { z  e.  S  |  ( 2  x.  u )  =  ( 1st `  z ) } )  =  sum_ u  e.  ( 1 ... ( |_ `  ( M  /  2 ) ) ) ( # `  {
z  e.  S  | 
( 2  x.  u
)  =  ( 1st `  z ) } ) )
356 iunrab 4138 . . . . . . . . 9  |-  U_ u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) { z  e.  S  |  ( 2  x.  u )  =  ( 1st `  z ) }  =  { z  e.  S  |  E. u  e.  ( 1 ... ( |_ `  ( M  /  2
) ) ) ( 2  x.  u )  =  ( 1st `  z
) }
357 zcn 10287 . . . . . . . . . . . . . . 15  |-  ( u  e.  ZZ  ->  u  e.  CC )
358357adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ZZ )  ->  u  e.  CC )
359 mulcom 9076 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  CC  /\  u  e.  CC )  ->  ( 2  x.  u
)  =  ( u  x.  2 ) )
360230, 358, 359sylancr 645 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ZZ )  ->  (
2  x.  u )  =  ( u  x.  2 ) )
361360eqeq1d 2444 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ZZ )  ->  (
( 2  x.  u
)  =  ( 1st `  z )  <->  ( u  x.  2 )  =  ( 1st `  z ) ) )
362361rexbidva 2722 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  S )  ->  ( E. u  e.  ZZ  ( 2  x.  u
)  =  ( 1st `  z )  <->  E. u  e.  ZZ  ( u  x.  2 )  =  ( 1st `  z ) ) )
363152anim1i 552 . . . . . . . . . . . . 13  |-  ( ( u  e.  ( 1 ... ( |_ `  ( M  /  2
) ) )  /\  ( 2  x.  u
)  =  ( 1st `  z ) )  -> 
( u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )
364363reximi2 2812 . . . . . . . . . . . 12  |-  ( E. u  e.  ( 1 ... ( |_ `  ( M  /  2
) ) ) ( 2  x.  u )  =  ( 1st `  z
)  ->  E. u  e.  ZZ  ( 2  x.  u )  =  ( 1st `  z ) )
365 simprr 734 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( 2  x.  u )  =  ( 1st `  z ) )
366 simpr 448 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  z  e.  S )  ->  z  e.  S )
367105, 366sseldi 3346 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  z  e.  S )  ->  z  e.  ( ( 1 ... M )  X.  (
1 ... N ) ) )
368 xp1st 6376 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  ( ( 1 ... M )  X.  ( 1 ... N
) )  ->  ( 1st `  z )  e.  ( 1 ... M
) )
369367, 368syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  S )  ->  ( 1st `  z )  e.  ( 1 ... M
) )
370369adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( 1st `  z
)  e.  ( 1 ... M ) )
371 elfzle2 11061 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1st `  z )  e.  ( 1 ... M )  ->  ( 1st `  z )  <_  M )
372370, 371syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( 1st `  z
)  <_  M )
373365, 372eqbrtrd 4232 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( 2  x.  u )  <_  M
)
374 zre 10286 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  e.  ZZ  ->  u  e.  RR )
375374ad2antrl 709 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  u  e.  RR )
37611ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  M  e.  RR )
377160a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  2  e.  RR )
378162a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  0  <  2
)
379375, 376, 377, 378, 164syl112anc 1188 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  u )  <_  M 
<->  u  <_  ( M  /  2 ) ) )
380373, 379mpbid 202 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  u  <_  ( M  /  2 ) )
38112ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( M  / 
2 )  e.  RR )
382 simprl 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  u  e.  ZZ )
383381, 382, 154syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( u  <_ 
( M  /  2
)  <->  u  <_  ( |_
`  ( M  / 
2 ) ) ) )
384380, 383mpbid 202 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  u  <_  ( |_ `  ( M  / 
2 ) ) )
385230mul01i 9256 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  x.  0 )  =  0
386 elfznn 11080 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 1st `  z )  e.  ( 1 ... M )  ->  ( 1st `  z )  e.  NN )
387370, 386syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( 1st `  z
)  e.  NN )
388365, 387eqeltrd 2510 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( 2  x.  u )  e.  NN )
389388nngt0d 10043 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  0  <  (
2  x.  u ) )
390385, 389syl5eqbr 4245 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( 2  x.  0 )  <  (
2  x.  u ) )
391 0re 9091 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
392391a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  0  e.  RR )
393 ltmul2 9861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0  e.  RR  /\  u  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( 0  < 
u  <->  ( 2  x.  0 )  <  (
2  x.  u ) ) )
394392, 375, 377, 378, 393syl112anc 1188 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( 0  < 
u  <->  ( 2  x.  0 )  <  (
2  x.  u ) ) )
395390, 394mpbird 224 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  0  <  u
)
396 elnnz 10292 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  NN  <->  ( u  e.  ZZ  /\  0  < 
u ) )
397382, 395, 396sylanbrc 646 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  u  e.  NN )
398397, 288syl6eleq 2526 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  u  e.  (
ZZ>= `  1 ) )
39913ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( |_ `  ( M  /  2
) )  e.  ZZ )
400 elfz5 11051 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  ( ZZ>= ` 
1 )  /\  ( |_ `  ( M  / 
2 ) )  e.  ZZ )  ->  (
u  e.  ( 1 ... ( |_ `  ( M  /  2
) ) )  <->  u  <_  ( |_ `  ( M  /  2 ) ) ) )
401398, 399, 400syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) )  <-> 
u  <_  ( |_ `  ( M  /  2
) ) ) )
402384, 401mpbird 224 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  u  e.  ( 1 ... ( |_
`  ( M  / 
2 ) ) ) )
403402, 365jca 519 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  S )  /\  (
u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) ) )  ->  ( u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) )  /\  ( 2  x.  u )  =  ( 1st `  z ) ) )
404403ex 424 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  S )  ->  (
( u  e.  ZZ  /\  ( 2  x.  u
)  =  ( 1st `  z ) )  -> 
( u  e.  ( 1 ... ( |_
`  ( M  / 
2 ) ) )  /\  ( 2  x.  u )  =  ( 1st `  z ) ) ) )
405404reximdv2 2815 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  S )  ->  ( E. u  e.  ZZ  ( 2  x.  u
)  =  ( 1st `  z )  ->  E. u  e.  ( 1 ... ( |_ `  ( M  / 
2 ) ) ) ( 2  x.  u
)  =  ( 1st `  z ) ) )
406364, 405impbid2 196 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  S )  ->  ( E. u  e.  (
1 ... ( |_ `  ( M  /  2
) ) ) ( 2  x.  u )  =  ( 1st `  z
)  <->  E. u  e.  ZZ  ( 2  x.  u
)  =  ( 1st `  z ) ) )
407 2z 10312 . . . . . . . . . . . 12  |-  2  e.  ZZ
408 elfzelz 11059 . . . . . . . . . . . . 13  |-  ( ( 1st `  z )  e.  ( 1 ... M )  ->  ( 1st `  z )  e.  ZZ )
409369, 408syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  S )  ->  ( 1st `  z )  e.  ZZ )
410 divides 12854 . . . . . . . . . . . 12  |-  ( ( 2  e.  ZZ  /\  ( 1st `  z )  e.  ZZ )  -> 
( 2  ||  ( 1st `  z )  <->  E. u  e.  ZZ  ( u