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

Theorem lgsquadlem1 20609
Description: Lemma for lgsquad 20612. 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 9829 . . . . . 6  |-  -u 1  e.  CC
2 fzfid 11051 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
3 fzfid 11051 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... N
)  e.  Fin )
4 xpfi 7144 . . . . . . . . . 10  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ( 1 ... N
)  e.  Fin )  ->  ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin )
52, 3, 4syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin )
6 lgsquad.6 . . . . . . . . . 10  |-  S  =  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  <  (
x  x.  Q ) ) }
7 opabssxp 4778 . . . . . . . . . 10  |-  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  < 
( x  x.  Q
) ) }  C_  ( ( 1 ... M )  X.  (
1 ... N ) )
86, 7eqsstri 3221 . . . . . . . . 9  |-  S  C_  ( ( 1 ... M )  X.  (
1 ... N ) )
9 ssfi 7099 . . . . . . . . 9  |-  ( ( ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin  /\  S  C_  ( ( 1 ... M )  X.  (
1 ... N ) ) )  ->  S  e.  Fin )
105, 8, 9sylancl 643 . . . . . . . 8  |-  ( ph  ->  S  e.  Fin )
11 ssrab2 3271 . . . . . . . 8  |-  { z  e.  S  |  -.  2  ||  ( 1st `  z
) }  C_  S
12 ssfi 7099 . . . . . . . 8  |-  ( ( S  e.  Fin  /\  { z  e.  S  |  -.  2  ||  ( 1st `  z ) }  C_  S )  ->  { z  e.  S  |  -.  2  ||  ( 1st `  z
) }  e.  Fin )
1310, 11, 12sylancl 643 . . . . . . 7  |-  ( ph  ->  { z  e.  S  |  -.  2  ||  ( 1st `  z ) }  e.  Fin )
14 hashcl 11366 . . . . . . 7  |-  ( { z  e.  S  |  -.  2  ||  ( 1st `  z ) }  e.  Fin  ->  ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } )  e.  NN0 )
1513, 14syl 15 . . . . . 6  |-  ( ph  ->  ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } )  e.  NN0 )
16 expcl 11137 . . . . . 6  |-  ( (
-u 1  e.  CC  /\  ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } )  e.  NN0 )  -> 
( -u 1 ^ ( # `
 { z  e.  S  |  -.  2  ||  ( 1st `  z
) } ) )  e.  CC )
171, 15, 16sylancr 644 . . . . 5  |-  ( ph  ->  ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )  e.  CC )
181a1i 10 . . . . . 6  |-  ( ph  -> 
-u 1  e.  CC )
19 ax-1cn 8811 . . . . . . . 8  |-  1  e.  CC
20 ax-1ne0 8822 . . . . . . . 8  |-  1  =/=  0
2119, 20negne0i 9137 . . . . . . 7  |-  -u 1  =/=  0
2221a1i 10 . . . . . 6  |-  ( ph  -> 
-u 1  =/=  0
)
2315nn0zd 10131 . . . . . 6  |-  ( ph  ->  ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } )  e.  ZZ )
2418, 22, 23expne0d 11267 . . . . 5  |-  ( ph  ->  ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )  =/=  0 )
2517, 24recidd 9547 . . . 4  |-  ( ph  ->  ( ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )  x.  ( 1  /  ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) ) ) )  =  1 )
2619div1i 9504 . . . . . . . . 9  |-  ( 1  /  1 )  =  1
2726negeqi 9061 . . . . . . . 8  |-  -u (
1  /  1 )  =  -u 1
28 divneg2 9500 . . . . . . . . 9  |-  ( ( 1  e.  CC  /\  1  e.  CC  /\  1  =/=  0 )  ->  -u (
1  /  1 )  =  ( 1  /  -u 1 ) )
2919, 19, 20, 28mp3an 1277 . . . . . . . 8  |-  -u (
1  /  1 )  =  ( 1  /  -u 1 )
3027, 29eqtr3i 2318 . . . . . . 7  |-  -u 1  =  ( 1  /  -u 1 )
3130oveq1i 5884 . . . . . 6  |-  ( -u
1 ^ ( # `  { z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )  =  ( ( 1  /  -u 1
) ^ ( # `  { z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )
3218, 22, 23exprecd 11269 . . . . . 6  |-  ( ph  ->  ( ( 1  /  -u 1 ) ^ ( # `
 { z  e.  S  |  -.  2  ||  ( 1st `  z
) } ) )  =  ( 1  / 
( -u 1 ^ ( # `
 { z  e.  S  |  -.  2  ||  ( 1st `  z
) } ) ) ) )
3331, 32syl5eq 2340 . . . . 5  |-  ( ph  ->  ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) )  =  ( 1  /  ( -u 1 ^ ( # `  {
z  e.  S  |  -.  2  ||  ( 1st `  z ) } ) ) ) )
3433oveq2d 5890 . . . 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 ) } ) ) ) ) )
35 fzfid 11051 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  e.  Fin )
3610adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  S  e.  Fin )
37 ssrab2 3271 . . . . . . . . . . . 12  |-  { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u
) ) }  C_  S
38 ssfi 7099 . . . . . . . . . . . 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 )
3936, 37, 38sylancl 643 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u
) ) }  e.  Fin )
40 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  =  v  ->  ( 1st `  z )  =  ( 1st `  v
) )
4140eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  v  ->  (
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) )  <->  ( 1st `  v )  =  ( P  -  ( 2  x.  u ) ) ) )
4241elrab 2936 . . . . . . . . . . . . . . . . . . . 20  |-  ( v  e.  { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u ) ) }  <->  ( v  e.  S  /\  ( 1st `  v )  =  ( P  -  ( 2  x.  u ) ) ) )
4342simprbi 450 . . . . . . . . . . . . . . . . . . 19  |-  ( v  e.  { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u ) ) }  ->  ( 1st `  v )  =  ( P  -  ( 2  x.  u ) ) )
4443ad2antll 709 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  ( 1st `  v )  =  ( P  -  (
2  x.  u ) ) )
4544oveq2d 5890 . . . . . . . . . . . . . . . . 17  |-  ( (
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 ) ) ) )
46 lgseisen.1 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
47 eldifi 3311 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  e.  Prime )
48 prmnn 12777 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  Prime  ->  P  e.  NN )
4946, 47, 483syl 18 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  P  e.  NN )
5049adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  NN )
5150nncnd 9778 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  CC )
5251adantrr 697 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  P  e.  CC )
53 2z 10070 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  ZZ
54 elfzelz 10814 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  e.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M )  ->  u  e.  ZZ )
5554adantl 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  u  e.  ZZ )
56 zmulcl 10082 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  ZZ  /\  u  e.  ZZ )  ->  ( 2  x.  u
)  e.  ZZ )
5753, 55, 56sylancr 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  u )  e.  ZZ )
5857zcnd 10134 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  u )  e.  CC )
5958adantrr 697 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  (
2  x.  u )  e.  CC )
6052, 59nncand 9178 . . . . . . . . . . . . . . . . 17  |-  ( (
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 ) )
6145, 60eqtrd 2328 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  ( P  -  ( 1st `  v ) )  =  ( 2  x.  u
) )
6261oveq1d 5889 . . . . . . . . . . . . . . 15  |-  ( (
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
) )
6355zcnd 10134 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  u  e.  CC )
6463adantrr 697 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  u  e.  CC )
65 2cn 9832 . . . . . . . . . . . . . . . . 17  |-  2  e.  CC
6665a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  2  e.  CC )
67 2ne0 9845 . . . . . . . . . . . . . . . . 17  |-  2  =/=  0
6867a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  2  =/=  0 )
6964, 66, 68divcan3d 9557 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  (
( 2  x.  u
)  /  2 )  =  u )
7062, 69eqtr2d 2329 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  u  =  ( ( P  -  ( 1st `  v
) )  /  2
) )
7170eqcomd 2301 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
)  /\  v  e.  { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } ) )  ->  (
( P  -  ( 1st `  v ) )  /  2 )  =  u )
7271ralrimivva 2648 . . . . . . . . . . . 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 )
73 invdisj 4028 . . . . . . . . . . . 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 ) ) } )
7472, 73syl 15 . . . . . . . . . . 11  |-  ( ph  -> Disj  u  e.  ( (
( |_ `  ( M  /  2 ) )  +  1 ) ... M ) { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u
) ) } )
7535, 39, 74hashiun 12296 . . . . . . . . . 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 ) ) } ) )
76 iunrab 3965 . . . . . . . . . . . 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 ) ) }
77 eldifsni 3763 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  =/=  2 )
7846, 77syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  P  =/=  2 )
7978necomd 2542 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  2  =/=  P )
8079neneqd 2475 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  -.  2  =  P )
8180ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  -.  2  =  P )
82 uzid 10258 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  e.  ZZ  ->  2  e.  ( ZZ>= `  2 )
)
8353, 82ax-mp 8 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  ( ZZ>= `  2 )
8446, 47syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  P  e.  Prime )
8584ad2antrr 706 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  Prime )
86 dvdsprm 12794 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2  e.  ( ZZ>= ` 
2 )  /\  P  e.  Prime )  ->  (
2  ||  P  <->  2  =  P ) )
8783, 85, 86sylancr 644 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  ||  P  <->  2  =  P ) )
8881, 87mtbird 292 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  -.  2  ||  P )
8949ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  NN )
9089nncnd 9778 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  CC )
9157adantlr 695 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  u )  e.  ZZ )
9291zcnd 10134 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  u )  e.  CC )
9390, 92npcand 9177 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  -  (
2  x.  u ) )  +  ( 2  x.  u ) )  =  P )
9493breq2d 4051 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  ||  ( ( P  -  ( 2  x.  u ) )  +  ( 2  x.  u ) )  <->  2  ||  P ) )
9588, 94mtbird 292 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  -.  2  ||  ( ( P  -  ( 2  x.  u ) )  +  ( 2  x.  u
) ) )
9654adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  u  e.  ZZ )
97 dvdsmul1 12566 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2  e.  ZZ  /\  u  e.  ZZ )  ->  2  ||  ( 2  x.  u ) )
9853, 96, 97sylancr 644 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  2  ||  ( 2  x.  u
) )
9953a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  2  e.  ZZ )
10089nnzd 10132 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  ZZ )
101100, 91zsubcld 10138 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  -  ( 2  x.  u ) )  e.  ZZ )
102 dvds2add 12576 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
10399, 101, 91, 102syl3anc 1182 . . . . . . . . . . . . . . . . . 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 ) ) ) )
10498, 103mpan2d 655 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  ||  ( P  -  ( 2  x.  u ) )  -> 
2  ||  ( ( P  -  ( 2  x.  u ) )  +  ( 2  x.  u ) ) ) )
10595, 104mtod 168 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  -.  2  ||  ( P  -  ( 2  x.  u
) ) )
106 breq2 4043 . . . . . . . . . . . . . . . . 17  |-  ( ( 1st `  z )  =  ( P  -  ( 2  x.  u
) )  ->  (
2  ||  ( 1st `  z )  <->  2  ||  ( P  -  (
2  x.  u ) ) ) )
107106notbid 285 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  z )  =  ( P  -  ( 2  x.  u
) )  ->  ( -.  2  ||  ( 1st `  z )  <->  -.  2  ||  ( P  -  (
2  x.  u ) ) ) )
108105, 107syl5ibrcom 213 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  S )  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) )  ->  -.  2  ||  ( 1st `  z ) ) )
109108rexlimdva 2680 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  S )  ->  ( E. u  e.  (
( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) ( 1st `  z
)  =  ( P  -  ( 2  x.  u ) )  ->  -.  2  ||  ( 1st `  z ) ) )
110 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  S )  ->  z  e.  S )
1118, 110sseldi 3191 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  S )  ->  z  e.  ( ( 1 ... M )  X.  (
1 ... N ) ) )
112 xp1st 6165 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( ( 1 ... M )  X.  ( 1 ... N
) )  ->  ( 1st `  z )  e.  ( 1 ... M
) )
113111, 112syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  S )  ->  ( 1st `  z )  e.  ( 1 ... M
) )
114 elfzelz 10814 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  z )  e.  ( 1 ... M )  ->  ( 1st `  z )  e.  ZZ )
115 odd2np1 12603 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  z )  e.  ZZ  ->  ( -.  2  ||  ( 1st `  z )  <->  E. n  e.  ZZ  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )
116113, 114, 1153syl 18 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  S )  ->  ( -.  2  ||  ( 1st `  z )  <->  E. n  e.  ZZ  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )
117 lgsquad.4 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  M  =  ( ( P  - 
1 )  /  2
)
118 oddprm 12884 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
11946, 118syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN )
120117, 119syl5eqel 2380 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  M  e.  NN )
121120nnred 9777 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  RR )
122121ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  M  e.  RR )
123122rehalfcld 9974 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  / 
2 )  e.  RR )
124 reflcl 10944 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( M  /  2 )  e.  RR  ->  ( |_ `  ( M  / 
2 ) )  e.  RR )
125123, 124syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( |_ `  ( M  /  2
) )  e.  RR )
126120ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  M  e.  NN )
127126nnzd 10132 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  M  e.  ZZ )
128 simprl 732 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  n  e.  ZZ )
129127, 128zsubcld 10138 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  -  n )  e.  ZZ )
130129zred 10133 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  -  n )  e.  RR )
131 flle 10947 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( M  /  2 )  e.  RR  ->  ( |_ `  ( M  / 
2 ) )  <_ 
( M  /  2
) )
132123, 131syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( |_ `  ( M  /  2
) )  <_  ( M  /  2 ) )
133 zre 10044 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ZZ  ->  n  e.  RR )
134133ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  n  e.  RR )
135 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) )
136113adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 1st `  z
)  e.  ( 1 ... M ) )
137135, 136eqeltrd 2370 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  +  1 )  e.  ( 1 ... M ) )
138 elfzle2 10816 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 2  x.  n
)  +  1 )  e.  ( 1 ... M )  ->  (
( 2  x.  n
)  +  1 )  <_  M )
139137, 138syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  +  1 )  <_  M
)
140 zmulcl 10082 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 2  e.  ZZ  /\  n  e.  ZZ )  ->  ( 2  x.  n
)  e.  ZZ )
14153, 128, 140sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  n )  e.  ZZ )
142 zltp1le 10083 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 2  x.  n
)  e.  ZZ  /\  M  e.  ZZ )  ->  ( ( 2  x.  n )  <  M  <->  ( ( 2  x.  n
)  +  1 )  <_  M ) )
143141, 127, 142syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  < 
M  <->  ( ( 2  x.  n )  +  1 )  <_  M
) )
144139, 143mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  n )  <  M
)
145 2re 9831 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  2  e.  RR
146145a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  2  e.  RR )
147 2pos 9844 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  <  2
148147a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  0  <  2
)
149 ltmuldiv2 9643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  e.  RR  /\  M  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( 2  x.  n )  < 
M  <->  n  <  ( M  /  2 ) ) )
150134, 122, 146, 148, 149syl112anc 1186 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  < 
M  <->  n  <  ( M  /  2 ) ) )
151144, 150mpbid 201 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  n  <  ( M  /  2 ) )
152123recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  / 
2 )  e.  CC )
153152, 152pncan2d 9175 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( ( M  /  2 )  +  ( M  / 
2 ) )  -  ( M  /  2
) )  =  ( M  /  2 ) )
154120nncnd 9778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  M  e.  CC )
155154ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  M  e.  CC )
1561552halvesd 9973 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( M  /  2 )  +  ( M  /  2
) )  =  M )
157156oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( ( M  /  2 )  +  ( M  / 
2 ) )  -  ( M  /  2
) )  =  ( M  -  ( M  /  2 ) ) )
158153, 157eqtr3d 2330 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  / 
2 )  =  ( M  -  ( M  /  2 ) ) )
159151, 158breqtrd 4063 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  n  <  ( M  -  ( M  /  2 ) ) )
160134, 122, 123, 159ltsub13d 9394 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  / 
2 )  <  ( M  -  n )
)
161125, 123, 130, 132, 160lelttrd 8990 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( |_ `  ( M  /  2
) )  <  ( M  -  n )
)
162123flcld 10946 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( |_ `  ( M  /  2
) )  e.  ZZ )
163 zltp1le 10083 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( |_ `  ( M  /  2 ) )  e.  ZZ  /\  ( M  -  n )  e.  ZZ )  ->  (
( |_ `  ( M  /  2 ) )  <  ( M  -  n )  <->  ( ( |_ `  ( M  / 
2 ) )  +  1 )  <_  ( M  -  n )
) )
164162, 129, 163syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( |_
`  ( M  / 
2 ) )  < 
( M  -  n
)  <->  ( ( |_
`  ( M  / 
2 ) )  +  1 )  <_  ( M  -  n )
) )
165161, 164mpbid 201 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( |_
`  ( M  / 
2 ) )  +  1 )  <_  ( M  -  n )
)
16665mul01i 9018 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 2  x.  0 )  =  0
167 zcn 10045 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  e.  ZZ  ->  n  e.  CC )
168167ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  n  e.  CC )
169 mulcl 8837 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 2  e.  CC  /\  n  e.  CC )  ->  ( 2  x.  n
)  e.  CC )
17065, 168, 169sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  n )  e.  CC )
171 pncan 9073 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 2  x.  n
)  e.  CC  /\  1  e.  CC )  ->  ( ( ( 2  x.  n )  +  1 )  -  1 )  =  ( 2  x.  n ) )
172170, 19, 171sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( ( 2  x.  n )  +  1 )  - 
1 )  =  ( 2  x.  n ) )
173 elfznn 10835 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 2  x.  n
)  +  1 )  e.  ( 1 ... M )  ->  (
( 2  x.  n
)  +  1 )  e.  NN )
174 nnm1nn0 10021 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 2  x.  n
)  +  1 )  e.  NN  ->  (
( ( 2  x.  n )  +  1 )  -  1 )  e.  NN0 )
175137, 173, 1743syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( ( 2  x.  n )  +  1 )  - 
1 )  e.  NN0 )
176172, 175eqeltrrd 2371 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  n )  e.  NN0 )
177176nn0ge0d 10037 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  0  <_  (
2  x.  n ) )
178166, 177syl5eqbr 4072 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  0 )  <_  (
2  x.  n ) )
179 0re 8854 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR
180179a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  0  e.  RR )
181 lemul2 9625 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 0  e.  RR  /\  n  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( 0  <_  n 
<->  ( 2  x.  0 )  <_  ( 2  x.  n ) ) )
182180, 134, 146, 148, 181syl112anc 1186 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 0  <_  n 
<->  ( 2  x.  0 )  <_  ( 2  x.  n ) ) )
183178, 182mpbird 223 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  0  <_  n
)
184122, 134subge02d 9380 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 0  <_  n 
<->  ( M  -  n
)  <_  M )
)
185183, 184mpbid 201 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  -  n )  <_  M
)
186162peano2zd 10136 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( |_
`  ( M  / 
2 ) )  +  1 )  e.  ZZ )
187 elfz 10804 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 )
) )
188129, 186, 127, 187syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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
) ) )
189165, 185, 188mpbir2and 888 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( M  -  n )  e.  ( ( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) )
19084ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  P  e.  Prime )
191190, 48syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  P  e.  NN )
192191nncnd 9778 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  P  e.  CC )
193 peano2cn 9000 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  x.  n )  e.  CC  ->  (
( 2  x.  n
)  +  1 )  e.  CC )
194170, 193syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  n )  +  1 )  e.  CC )
195192, 194nncand 9178 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( P  -  ( P  -  (
( 2  x.  n
)  +  1 ) ) )  =  ( ( 2  x.  n
)  +  1 ) )
19619a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  1  e.  CC )
197192, 170, 196sub32d 9205 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( P  -  ( 2  x.  n ) )  - 
1 )  =  ( ( P  -  1 )  -  ( 2  x.  n ) ) )
198192, 170, 196subsub4d 9204 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( P  -  ( 2  x.  n ) )  - 
1 )  =  ( P  -  ( ( 2  x.  n )  +  1 ) ) )
19965a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  2  e.  CC )
200199, 155, 168subdid 9251 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  ( M  -  n
) )  =  ( ( 2  x.  M
)  -  ( 2  x.  n ) ) )
201117oveq2i 5885 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2  x.  M )  =  ( 2  x.  (
( P  -  1 )  /  2 ) )
20249nnzd 10132 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  P  e.  ZZ )
203202ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  P  e.  ZZ )
204 peano2zm 10078 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  ZZ  ->  ( P  -  1 )  e.  ZZ )
205203, 204syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( P  - 
1 )  e.  ZZ )
206205zcnd 10134 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( P  - 
1 )  e.  CC )
20767a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  2  =/=  0
)
208206, 199, 207divcan2d 9554 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  ( ( P  - 
1 )  /  2
) )  =  ( P  -  1 ) )
209201, 208syl5eq 2340 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 2  x.  M )  =  ( P  -  1 ) )
210209oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( 2  x.  M )  -  ( 2  x.  n
) )  =  ( ( P  -  1 )  -  ( 2  x.  n ) ) )
211200, 210eqtr2d 2329 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( ( P  -  1 )  -  ( 2  x.  n
) )  =  ( 2  x.  ( M  -  n ) ) )
212197, 198, 2113eqtr3d 2336 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( P  -  ( ( 2  x.  n )  +  1 ) )  =  ( 2  x.  ( M  -  n ) ) )
213212oveq2d 5890 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( P  -  ( P  -  (
( 2  x.  n
)  +  1 ) ) )  =  ( P  -  ( 2  x.  ( M  -  n ) ) ) )
214195, 213, 1353eqtr3rd 2337 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  S )  /\  (
n  e.  ZZ  /\  ( ( 2  x.  n )  +  1 )  =  ( 1st `  z ) ) )  ->  ( 1st `  z
)  =  ( P  -  ( 2  x.  ( M  -  n
) ) ) )
215 oveq2 5882 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  ( M  -  n )  ->  (
2  x.  u )  =  ( 2  x.  ( M  -  n
) ) )
216215oveq2d 5890 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  ( M  -  n )  ->  ( P  -  ( 2  x.  u ) )  =  ( P  -  ( 2  x.  ( M  -  n )
) ) )
217216eqeq2d 2307 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  ( M  -  n )  ->  (
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) )  <->  ( 1st `  z )  =  ( P  -  ( 2  x.  ( M  -  n ) ) ) ) )
218217rspcev 2897 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) )
219189, 214, 218syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) )
220219expr 598 . . . . . . . . . . . . . . . 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 ) ) ) )
221220rexlimdva 2680 . . . . . . . . . . . . . . 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 ) ) ) )
222116, 221sylbid 206 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  S )  ->  ( -.  2  ||  ( 1st `  z )  ->  E. u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) ( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) ) )
223109, 222impbid 183 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  S )  ->  ( E. u  e.  (
( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) ( 1st `  z
)  =  ( P  -  ( 2  x.  u ) )  <->  -.  2  ||  ( 1st `  z
) ) )
224223rabbidva 2792 . . . . . . . . . . . 12  |-  ( ph  ->  { z  e.  S  |  E. u  e.  ( ( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) ( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) }  =  { z  e.  S  |  -.  2  ||  ( 1st `  z
) } )
22576, 224syl5eq 2340 . . . . . . . . . . 11  |-  ( ph  ->  U_ u  e.  ( ( ( |_ `  ( M  /  2
) )  +  1 ) ... M ) { z  e.  S  |  ( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) }  =  { z  e.  S  |  -.  2  ||  ( 1st `  z
) } )
226225fveq2d 5545 . . . . . . . . . 10  |-  ( ph  ->  ( # `  U_ u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u ) ) } )  =  (
# `  { z  e.  S  |  -.  2  ||  ( 1st `  z
) } ) )
2276relopabi 4827 . . . . . . . . . . . . . . 15  |-  Rel  S
228 relss 4791 . . . . . . . . . . . . . . 15  |-  ( { z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) } 
C_  S  ->  ( Rel  S  ->  Rel  { z  e.  S  |  ( 1st `  z )  =  ( P  -  ( 2  x.  u
) ) } ) )
22937, 227, 228mp2 17 . . . . . . . . . . . . . 14  |-  Rel  {
z  e.  S  | 
( 1st `  z
)  =  ( P  -  ( 2  x.  u ) ) }
230 relxp 4810 . . . . . . . . . . . . . 14  |-  Rel  ( { ( P  -  ( 2  x.  u
) ) }  X.  ( 1 ... (
( 2  x.  N
)  -  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  u
) ) ) ) ) )
2316eleq2i 2360 . . . . . . . . . . . . . . . . . 18  |-  ( <.
x ,  y >.  e.  S  <->  <. x ,  y
>.  e.  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  < 
( x  x.  Q
) ) } )
232 opabid 4287 . . . . . . . . . . . . . . . . . 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 ) ) )
233231, 232bitri 240 . . . . . . . . . . . . . . . . 17  |-  ( <.
x ,  y >.  e.  S  <->  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) )
234 anass 630 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
235 lgseisen.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
236 eldifi 3311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( Q  e.  ( Prime  \  {
2 } )  ->  Q  e.  Prime )
237 prmnn 12777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( Q  e.  Prime  ->  Q  e.  NN )
238235, 236, 2373syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  Q  e.  NN )
239238nnred 9777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  Q  e.  RR )
240239, 49nndivred 9810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( Q  /  P
)  e.  RR )
241240adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  /  P )  e.  RR )
24257zred 10133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  u )  e.  RR )
243241, 242remulcld 8879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  /  P
)  x.  ( 2  x.  u ) )  e.  RR )
244243flcld 10946 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e.  ZZ )
245244peano2zd 10136 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  +  1 )  e.  ZZ )
246245zred 10133 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  +  1 )  e.  RR )
247246adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  (
( |_ `  (
( Q  /  P
)  x.  ( 2  x.  u ) ) )  +  1 )  e.  RR )
248239ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  Q  e.  RR )
249 nnre 9769 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  NN  ->  y  e.  RR )
250249adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  y  e.  RR )
251 lesub 9269 . . . . . . . . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
253239adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  Q  e.  RR )
254253recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  Q  e.  CC )
25551, 254mulcomd 8872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  x.  Q )  =  ( Q  x.  P ) )
25658, 254mulcomd 8872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 2  x.  u
)  x.  Q )  =  ( Q  x.  ( 2  x.  u
) ) )
25750nnne0d 9806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  =/=  0 )
258254, 51, 257divcan1d 9553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  /  P
)  x.  P )  =  Q )
259258oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( ( Q  /  P )  x.  P
)  x.  ( 2  x.  u ) )  =  ( Q  x.  ( 2  x.  u
) ) )
260241recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  /  P )  e.  CC )
261260, 51, 58mul32d 9038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 2  x.  u
)  x.  Q )  =  ( ( ( Q  /  P )  x.  ( 2  x.  u ) )  x.  P ) )
263255, 262oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
26451, 58, 254subdird 9252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  -  (
2  x.  u ) )  x.  Q )  =  ( ( P  x.  Q )  -  ( ( 2  x.  u )  x.  Q
) ) )
265243recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  /  P
)  x.  ( 2  x.  u ) )  e.  CC )
266254, 265, 51subdird 9252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2338 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  -  (
2  x.  u ) )  x.  Q )  =  ( ( Q  -  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  x.  P ) )
268267adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4051 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
270243adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  (
( Q  /  P
)  x.  ( 2  x.  u ) )  e.  RR )
271248, 270resubcld 9227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  ( Q  -  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e.  RR )
27250adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  P  e.  NN )
273272nnred 9777 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  P  e.  RR )
274272nngt0d 9805 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  0  <  P )
275 ltmul1 9622 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . . . . . . . . . . . . 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 9271 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . . . . . . . . . . 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 272 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
280238adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  Q  e.  NN )
281280nnzd 10132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  Q  e.  ZZ )
282 nnz 10061 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  NN  ->  y  e.  ZZ )
283 zsubcl 10077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Q  e.  ZZ  /\  y  e.  ZZ )  ->  ( Q  -  y
)  e.  ZZ )
284281, 282, 283syl2an 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  ( Q  -  y )  e.  ZZ )
285 fllt 10954 . . . . . . . . . . . . . . . . . . . . . . . . . 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 642 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
287244adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  /\  y  e.  NN )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e.  ZZ )
288 zltp1le 10083 . . . . . . . . . . . . . . . . . . . . . . . . . 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 642 . . . . . . . . . . . . . . . . . . . . . . . . 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 270 . . . . . . . . . . . . . . . . . . . . . . . 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 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 2  x.  N )  =  ( 2  x.  (
( Q  -  1 )  /  2 ) )
293 peano2rem 9129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Q  e.  RR  ->  ( Q  -  1 )  e.  RR )
294253, 293syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  -  1 )  e.  RR )
295294recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  -  1 )  e.  CC )
29665a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  2  e.  CC )
29767a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  2  =/=  0 )
298295, 296, 297divcan2d 9554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  ( ( Q  -  1 )  /  2 ) )  =  ( Q  - 
1 ) )
299292, 298syl5eq 2340 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  N )  =  ( Q  - 
1 ) )
300299oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
30119a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  1  e.  CC )
302244zcnd 10134 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e.  CC )
303254, 301, 302sub32d 9205 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9204 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2332 . . . . . . . . . . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . . . . . . . . . . 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 4051 . . . . . . . . . . . . . . . . . . . . . . . 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 276 . . . . . . . . . . . . . . . . . . . . . . 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 684 . . . . . . . . . . . . . . . . . . . . . 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 9893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  2  e.  NN
311 oddprm 12884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( Q  e.  ( Prime  \  {
2 } )  -> 
( ( Q  - 
1 )  /  2
)  e.  NN )
312235, 311syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( ( Q  - 
1 )  /  2
)  e.  NN )
313291, 312syl5eqel 2380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  N  e.  NN )
314 nnmulcl 9785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 2  e.  NN  /\  N  e.  NN )  ->  ( 2  x.  N
)  e.  NN )
315310, 313, 314sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( 2  x.  N
)  e.  NN )
316315adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  N )  e.  NN )
317316nnred 9777 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  N )  e.  RR )
318313adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  N  e.  NN )
319318nnred 9777 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  N  e.  RR )
320244zred 10133 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  u
) ) )  e.  RR )
321313nncnd 9778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  N  e.  CC )
322321adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  N  e.  CC )
3233222timesd 9970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  N )  =  ( N  +  N ) )
324323oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 2  x.  N
)  -  N )  =  ( ( N  +  N )  -  N ) )
325322, 322pncan2d 9175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( N  +  N
)  -  N )  =  N )
326324, 325eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( 2  x.  N
)  -  N )  =  N )
327253rehalfcld 9974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  /  2 )  e.  RR )
328253ltm1d 9705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  -  1 )  <  Q )
329145a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  2  e.  RR )
330147a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  0  <  2 )
331 ltdiv1 9636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  -  1 )  <  Q  <->  ( ( Q  -  1 )  /  2 )  < 
( Q  /  2
) ) )
333328, 332mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  -  1 )  /  2 )  <  ( Q  / 
2 ) )
334291, 333syl5eqbr 4072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  N  <  ( Q  /  2
) )
335319, 327, 334ltled 8983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  N  <_  ( Q  /  2
) )
336254, 296, 51, 297div32d 9575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  /  2
)  x.  P )  =  ( Q  x.  ( P  /  2
) ) )
337121adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  M  e.  RR )
338337rehalfcld 9974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( M  /  2 )  e.  RR )
339 peano2re 9001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( |_ `  ( M  /  2 ) )  e.  RR  ->  (
( |_ `  ( M  /  2 ) )  +  1 )  e.  RR )
340338, 124, 3393syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( |_ `  ( M  /  2 ) )  +  1 )  e.  RR )
34155zred 10133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  u  e.  RR )
342 flltp1 10948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( M  /  2 )  e.  RR  ->  ( M  /  2 )  < 
( ( |_ `  ( M  /  2
) )  +  1 ) )
343338, 342syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( M  /  2 )  < 
( ( |_ `  ( M  /  2
) )  +  1 ) )
344 elfzle1 10815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( u  e.  ( ( ( |_ `  ( M  /  2 ) )  +  1 ) ... M )  ->  (
( |_ `  ( M  /  2 ) )  +  1 )  <_  u )
345344adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( |_ `  ( M  /  2 ) )  +  1 )  <_  u )
346338, 340, 341, 343, 345ltletrd 8992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( M  /  2 )  < 
u )
347 ltdivmul 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( M  e.  RR  /\  u  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( M  /  2 )  < 
u  <->  M  <  ( 2  x.  u ) ) )
348337, 341, 329, 330, 347syl112anc 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( M  /  2
)  <  u  <->  M  <  ( 2  x.  u ) ) )
349346, 348mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  M  <  ( 2  x.  u
) )
350117, 349syl5eqbrr 4073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  -  1 )  /  2 )  <  ( 2  x.  u ) )
35150nnred 9777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  RR )
352 peano2rem 9129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( P  e.  RR  ->  ( P  -  1 )  e.  RR )
353351, 352syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  -  1 )  e.  RR )
354 ltdivmul 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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, 242, 329, 330, 354syl112anc 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( ( P  - 
1 )  /  2
)  <  ( 2  x.  u )  <->  ( P  -  1 )  < 
( 2  x.  (
2  x.  u ) ) ) )
356350, 355mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  -  1 )  <  ( 2  x.  ( 2  x.  u
) ) )
357202adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  e.  ZZ )
358 zmulcl 10082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 2  e.  ZZ  /\  ( 2  x.  u
)  e.  ZZ )  ->  ( 2  x.  ( 2  x.  u
) )  e.  ZZ )
35953, 57, 358sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
2  x.  ( 2  x.  u ) )  e.  ZZ )
360 zlem1lt 10085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  <_  ( 2  x.  ( 2  x.  u
) )  <->  ( P  -  1 )  < 
( 2  x.  (
2  x.  u ) ) ) )
362356, 361mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  P  <_  ( 2  x.  (
2  x.  u ) ) )
363 ledivmul 9645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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, 242, 329, 330, 363syl112anc 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  /  2
)  <_  ( 2  x.  u )  <->  P  <_  ( 2  x.  ( 2  x.  u ) ) ) )
365362, 364mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  /  2 )  <_ 
( 2  x.  u
) )
366351rehalfcld 9974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( P  /  2 )  e.  RR )
367280nngt0d 9805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  0  <  Q )
368 lemul2 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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, 242, 253, 367, 368syl112anc 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( P  /  2
)  <_  ( 2  x.  u )  <->  ( Q  x.  ( P  /  2
) )  <_  ( Q  x.  ( 2  x.  u ) ) ) )
370365, 369mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  x.  ( P  /  2 ) )  <_  ( Q  x.  ( 2  x.  u
) ) )
371336, 370eqbrtrd 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  /  2
)  x.  P )  <_  ( Q  x.  ( 2  x.  u
) ) )
372253, 242remulcld 8879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  x.  ( 2  x.  u ) )  e.  RR )
37350nngt0d 9805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  0  <  P )
374 lemuldiv 9651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  ( Q  /  2 )  <_ 
( ( Q  x.  ( 2  x.  u
) )  /  P
) )
377254, 58, 51, 257div23d 9589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  u  e.  ( ( ( |_
`  ( M  / 
2 ) )  +  1 ) ... M
) )  ->  (
( Q  x.  (