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

Theorem lgsquadlem1 21140
Description: Lemma for lgsquad 21143. Count the members of  S with odd coordinates. (Contributed by Mario Carneiro, 19-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
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
) } ) ) )
Distinct variable groups:    x, u, y, z, P    ph, u, x, y, z    u, M, y, z    u, N, x, y, z    u, Q, x, y, z    u, S, x, z    x, M   
y, S

Proof of Theorem lgsquadlem1
Dummy variables  n  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neg1cn 10069 . . . 4  |-  -u 1  e.  CC
21a1i 11 . . 3  |-  ( ph  -> 
-u 1  e.  CC )
3 ax-1cn 9050 . . . . 5  |-  1  e.  CC
4 ax-1ne0 9061 . . . . 5  |-  1  =/=  0
53, 4negne0i 9377 . . . 4  |-  -u 1  =/=  0
65a1i 11 . . 3  |-  ( ph  -> 
-u 1  =/=  0
)
7 fzfid 11314 . . . 4  |-  ( ph  ->  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  e.  Fin )
8 lgseisen.2 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
9 eldifi 3471 . . . . . . . . . 10  |-  ( Q  e.  ( Prime  \  {
2 } )  ->  Q  e.  Prime )
10 prmnn 13084 . . . . . . . . . 10  |-  ( Q  e.  Prime  ->  Q  e.  NN )
118, 9, 103syl 19 . . . . . . . . 9  |-  ( ph  ->  Q  e.  NN )
1211nnred 10017 . . . . . . . 8  |-  ( ph  ->  Q  e.  RR )
13 lgseisen.1 . . . . . . . . 9  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
14 eldifi 3471 . . . . . . . . 9  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  e.  Prime )
15 prmnn 13084 . . . . . . . . 9  |-  ( P  e.  Prime  ->  P  e.  NN )
1613, 14, 153syl 19 . . . . . . . 8  |-  ( ph  ->  P  e.  NN )
1712, 16nndivred 10050 . . . . . . 7  |-  ( ph  ->  ( Q  /  P
)  e.  RR )
1817adantr 453 . . . . . 6  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  /  P )  e.  RR )
19 2z 10314 . . . . . . . 8  |-  2  e.  ZZ
20 elfzelz 11061 . . . . . . . . 9  |-  ( u  e.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M )  ->  u  e.  ZZ )
2120adantl 454 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  u  e.  ZZ )
22 zmulcl 10326 . . . . . . . 8  |-  ( ( 2  e.  ZZ  /\  u  e.  ZZ )  ->  ( 2  x.  u
)  e.  ZZ )
2319, 21, 22sylancr 646 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  u )  e.  ZZ )
2423zred 10377 . . . . . 6  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  u )  e.  RR )
2518, 24remulcld 9118 . . . . 5  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  /  P
)  x.  ( 2  x.  u ) )  e.  RR )
2625flcld 11209 . . . 4  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e.  ZZ )
277, 26fsumzcl 12531 . . 3  |-  ( ph  -> 
sum_ u  e.  (
( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  e.  ZZ )
282, 6, 27expclzd 11530 . 2  |-  ( ph  ->  ( -u 1 ^
sum_ u  e.  (
( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) ) )  e.  CC )
29 fzfid 11314 . . . . . . 7  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
30 fzfid 11314 . . . . . . 7  |-  ( ph  ->  ( 1 ... N
)  e.  Fin )
31 xpfi 7380 . . . . . . 7  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ( 1 ... N
)  e.  Fin )  ->  ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin )
3229, 30, 31syl2anc 644 . . . . . 6  |-  ( ph  ->  ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin )
33 lgsquad.6 . . . . . . 7  |-  S  =  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  <  (
x  x.  Q ) ) }
34 opabssxp 4952 . . . . . . 7  |-  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  < 
( x  x.  Q
) ) }  C_  ( ( 1 ... M )  X.  (
1 ... N ) )
3533, 34eqsstri 3380 . . . . . 6  |-  S  C_  ( ( 1 ... M )  X.  (
1 ... N ) )
36 ssfi 7331 . . . . . 6  |-  ( ( ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin  /\  S  C_  ( ( 1 ... M )  X.  (
1 ... N ) ) )  ->  S  e.  Fin )
3732, 35, 36sylancl 645 . . . . 5  |-  ( ph  ->  S  e.  Fin )
38 ssrab2 3430 . . . . 5  |-  { z  e.  S  |  -.  2  ||  ( 1st `  z
) }  C_  S
39 ssfi 7331 . . . . 5  |-  ( ( S  e.  Fin  /\  { z  e.  S  |  -.  2  ||  ( 1st `  z ) }  C_  S )  ->  { z  e.  S  |  -.  2  ||  ( 1st `  z
) }  e.  Fin )
4037, 38, 39sylancl 645 . . . 4  |-  ( ph  ->  { z  e.  S  |  -.  2  ||  ( 1st `  z ) }  e.  Fin )
41 hashcl 11641 . . . 4  |-  ( { z  e.  S  |  -.  2  ||  ( 1st `  z ) }  e.  Fin  ->  ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } )  e.  NN0 )
4240, 41syl 16 . . 3  |-  ( ph  ->  ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } )  e.  NN0 )
43 expcl 11401 . . 3  |-  ( (
-u 1  e.  CC  /\  ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } )  e.  NN0 )  -> 
( -u 1 ^ ( # `
 { z  e.  S  |  -.  2  ||  ( 1st `  z
) } ) )  e.  CC )
441, 42, 43sylancr 646 . 2  |-  ( ph  ->  ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )  e.  CC )
4542nn0zd 10375 . . 3  |-  ( ph  ->  ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } )  e.  ZZ )
462, 6, 45expne0d 11531 . 2  |-  ( ph  ->  ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )  =/=  0 )
4744, 46recidd 9787 . . . 4  |-  ( ph  ->  ( ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )  x.  ( 1  /  ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) ) ) )  =  1 )
483div1i 9744 . . . . . . . . 9  |-  ( 1  /  1 )  =  1
4948negeqi 9301 . . . . . . . 8  |-  -u (
1  /  1 )  =  -u 1
50 divneg2 9740 . . . . . . . . 9  |-  ( ( 1  e.  CC  /\  1  e.  CC  /\  1  =/=  0 )  ->  -u (
1  /  1 )  =  ( 1  /  -u 1 ) )
513, 3, 4, 50mp3an 1280 . . . . . . . 8  |-  -u (
1  /  1 )  =  ( 1  /  -u 1 )
5249, 51eqtr3i 2460 . . . . . . 7  |-  -u 1  =  ( 1  /  -u 1 )
5352oveq1i 6093 . . . . . 6  |-  ( -u
1 ^ ( # `  { z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )  =  ( ( 1  /  -u 1
) ^ ( # `  { z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )
542, 6, 45exprecd 11533 . . . . . 6  |-  ( ph  ->  ( ( 1  /  -u 1 ) ^ ( # `
 { z  e.  S  |  -.  2  ||  ( 1st `  z
) } ) )  =  ( 1  / 
( -u 1 ^ ( # `
 { z  e.  S  |  -.  2  ||  ( 1st `  z
) } ) ) ) )
5553, 54syl5eq 2482 . . . . 5  |-  ( ph  ->  ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )  =  ( 1  /  ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) ) ) )
5655oveq2d 6099 . . . 4  |-  ( 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 ) } ) ) ) ) )
5737adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  S  e.  Fin )
58 ssrab2 3430 . . . . . . . . . . . 12  |-  { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u
) ) }  C_  S
59 ssfi 7331 . . . . . . . . . . . 12  |-  ( ( 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 )
6057, 58, 59sylancl 645 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u
) ) }  e.  Fin )
61 fveq2 5730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  v  ->  ( 1st `  z )  =  ( 1st `  v
) )
6261eqeq1d 2446 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  v  ->  (
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) )  <->  ( 1st `  v )  =  ( P  -  ( 2  x.  u ) ) ) )
6362elrab 3094 . . . . . . . . . . . . . . . . . . 19  |-  ( v  e.  { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u ) ) }  <->  ( v  e.  S  /\  ( 1st `  v )  =  ( P  -  ( 2  x.  u ) ) ) )
6463simprbi 452 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u ) ) }  ->  ( 1st `  v )  =  ( P  -  ( 2  x.  u ) ) )
6564ad2antll 711 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  ( 1st `  v )  =  ( P  -  (
2  x.  u ) ) )
6665oveq2d 6099 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) ) ) )
6716adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  NN )
6867nncnd 10018 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  CC )
6968adantrr 699 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  P  e.  CC )
7023zcnd 10378 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  u )  e.  CC )
7170adantrr 699 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  (
2  x.  u )  e.  CC )
7269, 71nncand 9418 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) )
7366, 72eqtrd 2470 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  ( P  -  ( 1st `  v ) )  =  ( 2  x.  u
) )
7473oveq1d 6098 . . . . . . . . . . . . . 14  |-  ( (
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
) )
7521zcnd 10378 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  u  e.  CC )
7675adantrr 699 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  u  e.  CC )
77 2cn 10072 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
7877a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  2  e.  CC )
79 2ne0 10085 . . . . . . . . . . . . . . . 16  |-  2  =/=  0
8079a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  2  =/=  0 )
8176, 78, 80divcan3d 9797 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  (
( 2  x.  u
)  /  2 )  =  u )
8274, 81eqtrd 2470 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  (
( P  -  ( 1st `  v ) )  /  2 )  =  u )
8382ralrimivva 2800 . . . . . . . . . . . 12  |-  ( 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 )
84 invdisj 4203 . . . . . . . . . . . 12  |-  ( 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 ) ) } )
8583, 84syl 16 . . . . . . . . . . 11  |-  ( ph  -> Disj  u  e.  ( (
( |_ `  ( M  /  2 ) )  +  1 ) ... M ) { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u
) ) } )
867, 60, 85hashiun 12603 . . . . . . . . . 10  |-  ( 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 ) ) } ) )
87 iunrab 4140 . . . . . . . . . . . 12  |-  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 ) ) }
88 eldifsni 3930 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  =/=  2 )
8913, 88syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  P  =/=  2 )
9089necomd 2689 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  2  =/=  P )
9190neneqd 2619 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  -.  2  =  P )
9291ad2antrr 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  -.  2  =  P )
93 uzid 10502 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  e.  ZZ  ->  2  e.  ( ZZ>= `  2 )
)
9419, 93ax-mp 8 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  ( ZZ>= `  2 )
9513, 14syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  P  e.  Prime )
9695ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  Prime )
97 dvdsprm 13101 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2  e.  ( ZZ>= ` 
2 )  /\  P  e.  Prime )  ->  (
2  ||  P  <->  2  =  P ) )
9894, 96, 97sylancr 646 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  ||  P  <->  2  =  P ) )
9992, 98mtbird 294 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  -.  2  ||  P )
10016ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  NN )
101100nncnd 10018 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  CC )
10223adantlr 697 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  u )  e.  ZZ )
103102zcnd 10378 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  u )  e.  CC )
104101, 103npcand 9417 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  -  (
2  x.  u ) )  +  ( 2  x.  u ) )  =  P )
105104breq2d 4226 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  ||  ( ( P  -  ( 2  x.  u ) )  +  ( 2  x.  u ) )  <->  2  ||  P ) )
10699, 105mtbird 294 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  -.  2  ||  ( ( P  -  ( 2  x.  u ) )  +  ( 2  x.  u
) ) )
10720adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  u  e.  ZZ )
108 dvdsmul1 12873 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2  e.  ZZ  /\  u  e.  ZZ )  ->  2  ||  ( 2  x.  u ) )
10919, 107, 108sylancr 646 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  2  ||  ( 2  x.  u
) )
11019a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  2  e.  ZZ )
111100nnzd 10376 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  ZZ )
112111, 102zsubcld 10382 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  -  ( 2  x.  u ) )  e.  ZZ )
113 dvds2add 12883 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) ) )
114110, 112, 102, 113syl3anc 1185 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) ) )
115109, 114mpan2d 657 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  ||  ( P  -  ( 2  x.  u ) )  -> 
2  ||  ( ( P  -  ( 2  x.  u ) )  +  ( 2  x.  u ) ) ) )
116106, 115mtod 171 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  -.  2  ||  ( P  -  ( 2  x.  u
) ) )
117 breq2 4218 . . . . . . . . . . . . . . . . 17  |-  ( ( 1st `  z )  =  ( P  -  ( 2  x.  u
) )  ->  (
2  ||  ( 1st `  z )  <->  2  ||  ( P  -  (
2  x.  u ) ) ) )
118117notbid 287 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  z )  =  ( P  -  ( 2  x.  u
) )  ->  ( -.  2  ||  ( 1st `  z )  <->  -.  2  ||  ( P  -  (
2  x.  u ) ) ) )
119116, 118syl5ibrcom 215 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) )  ->  -.  2  ||  ( 1st `  z ) ) )
120119rexlimdva 2832 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  S )  ->  ( E. u  e.  (
( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) ( 1st `  z
)  =  ( P  -  ( 2  x.  u ) )  ->  -.  2  ||  ( 1st `  z ) ) )
121 simpr 449 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  S )  ->  z  e.  S )
12235, 121sseldi 3348 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  S )  ->  z  e.  ( ( 1 ... M )  X.  (
1 ... N ) ) )
123 xp1st 6378 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( ( 1 ... M )  X.  ( 1 ... N
) )  ->  ( 1st `  z )  e.  ( 1 ... M
) )
124122, 123syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  S )  ->  ( 1st `  z )  e.  ( 1 ... M
) )
125 elfzelz 11061 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  z )  e.  ( 1 ... M )  ->  ( 1st `  z )  e.  ZZ )
126 odd2np1 12910 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  z )  e.  ZZ  ->  ( -.  2  ||  ( 1st `  z )  <->  E. n  e.  ZZ  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )
127124, 125, 1263syl 19 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  S )  ->  ( -.  2  ||  ( 1st `  z )  <->  E. n  e.  ZZ  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )
128 lgsquad.4 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  M  =  ( ( P  - 
1 )  /  2
)
129 oddprm 13191 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
13013, 129syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN )
131128, 130syl5eqel 2522 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  NN )
132131nnred 10017 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  M  e.  RR )
133132ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  M  e.  RR )
134133rehalfcld 10216 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  / 
2 )  e.  RR )
135 reflcl 11207 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( M  /  2 )  e.  RR  ->  ( |_ `  ( M  / 
2 ) )  e.  RR )
136134, 135syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( |_ `  ( M  /  2
) )  e.  RR )
137131ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  M  e.  NN )
138137nnzd 10376 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  M  e.  ZZ )
139 simprl 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  n  e.  ZZ )
140138, 139zsubcld 10382 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  -  n )  e.  ZZ )
141140zred 10377 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  -  n )  e.  RR )
142 flle 11210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( M  /  2 )  e.  RR  ->  ( |_ `  ( M  / 
2 ) )  <_ 
( M  /  2
) )
143134, 142syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( |_ `  ( M  /  2
) )  <_  ( M  /  2 ) )
144 zre 10288 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ZZ  ->  n  e.  RR )
145144ad2antrl 710 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  n  e.  RR )
146 simprr 735 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) )
147124adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 1st `  z
)  e.  ( 1 ... M ) )
148146, 147eqeltrd 2512 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  +  1 )  e.  ( 1 ... M ) )
149 elfzle2 11063 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 2  x.  n
)  +  1 )  e.  ( 1 ... M )  ->  (
( 2  x.  n
)  +  1 )  <_  M )
150148, 149syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  +  1 )  <_  M
)
151 zmulcl 10326 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 2  e.  ZZ  /\  n  e.  ZZ )  ->  ( 2  x.  n
)  e.  ZZ )
15219, 139, 151sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  n )  e.  ZZ )
153 zltp1le 10327 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 2  x.  n
)  e.  ZZ  /\  M  e.  ZZ )  ->  ( ( 2  x.  n )  <  M  <->  ( ( 2  x.  n
)  +  1 )  <_  M ) )
154152, 138, 153syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  < 
M  <->  ( ( 2  x.  n )  +  1 )  <_  M
) )
155150, 154mpbird 225 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  n )  <  M
)
156 2re 10071 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  2  e.  RR
157156a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  2  e.  RR )
158 2pos 10084 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  <  2
159158a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  0  <  2
)
160 ltmuldiv2 9883 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  RR  /\  M  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( 2  x.  n )  < 
M  <->  n  <  ( M  /  2 ) ) )
161145, 133, 157, 159, 160syl112anc 1189 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  < 
M  <->  n  <  ( M  /  2 ) ) )
162155, 161mpbid 203 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  n  <  ( M  /  2 ) )
163134recnd 9116 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  / 
2 )  e.  CC )
164163, 163pncan2d 9415 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( ( M  /  2 )  +  ( M  / 
2 ) )  -  ( M  /  2
) )  =  ( M  /  2 ) )
165131nncnd 10018 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  M  e.  CC )
166165ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  M  e.  CC )
1671662halvesd 10215 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( M  /  2 )  +  ( M  /  2
) )  =  M )
168167oveq1d 6098 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( ( M  /  2 )  +  ( M  / 
2 ) )  -  ( M  /  2
) )  =  ( M  -  ( M  /  2 ) ) )
169164, 168eqtr3d 2472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  / 
2 )  =  ( M  -  ( M  /  2 ) ) )
170162, 169breqtrd 4238 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  n  <  ( M  -  ( M  /  2 ) ) )
171145, 133, 134, 170ltsub13d 9634 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  / 
2 )  <  ( M  -  n )
)
172136, 134, 141, 143, 171lelttrd 9230 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( |_ `  ( M  /  2
) )  <  ( M  -  n )
)
173134flcld 11209 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( |_ `  ( M  /  2
) )  e.  ZZ )
174 zltp1le 10327 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( |_ `  ( M  /  2 ) )  e.  ZZ  /\  ( M  -  n )  e.  ZZ )  ->  (
( |_ `  ( M  /  2 ) )  <  ( M  -  n )  <->  ( ( |_ `  ( M  / 
2 ) )  +  1 )  <_  ( M  -  n )
) )
175173, 140, 174syl2anc 644 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( |_
`  ( M  / 
2 ) )  < 
( M  -  n
)  <->  ( ( |_
`  ( M  / 
2 ) )  +  1 )  <_  ( M  -  n )
) )
176172, 175mpbid 203 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( |_
`  ( M  / 
2 ) )  +  1 )  <_  ( M  -  n )
)
17777mul01i 9258 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  x.  0 )  =  0
178 zcn 10289 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  e.  ZZ  ->  n  e.  CC )
179178ad2antrl 710 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  n  e.  CC )
180 mulcl 9076 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 2  e.  CC  /\  n  e.  CC )  ->  ( 2  x.  n
)  e.  CC )
18177, 179, 180sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  n )  e.  CC )
182 pncan 9313 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 2  x.  n
)  e.  CC  /\  1  e.  CC )  ->  ( ( ( 2  x.  n )  +  1 )  -  1 )  =  ( 2  x.  n ) )
183181, 3, 182sylancl 645 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( ( 2  x.  n )  +  1 )  - 
1 )  =  ( 2  x.  n ) )
184 elfznn 11082 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 2  x.  n
)  +  1 )  e.  ( 1 ... M )  ->  (
( 2  x.  n
)  +  1 )  e.  NN )
185 nnm1nn0 10263 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 2  x.  n
)  +  1 )  e.  NN  ->  (
( ( 2  x.  n )  +  1 )  -  1 )  e.  NN0 )
186148, 184, 1853syl 19 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( ( 2  x.  n )  +  1 )  - 
1 )  e.  NN0 )
187183, 186eqeltrrd 2513 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  n )  e.  NN0 )
188187nn0ge0d 10279 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  0  <_  (
2  x.  n ) )
189177, 188syl5eqbr 4247 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  0 )  <_  (
2  x.  n ) )
190 0re 9093 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
191190a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  0  e.  RR )
192 lemul2 9865 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0  e.  RR  /\  n  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( 0  <_  n 
<->  ( 2  x.  0 )  <_  ( 2  x.  n ) ) )
193191, 145, 157, 159, 192syl112anc 1189 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 0  <_  n 
<->  ( 2  x.  0 )  <_  ( 2  x.  n ) ) )
194189, 193mpbird 225 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  0  <_  n
)
195133, 145subge02d 9620 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 0  <_  n 
<->  ( M  -  n
)  <_  M )
)
196194, 195mpbid 203 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  -  n )  <_  M
)
197173peano2zd 10380 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( |_
`  ( M  / 
2 ) )  +  1 )  e.  ZZ )
198 elfz 11051 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 )
) )
199140, 197, 138, 198syl3anc 1185 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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
) ) )
200176, 196, 199mpbir2and 890 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  -  n )  e.  ( ( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) )
20195ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  P  e.  Prime )
202201, 15syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  P  e.  NN )
203202nncnd 10018 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  P  e.  CC )
204 peano2cn 9240 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2  x.  n )  e.  CC  ->  (
( 2  x.  n
)  +  1 )  e.  CC )
205181, 204syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  +  1 )  e.  CC )
206203, 205nncand 9418 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( P  -  ( P  -  (
( 2  x.  n
)  +  1 ) ) )  =  ( ( 2  x.  n
)  +  1 ) )
2073a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  1  e.  CC )
208203, 181, 207sub32d 9445 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( P  -  ( 2  x.  n ) )  - 
1 )  =  ( ( P  -  1 )  -  ( 2  x.  n ) ) )
209203, 181, 207subsub4d 9444 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( P  -  ( 2  x.  n ) )  - 
1 )  =  ( P  -  ( ( 2  x.  n )  +  1 ) ) )
21077a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  2  e.  CC )
211210, 166, 179subdid 9491 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  ( M  -  n
) )  =  ( ( 2  x.  M
)  -  ( 2  x.  n ) ) )
212128oveq2i 6094 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2  x.  M )  =  ( 2  x.  (
( P  -  1 )  /  2 ) )
21316nnzd 10376 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  P  e.  ZZ )
214213ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  P  e.  ZZ )
215 peano2zm 10322 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( P  e.  ZZ  ->  ( P  -  1 )  e.  ZZ )
216214, 215syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( P  - 
1 )  e.  ZZ )
217216zcnd 10378 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( P  - 
1 )  e.  CC )
21879a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  2  =/=  0
)
219217, 210, 218divcan2d 9794 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  ( ( P  - 
1 )  /  2
) )  =  ( P  -  1 ) )
220212, 219syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  M )  =  ( P  -  1 ) )
221220oveq1d 6098 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  M )  -  ( 2  x.  n
) )  =  ( ( P  -  1 )  -  ( 2  x.  n ) ) )
222211, 221eqtr2d 2471 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( P  -  1 )  -  ( 2  x.  n
) )  =  ( 2  x.  ( M  -  n ) ) )
223208, 209, 2223eqtr3d 2478 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( P  -  ( ( 2  x.  n )  +  1 ) )  =  ( 2  x.  ( M  -  n ) ) )
224223oveq2d 6099 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( P  -  ( P  -  (
( 2  x.  n
)  +  1 ) ) )  =  ( P  -  ( 2  x.  ( M  -  n ) ) ) )
225206, 224, 1463eqtr3rd 2479 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 1st `  z
)  =  ( P  -  ( 2  x.  ( M  -  n
) ) ) )
226 oveq2 6091 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  ( M  -  n )  ->  (
2  x.  u )  =  ( 2  x.  ( M  -  n
) ) )
227226oveq2d 6099 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  ( M  -  n )  ->  ( P  -  ( 2  x.  u ) )  =  ( P  -  ( 2  x.  ( M  -  n )
) ) )
228227eqeq2d 2449 . . . . . . . . . . . . . . . . . 18  |-  ( u  =  ( M  -  n )  ->  (
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) )  <->  ( 1st `  z )  =  ( P  -  ( 2  x.  ( M  -  n ) ) ) ) )
229228rspcev 3054 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) )
230200, 225, 229syl2anc 644 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
231230rexlimdvaa 2833 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) )
232127, 231sylbid 208 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  S )  ->  ( -.  2  ||  ( 1st `  z )  ->  E. u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) ( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) ) )
233120, 232impbid 185 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  S )  ->  ( E. u  e.  (
( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) ( 1st `  z
)  =  ( P  -  ( 2  x.  u ) )  <->  -.  2  ||  ( 1st `  z
) ) )
234233rabbidva 2949 . . . . . . . . . . . 12  |-  ( ph  ->  { z  e.  S  |  E. u  e.  ( ( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) ( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) }  =  { z  e.  S  |  -.  2  ||  ( 1st `  z
) } )
23587, 234syl5eq 2482 . . . . . . . . . . 11  |-  ( ph  ->  U_ u  e.  ( ( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) { z  e.  S  |  ( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) }  =  { z  e.  S  |  -.  2  ||  ( 1st `  z
) } )
236235fveq2d 5734 . . . . . . . . . 10  |-  ( ph  ->  ( # `  U_ u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u ) ) } )  =  (
# `  { z  e.  S  |  -.  2  ||  ( 1st `  z
) } ) )
23733relopabi 5002 . . . . . . . . . . . . . . 15  |-  Rel  S
238 relss 4965 . . . . . . . . . . . . . . 15  |-  ( { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } 
C_  S  ->  ( Rel  S  ->  Rel  { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u
) ) } ) )
23958, 237, 238mp2 9 . . . . . . . . . . . . . 14  |-  Rel  {
z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) }
240 relxp 4985 . . . . . . . . . . . . . 14  |-  Rel  ( { ( P  -  ( 2  x.  u
) ) }  X.  ( 1 ... (
( 2  x.  N
)  -  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) )
24133eleq2i 2502 . . . . . . . . . . . . . . . . . 18  |-  ( <.
x ,  y >.  e.  S  <->  <. x ,  y
>.  e.  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  < 
( x  x.  Q
) ) } )
242 opabid 4463 . . . . . . . . . . . . . . . . . 18  |-  ( <.
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 ) ) )
243241, 242bitri 242 . . . . . . . . . . . . . . . . 17  |-  ( <.
x ,  y >.  e.  S  <->  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) )
244 anass 632 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) ) ) )
24526peano2zd 10380 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  +  1 )  e.  ZZ )
246245zred 10377 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  +  1 )  e.  RR )
247246adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  (
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  +  1 )  e.  RR )
24812ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  Q  e.  RR )
249 nnre 10009 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  NN  ->  y  e.  RR )
250249adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  y  e.  RR )
251 lesub 9509 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( |_ `  ( ( 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 ) ) ) )
252247, 248, 250, 251syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 ) ) ) )
25312adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  Q  e.  RR )
254253recnd 9116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  Q  e.  CC )
25568, 254mulcomd 9111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  x.  Q )  =  ( Q  x.  P ) )
25670, 254mulcomd 9111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 2  x.  u
)  x.  Q )  =  ( Q  x.  ( 2  x.  u
) ) )
25767nnne0d 10046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  =/=  0 )
258254, 68, 257divcan1d 9793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  /  P
)  x.  P )  =  Q )
259258oveq1d 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( ( Q  /  P )  x.  P
)  x.  ( 2  x.  u ) )  =  ( Q  x.  ( 2  x.  u
) ) )
26018recnd 9116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  /  P )  e.  CC )
261260, 68, 70mul32d 9278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( ( Q  /  P )  x.  P
)  x.  ( 2  x.  u ) )  =  ( ( ( Q  /  P )  x.  ( 2  x.  u ) )  x.  P ) )
262256, 259, 2613eqtr2d 2476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 2  x.  u
)  x.  Q )  =  ( ( ( Q  /  P )  x.  ( 2  x.  u ) )  x.  P ) )
263255, 262oveq12d 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
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
) ) )
26468, 70, 254subdird 9492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  -  (
2  x.  u ) )  x.  Q )  =  ( ( P  x.  Q )  -  ( ( 2  x.  u )  x.  Q
) ) )
26525recnd 9116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  /  P
)  x.  ( 2  x.  u ) )  e.  CC )
266254, 265, 68subdird 9492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
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
) ) )
267263, 264, 2663eqtr4d 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  -  (
2  x.  u ) )  x.  Q )  =  ( ( Q  -  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  x.  P ) )
268267adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 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 ) )
269268breq2d 4226 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 ) ) )
27025adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  (
( Q  /  P
)  x.  ( 2  x.  u ) )  e.  RR )
271248, 270resubcld 9467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  ( Q  -  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e.  RR )
27267adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  P  e.  NN )
273272nnred 10017 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  P  e.  RR )
274272nngt0d 10045 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  0  <  P )
275 ltmul1 9862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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 ) ) )
276250, 271, 273, 274, 275syl112anc 1189 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 ) ) )
277 ltsub13 9511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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 )
) )
278250, 248, 270, 277syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 )
) )
279269, 276, 2783bitr2d 274 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 )
) )
28011adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  Q  e.  NN )
281280nnzd 10376 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  Q  e.  ZZ )
282 nnz 10305 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  NN  ->  y  e.  ZZ )
283 zsubcl 10321 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Q  e.  ZZ  /\  y  e.  ZZ )  ->  ( Q  -  y
)  e.  ZZ )
284281, 282, 283syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  ( Q  -  y )  e.  ZZ )
285 fllt 11217 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
) )
286270, 284, 285syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 )
) )
28726adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e.  ZZ )
288 zltp1le 10327 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( |_ `  (
( 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 )
) )
289287, 284, 288syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 )
) )
290279, 286, 2893bitrd 272 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 )
) )
291 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  N  =  ( ( Q  - 
1 )  /  2
)
292291oveq2i 6094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 2  x.  N )  =  ( 2  x.  (
( Q  -  1 )  /  2 ) )
293 peano2rem 9369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Q  e.  RR  ->  ( Q  -  1 )  e.  RR )
294253, 293syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  -  1 )  e.  RR )
295294recnd 9116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  -  1 )  e.  CC )
29677a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  2  e.  CC )
29779a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  2  =/=  0 )
298295, 296, 297divcan2d 9794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  ( ( Q  -  1 )  /  2 ) )  =  ( Q  - 
1 ) )
299292, 298syl5eq 2482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  N )  =  ( Q  - 
1 ) )
300299oveq1d 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 2  x.  N
)  -  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) )  =  ( ( Q  -  1 )  -  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u ) ) ) ) )
3013a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  1  e.  CC )
30226zcnd 10378 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e.  CC )
303254, 301, 302sub32d 9445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  -  1 )  -  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) )  =  ( ( Q  -  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) ) )  - 
1 ) )
304254, 302, 301subsub4d 9444 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  -  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) )  -  1 )  =  ( Q  -  (
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  +  1 ) ) )
305300, 303, 3043eqtrd 2474 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 2  x.  N
)  -  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) )  =  ( Q  -  ( ( |_ `  ( ( Q  /  P )  x.  (
2  x.  u ) ) )  +  1 ) ) )
306305adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 ) ) )
307306breq2d 4226 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 ) ) ) )
308252, 290, 3073bitr4d 278 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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
) ) ) ) ) )
309308anbi2d 686 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) ) ) ) ) ) )
310 2nn 10135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  2  e.  NN
311 oddprm 13191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Q  e.  ( Prime  \  {
2 } )  -> 
( ( Q  - 
1 )  /  2
)  e.  NN )
3128, 311syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( ( Q  - 
1 )  /  2
)  e.  NN )
313291, 312syl5eqel 2522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  N  e.  NN )
314 nnmulcl 10025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 2  e.  NN  /\  N  e.  NN )  ->  ( 2  x.  N
)  e.  NN )
315310, 313, 314sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( 2  x.  N
)  e.  NN )
316315adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  N )  e.  NN )
317316nnred 10017 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  N )  e.  RR )
318313adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  N  e.  NN )
319318nnred 10017 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  N  e.  RR )
32026zred 10377 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e.  RR )
321313nncnd 10018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  N  e.  CC )
322321adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  N  e.  CC )
3233222timesd 10212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  N )  =  ( N  +  N ) )
324323oveq1d 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 2  x.  N
)  -  N )  =  ( ( N  +  N )  -  N ) )
325322, 322pncan2d 9415 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( N  +  N
)  -  N )  =  N )
326324, 325eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 2  x.  N
)  -  N )  =  N )
327253rehalfcld 10216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  /  2 )  e.  RR )
328253ltm1d 9945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  -  1 )  <  Q )
329156a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  2  e.  RR )
330158a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  0  <  2 )
331 ltdiv1 9876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( Q  -  1 )  e.  RR  /\  Q  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( Q  -  1 )  < 
Q  <->  ( ( Q  -  1 )  / 
2 )  <  ( Q  /  2 ) ) )
332294, 253, 329, 330, 331syl112anc 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  -  1 )  <  Q  <->  ( ( Q  -  1 )  /  2 )  < 
( Q  /  2
) ) )
333328, 332mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  -  1 )  /  2 )  <  ( Q  / 
2 ) )
334291, 333syl5eqbr 4247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  N  <  ( Q  /  2
) )
335319, 327, 334ltled 9223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  N  <_  ( Q  /  2
) )
336254, 296, 68, 297div32d 9815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  /  2
)  x.  P )  =  ( Q  x.  ( P  /  2
) ) )
337132adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  M  e.  RR )
338337rehalfcld 10216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( M  /  2 )  e.  RR )
339 peano2re 9241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( |_ `  ( M  /  2 ) )  e.  RR  ->  (
( |_ `  ( M  /  2 ) )  +  1 )  e.  RR )
340338, 135, 3393syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( |_ `  ( M  /  2 ) )  +  1 )  e.  RR )
34121zred 10377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  u  e.  RR )
342 flltp1 11211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( M  /  2 )  e.  RR  ->  ( M  /  2 )  < 
( ( |_ `  ( M  /  2
) )  +  1 ) )
343338, 342syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( M  /  2 )  < 
( ( |_ `  ( M  /  2
) )  +  1 ) )
344 elfzle1 11062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( u  e.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M )  ->  (
( |_ `  ( M  /  2 ) )  +  1 )  <_  u )
345344adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( |_ `  ( M  /  2 ) )  +  1 )  <_  u )
346338, 340, 341, 343, 345ltletrd 9232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( M  /  2 )  < 
u )
347 ltdivmul 9884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( M  e.  RR  /\  u  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( M  /  2 )  < 
u  <->  M  <  ( 2  x.  u ) ) )
348337, 341, 329, 330, 347syl112anc 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( M  /  2
)  <  u  <->  M  <  ( 2  x.  u ) ) )
349346, 348mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  M  <  ( 2  x.  u
) )
350128, 349syl5eqbrr 4248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  -  1 )  /  2 )  <  ( 2  x.  u ) )
35167nnred 10017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  RR )
352 peano2rem 9369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( P  e.  RR  ->  ( P  -  1 )  e.  RR )
353351, 352syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  -  1 )  e.  RR )
354 ltdivmul 9884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( 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 ) ) ) )
355353, 24, 329, 330, 354syl112anc 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( ( P  - 
1 )  /  2
)  <  ( 2  x.  u )  <->  ( P  -  1 )  < 
( 2  x.  (
2  x.  u ) ) ) )
356350, 355mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  -  1 )  <  ( 2  x.  ( 2  x.  u
) ) )
357213adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  ZZ )
358 zmulcl 10326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 2  e.  ZZ  /\  ( 2  x.  u
)  e.  ZZ )  ->  ( 2  x.  ( 2  x.  u
) )  e.  ZZ )
35919, 23, 358sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  ( 2  x.  u ) )  e.  ZZ )
360 zlem1lt 10329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( P  e.  ZZ  /\  ( 2  x.  (
2  x.  u ) )  e.  ZZ )  ->  ( P  <_ 
( 2  x.  (
2  x.  u ) )  <->  ( P  - 
1 )  <  (
2  x.  ( 2  x.  u ) ) ) )
361357, 359, 360syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  <_  ( 2  x.  ( 2  x.  u
) )  <->  ( P  -  1 )  < 
( 2  x.  (
2  x.  u ) ) ) )
362356, 361mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  <_  ( 2  x.  (
2  x.  u ) ) )
363 ledivmul 9885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( P  e.  RR  /\  ( 2  x.  u
)  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( ( P  /  2 )  <_ 
( 2  x.  u
)  <->  P  <_  ( 2  x.  ( 2  x.  u ) ) ) )
364351, 24, 329, 330, 363syl112anc 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  /  2
)  <_  ( 2  x.  u )  <->  P  <_  ( 2  x.  ( 2  x.  u ) ) ) )
365362, 364mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  /  2 )  <_ 
( 2  x.  u
) )
366351rehalfcld 10216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  /  2 )  e.  RR )
367280nngt0d 10045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  0  <  Q )
368 lemul2 9865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( 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 ) ) ) )
369366, 24, 253, 367, 368syl112anc 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  /  2
)  <_  ( 2  x.  u )  <->  ( Q  x.  ( P  /  2
) )  <_  ( Q  x.  ( 2  x.  u ) ) ) )
370365, 369mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  x.  ( P  /  2 ) )  <_  ( Q  x.  ( 2  x.  u
) ) )
371336, 370eqbrtrd 4234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  /  2
)  x.  P )  <_  ( Q  x.  ( 2  x.  u
) ) )
372253, 24remulcld 9118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  x.  ( 2  x.  u ) )  e.  RR )
37367nngt0d 10045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  0  <  P )
374 lemuldiv 9891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( 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
) ) )
375327, 372, 351, 373, 374syl112anc 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( ( Q  / 
2 )  x.  P
)  <_  ( Q  x.  ( 2  x.  u
) )  <->  ( Q  /  2 )  <_ 
( ( Q  x.  ( 2  x.  u
) )  /  P
) ) )
376371, 375mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  /  2 )  <_ 
( ( Q  x.  ( 2  x.  u
) )  /  P
) )
377254, 70, 68, 257div23d 9829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  x.  (
2  x.  u ) )  /  P )  =  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )
378376, 377breqtrd 4238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  /  2 )  <_ 
( ( Q  /  P )  x.  (
2  x.  u ) ) )
379319, 327, 25, 335, 378letrd 9229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  (