ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  gausslemma2dlem1a Unicode version

Theorem gausslemma2dlem1a 15122
Description: Lemma for gausslemma2dlem1 15125. (Contributed by AV, 1-Jul-2021.)
Hypotheses
Ref Expression
gausslemma2d.p  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
gausslemma2d.h  |-  H  =  ( ( P  - 
1 )  /  2
)
gausslemma2d.r  |-  R  =  ( x  e.  ( 1 ... H ) 
|->  if ( ( x  x.  2 )  < 
( P  /  2
) ,  ( x  x.  2 ) ,  ( P  -  (
x  x.  2 ) ) ) )
Assertion
Ref Expression
gausslemma2dlem1a  |-  ( ph  ->  ran  R  =  ( 1 ... H ) )
Distinct variable groups:    x, H    x, P    ph, x
Allowed substitution hint:    R( x)

Proof of Theorem gausslemma2dlem1a
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 gausslemma2d.r . . . . 5  |-  R  =  ( x  e.  ( 1 ... H ) 
|->  if ( ( x  x.  2 )  < 
( P  /  2
) ,  ( x  x.  2 ) ,  ( P  -  (
x  x.  2 ) ) ) )
21elrnmpt 4905 . . . 4  |-  ( y  e.  _V  ->  (
y  e.  ran  R  <->  E. x  e.  ( 1 ... H ) y  =  if ( ( x  x.  2 )  <  ( P  / 
2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2
) ) ) ) )
32elv 2764 . . 3  |-  ( y  e.  ran  R  <->  E. x  e.  ( 1 ... H
) y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) ) )
4 iftrue 3562 . . . . . . . . . 10  |-  ( ( x  x.  2 )  <  ( P  / 
2 )  ->  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  =  ( x  x.  2 ) )
54eqeq2d 2205 . . . . . . . . 9  |-  ( ( x  x.  2 )  <  ( P  / 
2 )  ->  (
y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  <-> 
y  =  ( x  x.  2 ) ) )
65adantr 276 . . . . . . . 8  |-  ( ( ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  <-> 
y  =  ( x  x.  2 ) ) )
7 elfz1b 10146 . . . . . . . . . . . . 13  |-  ( x  e.  ( 1 ... H )  <->  ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H ) )
8 id 19 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  x  e.  NN )
9 2nn 9133 . . . . . . . . . . . . . . . . . . 19  |-  2  e.  NN
109a1i 9 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  2  e.  NN )
118, 10nnmulcld 9021 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  (
x  x.  2 )  e.  NN )
12113ad2ant1 1020 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  ->  (
x  x.  2 )  e.  NN )
13123ad2ant1 1020 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  /\  ph 
/\  ( x  x.  2 )  <  ( P  /  2 ) )  ->  ( x  x.  2 )  e.  NN )
14 gausslemma2d.h . . . . . . . . . . . . . . . . . . 19  |-  H  =  ( ( P  - 
1 )  /  2
)
1514eleq1i 2259 . . . . . . . . . . . . . . . . . 18  |-  ( H  e.  NN  <->  ( ( P  -  1 )  /  2 )  e.  NN )
1615biimpi 120 . . . . . . . . . . . . . . . . 17  |-  ( H  e.  NN  ->  (
( P  -  1 )  /  2 )  e.  NN )
17163ad2ant2 1021 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  ->  (
( P  -  1 )  /  2 )  e.  NN )
18173ad2ant1 1020 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  /\  ph 
/\  ( x  x.  2 )  <  ( P  /  2 ) )  ->  ( ( P  -  1 )  / 
2 )  e.  NN )
19 gausslemma2d.p . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
20 nnoddn2prm 12388 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( P  e.  NN  /\ 
-.  2  ||  P
) )
21 nnz 9326 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( P  e.  NN  ->  P  e.  ZZ )
2221anim1i 340 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( P  e.  NN  /\  -.  2  ||  P )  ->  ( P  e.  ZZ  /\  -.  2  ||  P ) )
2320, 22syl 14 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( P  e.  ZZ  /\ 
-.  2  ||  P
) )
24 nnz 9326 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  NN  ->  x  e.  ZZ )
25 2z 9335 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  2  e.  ZZ
2625a1i 9 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  NN  ->  2  e.  ZZ )
2724, 26zmulcld 9435 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  NN  ->  (
x  x.  2 )  e.  ZZ )
28273ad2ant1 1020 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  ->  (
x  x.  2 )  e.  ZZ )
2923, 28anim12i 338 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( P  e.  ( Prime  \  { 2 } )  /\  ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H ) )  -> 
( ( P  e.  ZZ  /\  -.  2  ||  P )  /\  (
x  x.  2 )  e.  ZZ ) )
30 df-3an 982 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( P  e.  ZZ  /\  -.  2  ||  P  /\  ( x  x.  2
)  e.  ZZ )  <-> 
( ( P  e.  ZZ  /\  -.  2  ||  P )  /\  (
x  x.  2 )  e.  ZZ ) )
3129, 30sylibr 134 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( P  e.  ( Prime  \  { 2 } )  /\  ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H ) )  -> 
( P  e.  ZZ  /\ 
-.  2  ||  P  /\  ( x  x.  2 )  e.  ZZ ) )
3231ex 115 . . . . . . . . . . . . . . . . . . 19  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  ->  ( P  e.  ZZ  /\  -.  2  ||  P  /\  (
x  x.  2 )  e.  ZZ ) ) )
3319, 32syl 14 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  ->  ( P  e.  ZZ  /\  -.  2  ||  P  /\  (
x  x.  2 )  e.  ZZ ) ) )
3433impcom 125 . . . . . . . . . . . . . . . . 17  |-  ( ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  /\  ph )  ->  ( P  e.  ZZ  /\  -.  2  ||  P  /\  (
x  x.  2 )  e.  ZZ ) )
35 ltoddhalfle 12024 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e.  ZZ  /\  -.  2  ||  P  /\  ( x  x.  2
)  e.  ZZ )  ->  ( ( x  x.  2 )  < 
( P  /  2
)  <->  ( x  x.  2 )  <_  (
( P  -  1 )  /  2 ) ) )
3634, 35syl 14 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  /\  ph )  ->  ( (
x  x.  2 )  <  ( P  / 
2 )  <->  ( x  x.  2 )  <_  (
( P  -  1 )  /  2 ) ) )
3736biimp3a 1356 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  /\  ph 
/\  ( x  x.  2 )  <  ( P  /  2 ) )  ->  ( x  x.  2 )  <_  (
( P  -  1 )  /  2 ) )
3813, 18, 373jca 1179 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  /\  ph 
/\  ( x  x.  2 )  <  ( P  /  2 ) )  ->  ( ( x  x.  2 )  e.  NN  /\  ( ( P  -  1 )  /  2 )  e.  NN  /\  ( x  x.  2 )  <_ 
( ( P  - 
1 )  /  2
) ) )
39383exp 1204 . . . . . . . . . . . . 13  |-  ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  ->  ( ph  ->  ( ( x  x.  2 )  < 
( P  /  2
)  ->  ( (
x  x.  2 )  e.  NN  /\  (
( P  -  1 )  /  2 )  e.  NN  /\  (
x  x.  2 )  <_  ( ( P  -  1 )  / 
2 ) ) ) ) )
407, 39sylbi 121 . . . . . . . . . . . 12  |-  ( x  e.  ( 1 ... H )  ->  ( ph  ->  ( ( x  x.  2 )  < 
( P  /  2
)  ->  ( (
x  x.  2 )  e.  NN  /\  (
( P  -  1 )  /  2 )  e.  NN  /\  (
x  x.  2 )  <_  ( ( P  -  1 )  / 
2 ) ) ) ) )
4140impcom 125 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... H
) )  ->  (
( x  x.  2 )  <  ( P  /  2 )  -> 
( ( x  x.  2 )  e.  NN  /\  ( ( P  - 
1 )  /  2
)  e.  NN  /\  ( x  x.  2
)  <_  ( ( P  -  1 )  /  2 ) ) ) )
4241impcom 125 . . . . . . . . . 10  |-  ( ( ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( ( x  x.  2 )  e.  NN  /\  ( ( P  - 
1 )  /  2
)  e.  NN  /\  ( x  x.  2
)  <_  ( ( P  -  1 )  /  2 ) ) )
4314oveq2i 5921 . . . . . . . . . . . 12  |-  ( 1 ... H )  =  ( 1 ... (
( P  -  1 )  /  2 ) )
4443eleq2i 2260 . . . . . . . . . . 11  |-  ( ( x  x.  2 )  e.  ( 1 ... H )  <->  ( x  x.  2 )  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) )
45 elfz1b 10146 . . . . . . . . . . 11  |-  ( ( x  x.  2 )  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  <->  ( (
x  x.  2 )  e.  NN  /\  (
( P  -  1 )  /  2 )  e.  NN  /\  (
x  x.  2 )  <_  ( ( P  -  1 )  / 
2 ) ) )
4644, 45bitri 184 . . . . . . . . . 10  |-  ( ( x  x.  2 )  e.  ( 1 ... H )  <->  ( (
x  x.  2 )  e.  NN  /\  (
( P  -  1 )  /  2 )  e.  NN  /\  (
x  x.  2 )  <_  ( ( P  -  1 )  / 
2 ) ) )
4742, 46sylibr 134 . . . . . . . . 9  |-  ( ( ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( x  x.  2 )  e.  ( 1 ... H ) )
48 eleq1 2256 . . . . . . . . 9  |-  ( y  =  ( x  x.  2 )  ->  (
y  e.  ( 1 ... H )  <->  ( x  x.  2 )  e.  ( 1 ... H ) ) )
4947, 48syl5ibrcom 157 . . . . . . . 8  |-  ( ( ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( y  =  ( x  x.  2 )  ->  y  e.  ( 1 ... H ) ) )
506, 49sylbid 150 . . . . . . 7  |-  ( ( ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  ->  y  e.  ( 1 ... H ) ) )
5150ancoms 268 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( 1 ... H
) )  /\  (
x  x.  2 )  <  ( P  / 
2 ) )  -> 
( y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  ->  y  e.  ( 1 ... H ) ) )
52 iffalse 3565 . . . . . . . . . 10  |-  ( -.  ( x  x.  2 )  <  ( P  /  2 )  ->  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  =  ( P  -  ( x  x.  2
) ) )
5352eqeq2d 2205 . . . . . . . . 9  |-  ( -.  ( x  x.  2 )  <  ( P  /  2 )  -> 
( y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  <-> 
y  =  ( P  -  ( x  x.  2 ) ) ) )
5453adantr 276 . . . . . . . 8  |-  ( ( -.  ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  <-> 
y  =  ( P  -  ( x  x.  2 ) ) ) )
55 eldifi 3281 . . . . . . . . . . . . . 14  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  e.  Prime )
56 prmz 12239 . . . . . . . . . . . . . 14  |-  ( P  e.  Prime  ->  P  e.  ZZ )
5719, 55, 563syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  P  e.  ZZ )
5857ad2antrl 490 . . . . . . . . . . . 12  |-  ( ( -.  ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  ->  P  e.  ZZ )
59 elfzelz 10081 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 ... H )  ->  x  e.  ZZ )
6025a1i 9 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 ... H )  ->  2  e.  ZZ )
6159, 60zmulcld 9435 . . . . . . . . . . . . 13  |-  ( x  e.  ( 1 ... H )  ->  (
x  x.  2 )  e.  ZZ )
6261ad2antll 491 . . . . . . . . . . . 12  |-  ( ( -.  ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( x  x.  2 )  e.  ZZ )
6358, 62zsubcld 9434 . . . . . . . . . . 11  |-  ( ( -.  ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( P  -  (
x  x.  2 ) )  e.  ZZ )
6456zred 9429 . . . . . . . . . . . . . 14  |-  ( P  e.  Prime  ->  P  e.  RR )
6514breq2i 4037 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  <_  H  <->  x  <_  ( ( P  -  1 )  /  2 ) )
66 nnre 8979 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  x  e.  RR )
6766adantr 276 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  x  e.  RR )
68 peano2rem 8276 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  RR  ->  ( P  -  1 )  e.  RR )
6968adantl 277 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  ( P  -  1 )  e.  RR )
70 2re 9042 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  RR
71 2pos 9063 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  <  2
7270, 71pm3.2i 272 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 2  e.  RR  /\  0  <  2 )
7372a1i 9 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  ( 2  e.  RR  /\  0  <  2 ) )
74 lemuldiv 8890 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  ( P  -  1
)  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( (
x  x.  2 )  <_  ( P  - 
1 )  <->  x  <_  ( ( P  -  1 )  /  2 ) ) )
7567, 69, 73, 74syl3anc 1249 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  ( ( x  x.  2 )  <_  ( P  -  1 )  <-> 
x  <_  ( ( P  -  1 )  /  2 ) ) )
7665, 75bitr4id 199 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  ( x  <_  H  <->  ( x  x.  2 )  <_  ( P  - 
1 ) ) )
7711nnred 8985 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  (
x  x.  2 )  e.  RR )
7877adantr 276 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  ( x  x.  2 )  e.  RR )
79 simpr 110 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  P  e.  RR )
8078, 69, 79lesub2d 8562 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  ( ( x  x.  2 )  <_  ( P  -  1 )  <-> 
( P  -  ( P  -  1 ) )  <_  ( P  -  ( x  x.  2 ) ) ) )
81 recn 7995 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( P  e.  RR  ->  P  e.  CC )
82 1cnd 8025 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( P  e.  RR  ->  1  e.  CC )
8381, 82nncand 8325 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( P  e.  RR  ->  ( P  -  ( P  -  1 ) )  =  1 )
8483adantl 277 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  ( P  -  ( P  -  1 ) )  =  1 )
8584breq1d 4039 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  ( ( P  -  ( P  -  1
) )  <_  ( P  -  ( x  x.  2 ) )  <->  1  <_  ( P  -  ( x  x.  2 ) ) ) )
8685biimpd 144 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  ( ( P  -  ( P  -  1
) )  <_  ( P  -  ( x  x.  2 ) )  -> 
1  <_  ( P  -  ( x  x.  2 ) ) ) )
8780, 86sylbid 150 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  ( ( x  x.  2 )  <_  ( P  -  1 )  ->  1  <_  ( P  -  ( x  x.  2 ) ) ) )
8876, 87sylbid 150 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  NN  /\  P  e.  RR )  ->  ( x  <_  H  ->  1  <_  ( P  -  ( x  x.  2 ) ) ) )
8988impancom 260 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  NN  /\  x  <_  H )  -> 
( P  e.  RR  ->  1  <_  ( P  -  ( x  x.  2 ) ) ) )
90893adant2 1018 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  NN  /\  H  e.  NN  /\  x  <_  H )  ->  ( P  e.  RR  ->  1  <_  ( P  -  ( x  x.  2
) ) ) )
917, 90sylbi 121 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 ... H )  ->  ( P  e.  RR  ->  1  <_  ( P  -  ( x  x.  2
) ) ) )
9291com12 30 . . . . . . . . . . . . . 14  |-  ( P  e.  RR  ->  (
x  e.  ( 1 ... H )  -> 
1  <_  ( P  -  ( x  x.  2 ) ) ) )
9319, 55, 64, 924syl 18 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  ( 1 ... H )  ->  1  <_  ( P  -  ( x  x.  2 ) ) ) )
9493imp 124 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... H
) )  ->  1  <_  ( P  -  (
x  x.  2 ) ) )
9594adantl 277 . . . . . . . . . . 11  |-  ( ( -.  ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
1  <_  ( P  -  ( x  x.  2 ) ) )
96 elnnz1 9330 . . . . . . . . . . 11  |-  ( ( P  -  ( x  x.  2 ) )  e.  NN  <->  ( ( P  -  ( x  x.  2 ) )  e.  ZZ  /\  1  <_ 
( P  -  (
x  x.  2 ) ) ) )
9763, 95, 96sylanbrc 417 . . . . . . . . . 10  |-  ( ( -.  ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( P  -  (
x  x.  2 ) )  e.  NN )
987simp2bi 1015 . . . . . . . . . . 11  |-  ( x  e.  ( 1 ... H )  ->  H  e.  NN )
9998ad2antll 491 . . . . . . . . . 10  |-  ( ( -.  ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  ->  H  e.  NN )
100 nnre 8979 . . . . . . . . . . . . . . . . . 18  |-  ( P  e.  NN  ->  P  e.  RR )
101100rehalfcld 9219 . . . . . . . . . . . . . . . . 17  |-  ( P  e.  NN  ->  ( P  /  2 )  e.  RR )
102101adantr 276 . . . . . . . . . . . . . . . 16  |-  ( ( P  e.  NN  /\  -.  2  ||  P )  ->  ( P  / 
2 )  e.  RR )
10361zred 9429 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 1 ... H )  ->  (
x  x.  2 )  e.  RR )
104 lenlt 8085 . . . . . . . . . . . . . . . 16  |-  ( ( ( P  /  2
)  e.  RR  /\  ( x  x.  2
)  e.  RR )  ->  ( ( P  /  2 )  <_ 
( x  x.  2 )  <->  -.  ( x  x.  2 )  <  ( P  /  2 ) ) )
105102, 103, 104syl2an 289 . . . . . . . . . . . . . . 15  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  (
( P  /  2
)  <_  ( x  x.  2 )  <->  -.  (
x  x.  2 )  <  ( P  / 
2 ) ) )
10622, 61anim12i 338 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  (
( P  e.  ZZ  /\ 
-.  2  ||  P
)  /\  ( x  x.  2 )  e.  ZZ ) )
107106, 30sylibr 134 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  ( P  e.  ZZ  /\  -.  2  ||  P  /\  (
x  x.  2 )  e.  ZZ ) )
108 halfleoddlt 12025 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( P  e.  ZZ  /\  -.  2  ||  P  /\  ( x  x.  2
)  e.  ZZ )  ->  ( ( P  /  2 )  <_ 
( x  x.  2 )  <->  ( P  / 
2 )  <  (
x  x.  2 ) ) )
109107, 108syl 14 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  (
( P  /  2
)  <_  ( x  x.  2 )  <->  ( P  /  2 )  < 
( x  x.  2 ) ) )
110109biimpa 296 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( P  e.  NN  /\  -.  2  ||  P )  /\  x  e.  ( 1 ... H
) )  /\  ( P  /  2 )  <_ 
( x  x.  2 ) )  ->  ( P  /  2 )  < 
( x  x.  2 ) )
111 nncn 8980 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( P  e.  NN  ->  P  e.  CC )
112 subhalfhalf 9207 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( P  e.  CC  ->  ( P  -  ( P  /  2 ) )  =  ( P  / 
2 ) )
113111, 112syl 14 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  NN  ->  ( P  -  ( P  /  2 ) )  =  ( P  / 
2 ) )
114113breq1d 4039 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e.  NN  ->  (
( P  -  ( P  /  2 ) )  <  ( x  x.  2 )  <->  ( P  /  2 )  < 
( x  x.  2 ) ) )
115114ad3antrrr 492 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( P  e.  NN  /\  -.  2  ||  P )  /\  x  e.  ( 1 ... H
) )  /\  ( P  /  2 )  <_ 
( x  x.  2 ) )  ->  (
( P  -  ( P  /  2 ) )  <  ( x  x.  2 )  <->  ( P  /  2 )  < 
( x  x.  2 ) ) )
116110, 115mpbird 167 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( P  e.  NN  /\  -.  2  ||  P )  /\  x  e.  ( 1 ... H
) )  /\  ( P  /  2 )  <_ 
( x  x.  2 ) )  ->  ( P  -  ( P  /  2 ) )  <  ( x  x.  2 ) )
117100ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  P  e.  RR )
118101ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  ( P  /  2 )  e.  RR )
119103adantl 277 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  (
x  x.  2 )  e.  RR )
120117, 118, 1193jca 1179 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  ( P  e.  RR  /\  ( P  /  2 )  e.  RR  /\  ( x  x.  2 )  e.  RR ) )
121120adantr 276 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( P  e.  NN  /\  -.  2  ||  P )  /\  x  e.  ( 1 ... H
) )  /\  ( P  /  2 )  <_ 
( x  x.  2 ) )  ->  ( P  e.  RR  /\  ( P  /  2 )  e.  RR  /\  ( x  x.  2 )  e.  RR ) )
122 ltsub23 8451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( P  e.  RR  /\  ( P  /  2
)  e.  RR  /\  ( x  x.  2
)  e.  RR )  ->  ( ( P  -  ( P  / 
2 ) )  < 
( x  x.  2 )  <->  ( P  -  ( x  x.  2
) )  <  ( P  /  2 ) ) )
123121, 122syl 14 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( P  e.  NN  /\  -.  2  ||  P )  /\  x  e.  ( 1 ... H
) )  /\  ( P  /  2 )  <_ 
( x  x.  2 ) )  ->  (
( P  -  ( P  /  2 ) )  <  ( x  x.  2 )  <->  ( P  -  ( x  x.  2 ) )  < 
( P  /  2
) ) )
124116, 123mpbid 147 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( P  e.  NN  /\  -.  2  ||  P )  /\  x  e.  ( 1 ... H
) )  /\  ( P  /  2 )  <_ 
( x  x.  2 ) )  ->  ( P  -  ( x  x.  2 ) )  < 
( P  /  2
) )
12521ad2antrr 488 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  P  e.  ZZ )
126 simplr 528 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  -.  2  ||  P )
12761adantl 277 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  (
x  x.  2 )  e.  ZZ )
128125, 127zsubcld 9434 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  ( P  -  ( x  x.  2 ) )  e.  ZZ )
129125, 126, 1283jca 1179 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  ( P  e.  ZZ  /\  -.  2  ||  P  /\  ( P  -  ( x  x.  2 ) )  e.  ZZ ) )
130129adantr 276 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( P  e.  NN  /\  -.  2  ||  P )  /\  x  e.  ( 1 ... H
) )  /\  ( P  /  2 )  <_ 
( x  x.  2 ) )  ->  ( P  e.  ZZ  /\  -.  2  ||  P  /\  ( P  -  ( x  x.  2 ) )  e.  ZZ ) )
131 ltoddhalfle 12024 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e.  ZZ  /\  -.  2  ||  P  /\  ( P  -  (
x  x.  2 ) )  e.  ZZ )  ->  ( ( P  -  ( x  x.  2 ) )  < 
( P  /  2
)  <->  ( P  -  ( x  x.  2
) )  <_  (
( P  -  1 )  /  2 ) ) )
132130, 131syl 14 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( P  e.  NN  /\  -.  2  ||  P )  /\  x  e.  ( 1 ... H
) )  /\  ( P  /  2 )  <_ 
( x  x.  2 ) )  ->  (
( P  -  (
x  x.  2 ) )  <  ( P  /  2 )  <->  ( P  -  ( x  x.  2 ) )  <_ 
( ( P  - 
1 )  /  2
) ) )
133124, 132mpbid 147 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( P  e.  NN  /\  -.  2  ||  P )  /\  x  e.  ( 1 ... H
) )  /\  ( P  /  2 )  <_ 
( x  x.  2 ) )  ->  ( P  -  ( x  x.  2 ) )  <_ 
( ( P  - 
1 )  /  2
) )
134133ex 115 . . . . . . . . . . . . . . . 16  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  (
( P  /  2
)  <_  ( x  x.  2 )  ->  ( P  -  ( x  x.  2 ) )  <_ 
( ( P  - 
1 )  /  2
) ) )
13514breq2i 4037 . . . . . . . . . . . . . . . 16  |-  ( ( P  -  ( x  x.  2 ) )  <_  H  <->  ( P  -  ( x  x.  2 ) )  <_ 
( ( P  - 
1 )  /  2
) )
136134, 135imbitrrdi 162 . . . . . . . . . . . . . . 15  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  (
( P  /  2
)  <_  ( x  x.  2 )  ->  ( P  -  ( x  x.  2 ) )  <_  H ) )
137105, 136sylbird 170 . . . . . . . . . . . . . 14  |-  ( ( ( P  e.  NN  /\ 
-.  2  ||  P
)  /\  x  e.  ( 1 ... H
) )  ->  ( -.  ( x  x.  2 )  <  ( P  /  2 )  -> 
( P  -  (
x  x.  2 ) )  <_  H )
)
138137ex 115 . . . . . . . . . . . . 13  |-  ( ( P  e.  NN  /\  -.  2  ||  P )  ->  ( x  e.  ( 1 ... H
)  ->  ( -.  ( x  x.  2
)  <  ( P  /  2 )  -> 
( P  -  (
x  x.  2 ) )  <_  H )
) )
13919, 20, 1383syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  ( 1 ... H )  ->  ( -.  (
x  x.  2 )  <  ( P  / 
2 )  ->  ( P  -  ( x  x.  2 ) )  <_  H ) ) )
140139imp 124 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... H
) )  ->  ( -.  ( x  x.  2 )  <  ( P  /  2 )  -> 
( P  -  (
x  x.  2 ) )  <_  H )
)
141140impcom 125 . . . . . . . . . 10  |-  ( ( -.  ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( P  -  (
x  x.  2 ) )  <_  H )
142 elfz1b 10146 . . . . . . . . . 10  |-  ( ( P  -  ( x  x.  2 ) )  e.  ( 1 ... H )  <->  ( ( P  -  ( x  x.  2 ) )  e.  NN  /\  H  e.  NN  /\  ( P  -  ( x  x.  2 ) )  <_  H ) )
14397, 99, 141, 142syl3anbrc 1183 . . . . . . . . 9  |-  ( ( -.  ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( P  -  (
x  x.  2 ) )  e.  ( 1 ... H ) )
144 eleq1 2256 . . . . . . . . 9  |-  ( y  =  ( P  -  ( x  x.  2
) )  ->  (
y  e.  ( 1 ... H )  <->  ( P  -  ( x  x.  2 ) )  e.  ( 1 ... H
) ) )
145143, 144syl5ibrcom 157 . . . . . . . 8  |-  ( ( -.  ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( y  =  ( P  -  ( x  x.  2 ) )  ->  y  e.  ( 1 ... H ) ) )
14654, 145sylbid 150 . . . . . . 7  |-  ( ( -.  ( x  x.  2 )  <  ( P  /  2 )  /\  ( ph  /\  x  e.  ( 1 ... H
) ) )  -> 
( y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  ->  y  e.  ( 1 ... H ) ) )
147146ancoms 268 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( 1 ... H
) )  /\  -.  ( x  x.  2
)  <  ( P  /  2 ) )  ->  ( y  =  if ( ( x  x.  2 )  < 
( P  /  2
) ,  ( x  x.  2 ) ,  ( P  -  (
x  x.  2 ) ) )  ->  y  e.  ( 1 ... H
) ) )
14861adantl 277 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... H
) )  ->  (
x  x.  2 )  e.  ZZ )
149 zq 9681 . . . . . . . . 9  |-  ( ( x  x.  2 )  e.  ZZ  ->  (
x  x.  2 )  e.  QQ )
150148, 149syl 14 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... H
) )  ->  (
x  x.  2 )  e.  QQ )
15157adantr 276 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... H
) )  ->  P  e.  ZZ )
152 znq 9679 . . . . . . . . 9  |-  ( ( P  e.  ZZ  /\  2  e.  NN )  ->  ( P  /  2
)  e.  QQ )
153151, 9, 152sylancl 413 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... H
) )  ->  ( P  /  2 )  e.  QQ )
154 qdclt 10305 . . . . . . . 8  |-  ( ( ( x  x.  2 )  e.  QQ  /\  ( P  /  2
)  e.  QQ )  -> DECID 
( x  x.  2 )  <  ( P  /  2 ) )
155150, 153, 154syl2anc 411 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... H
) )  -> DECID  ( x  x.  2 )  <  ( P  /  2 ) )
156 exmiddc 837 . . . . . . 7  |-  (DECID  ( x  x.  2 )  < 
( P  /  2
)  ->  ( (
x  x.  2 )  <  ( P  / 
2 )  \/  -.  ( x  x.  2
)  <  ( P  /  2 ) ) )
157155, 156syl 14 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... H
) )  ->  (
( x  x.  2 )  <  ( P  /  2 )  \/ 
-.  ( x  x.  2 )  <  ( P  /  2 ) ) )
15851, 147, 157mpjaodan 799 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... H
) )  ->  (
y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  ->  y  e.  ( 1 ... H ) ) )
159158rexlimdva 2611 . . . 4  |-  ( ph  ->  ( E. x  e.  ( 1 ... H
) y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  ->  y  e.  ( 1 ... H ) ) )
160 elfz1b 10146 . . . . . . . . . . . 12  |-  ( y  e.  ( 1 ... H )  <->  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )
161 simp1 999 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H )  ->  y  e.  NN )
162 simpl 109 . . . . . . . . . . . . . . 15  |-  ( ( 2  ||  y  /\  ph )  ->  2  ||  y )
163 nnehalf 12035 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN  /\  2  ||  y )  -> 
( y  /  2
)  e.  NN )
164161, 162, 163syl2anr 290 . . . . . . . . . . . . . 14  |-  ( ( ( 2  ||  y  /\  ph )  /\  (
y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  -> 
( y  /  2
)  e.  NN )
165 simpr2 1006 . . . . . . . . . . . . . 14  |-  ( ( ( 2  ||  y  /\  ph )  /\  (
y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  H  e.  NN )
166 nnre 8979 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  y  e.  RR )
167166ad2antrr 488 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( 2  ||  y  /\  ph ) )  ->  y  e.  RR )
168 nnrp 9719 . . . . . . . . . . . . . . . . . . . . 21  |-  ( H  e.  NN  ->  H  e.  RR+ )
169168adantl 277 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  NN  /\  H  e.  NN )  ->  H  e.  RR+ )
170169adantr 276 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( 2  ||  y  /\  ph ) )  ->  H  e.  RR+ )
171 2rp 9714 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR+
172 1le2 9180 . . . . . . . . . . . . . . . . . . . . 21  |-  1  <_  2
173171, 172pm3.2i 272 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2  e.  RR+  /\  1  <_  2 )
174173a1i 9 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( 2  ||  y  /\  ph ) )  ->  ( 2  e.  RR+  /\  1  <_  2
) )
175 ledivge1le 9782 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  RR  /\  H  e.  RR+  /\  (
2  e.  RR+  /\  1  <_  2 ) )  -> 
( y  <_  H  ->  ( y  /  2
)  <_  H )
)
176167, 170, 174, 175syl3anc 1249 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( 2  ||  y  /\  ph ) )  ->  ( y  <_  H  ->  ( y  / 
2 )  <_  H
) )
177176ex 115 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  NN  /\  H  e.  NN )  ->  ( ( 2  ||  y  /\  ph )  -> 
( y  <_  H  ->  ( y  /  2
)  <_  H )
) )
178177com23 78 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  NN  /\  H  e.  NN )  ->  ( y  <_  H  ->  ( ( 2  ||  y  /\  ph )  -> 
( y  /  2
)  <_  H )
) )
1791783impia 1202 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H )  ->  (
( 2  ||  y  /\  ph )  ->  (
y  /  2 )  <_  H ) )
180179impcom 125 . . . . . . . . . . . . . 14  |-  ( ( ( 2  ||  y  /\  ph )  /\  (
y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  -> 
( y  /  2
)  <_  H )
181164, 165, 1803jca 1179 . . . . . . . . . . . . 13  |-  ( ( ( 2  ||  y  /\  ph )  /\  (
y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  -> 
( ( y  / 
2 )  e.  NN  /\  H  e.  NN  /\  ( y  /  2
)  <_  H )
)
182181ex 115 . . . . . . . . . . . 12  |-  ( ( 2  ||  y  /\  ph )  ->  ( (
y  e.  NN  /\  H  e.  NN  /\  y  <_  H )  ->  (
( y  /  2
)  e.  NN  /\  H  e.  NN  /\  (
y  /  2 )  <_  H ) ) )
183160, 182biimtrid 152 . . . . . . . . . . 11  |-  ( ( 2  ||  y  /\  ph )  ->  ( y  e.  ( 1 ... H
)  ->  ( (
y  /  2 )  e.  NN  /\  H  e.  NN  /\  ( y  /  2 )  <_  H ) ) )
1841833impia 1202 . . . . . . . . . 10  |-  ( ( 2  ||  y  /\  ph 
/\  y  e.  ( 1 ... H ) )  ->  ( (
y  /  2 )  e.  NN  /\  H  e.  NN  /\  ( y  /  2 )  <_  H ) )
185 elfz1b 10146 . . . . . . . . . 10  |-  ( ( y  /  2 )  e.  ( 1 ... H )  <->  ( (
y  /  2 )  e.  NN  /\  H  e.  NN  /\  ( y  /  2 )  <_  H ) )
186184, 185sylibr 134 . . . . . . . . 9  |-  ( ( 2  ||  y  /\  ph 
/\  y  e.  ( 1 ... H ) )  ->  ( y  /  2 )  e.  ( 1 ... H
) )
187 oveq1 5917 . . . . . . . . . . . . 13  |-  ( x  =  ( y  / 
2 )  ->  (
x  x.  2 )  =  ( ( y  /  2 )  x.  2 ) )
188187breq1d 4039 . . . . . . . . . . . 12  |-  ( x  =  ( y  / 
2 )  ->  (
( x  x.  2 )  <  ( P  /  2 )  <->  ( (
y  /  2 )  x.  2 )  < 
( P  /  2
) ) )
189187oveq2d 5926 . . . . . . . . . . . 12  |-  ( x  =  ( y  / 
2 )  ->  ( P  -  ( x  x.  2 ) )  =  ( P  -  (
( y  /  2
)  x.  2 ) ) )
190188, 187, 189ifbieq12d 3583 . . . . . . . . . . 11  |-  ( x  =  ( y  / 
2 )  ->  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  =  if ( ( ( y  /  2
)  x.  2 )  <  ( P  / 
2 ) ,  ( ( y  /  2
)  x.  2 ) ,  ( P  -  ( ( y  / 
2 )  x.  2 ) ) ) )
191190eqeq2d 2205 . . . . . . . . . 10  |-  ( x  =  ( y  / 
2 )  ->  (
y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  <-> 
y  =  if ( ( ( y  / 
2 )  x.  2 )  <  ( P  /  2 ) ,  ( ( y  / 
2 )  x.  2 ) ,  ( P  -  ( ( y  /  2 )  x.  2 ) ) ) ) )
192191adantl 277 . . . . . . . . 9  |-  ( ( ( 2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  /\  x  =  ( y  / 
2 ) )  -> 
( y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  <-> 
y  =  if ( ( ( y  / 
2 )  x.  2 )  <  ( P  /  2 ) ,  ( ( y  / 
2 )  x.  2 ) ,  ( P  -  ( ( y  /  2 )  x.  2 ) ) ) ) )
193 elfzelz 10081 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 1 ... H )  ->  y  e.  ZZ )
194193zcnd 9430 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 1 ... H )  ->  y  e.  CC )
1951943ad2ant3 1022 . . . . . . . . . . . . 13  |-  ( ( 2  ||  y  /\  ph 
/\  y  e.  ( 1 ... H ) )  ->  y  e.  CC )
196 2cnd 9045 . . . . . . . . . . . . 13  |-  ( ( 2  ||  y  /\  ph 
/\  y  e.  ( 1 ... H ) )  ->  2  e.  CC )
197 2ap0 9065 . . . . . . . . . . . . . 14  |-  2 #  0
198197a1i 9 . . . . . . . . . . . . 13  |-  ( ( 2  ||  y  /\  ph 
/\  y  e.  ( 1 ... H ) )  ->  2 #  0
)
199195, 196, 198divcanap1d 8800 . . . . . . . . . . . 12  |-  ( ( 2  ||  y  /\  ph 
/\  y  e.  ( 1 ... H ) )  ->  ( (
y  /  2 )  x.  2 )  =  y )
20014breq2i 4037 . . . . . . . . . . . . . . . . . 18  |-  ( y  <_  H  <->  y  <_  ( ( P  -  1 )  /  2 ) )
201 nnz 9326 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  NN  ->  y  e.  ZZ )
20219, 20, 223syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( P  e.  ZZ  /\ 
-.  2  ||  P
) )
203202adantl 277 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2  ||  y  /\  ph )  ->  ( P  e.  ZZ  /\  -.  2  ||  P ) )
204201, 203anim12ci 339 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  NN  /\  ( 2  ||  y  /\  ph ) )  -> 
( ( P  e.  ZZ  /\  -.  2  ||  P )  /\  y  e.  ZZ ) )
205 df-3an 982 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( P  e.  ZZ  /\  -.  2  ||  P  /\  y  e.  ZZ )  <->  ( ( P  e.  ZZ  /\ 
-.  2  ||  P
)  /\  y  e.  ZZ ) )
206204, 205sylibr 134 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  NN  /\  ( 2  ||  y  /\  ph ) )  -> 
( P  e.  ZZ  /\ 
-.  2  ||  P  /\  y  e.  ZZ ) )
207 ltoddhalfle 12024 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( P  e.  ZZ  /\  -.  2  ||  P  /\  y  e.  ZZ )  ->  ( y  <  ( P  /  2 )  <->  y  <_  ( ( P  -  1 )  /  2 ) ) )
208206, 207syl 14 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  NN  /\  ( 2  ||  y  /\  ph ) )  -> 
( y  <  ( P  /  2 )  <->  y  <_  ( ( P  -  1 )  /  2 ) ) )
209208exbiri 382 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
( 2  ||  y  /\  ph )  ->  (
y  <_  ( ( P  -  1 )  /  2 )  -> 
y  <  ( P  /  2 ) ) ) )
210209com23 78 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
y  <_  ( ( P  -  1 )  /  2 )  -> 
( ( 2  ||  y  /\  ph )  -> 
y  <  ( P  /  2 ) ) ) )
211200, 210biimtrid 152 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
y  <_  H  ->  ( ( 2  ||  y  /\  ph )  ->  y  <  ( P  /  2
) ) ) )
212211a1d 22 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  ( H  e.  NN  ->  ( y  <_  H  ->  ( ( 2  ||  y  /\  ph )  ->  y  <  ( P  /  2
) ) ) ) )
2132123imp 1195 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H )  ->  (
( 2  ||  y  /\  ph )  ->  y  <  ( P  /  2
) ) )
214160, 213sylbi 121 . . . . . . . . . . . . . 14  |-  ( y  e.  ( 1 ... H )  ->  (
( 2  ||  y  /\  ph )  ->  y  <  ( P  /  2
) ) )
215214com12 30 . . . . . . . . . . . . 13  |-  ( ( 2  ||  y  /\  ph )  ->  ( y  e.  ( 1 ... H
)  ->  y  <  ( P  /  2 ) ) )
2162153impia 1202 . . . . . . . . . . . 12  |-  ( ( 2  ||  y  /\  ph 
/\  y  e.  ( 1 ... H ) )  ->  y  <  ( P  /  2 ) )
217199, 216eqbrtrd 4051 . . . . . . . . . . 11  |-  ( ( 2  ||  y  /\  ph 
/\  y  e.  ( 1 ... H ) )  ->  ( (
y  /  2 )  x.  2 )  < 
( P  /  2
) )
218217iftrued 3564 . . . . . . . . . 10  |-  ( ( 2  ||  y  /\  ph 
/\  y  e.  ( 1 ... H ) )  ->  if (
( ( y  / 
2 )  x.  2 )  <  ( P  /  2 ) ,  ( ( y  / 
2 )  x.  2 ) ,  ( P  -  ( ( y  /  2 )  x.  2 ) ) )  =  ( ( y  /  2 )  x.  2 ) )
219218, 199eqtr2d 2227 . . . . . . . . 9  |-  ( ( 2  ||  y  /\  ph 
/\  y  e.  ( 1 ... H ) )  ->  y  =  if ( ( ( y  /  2 )  x.  2 )  <  ( P  /  2 ) ,  ( ( y  / 
2 )  x.  2 ) ,  ( P  -  ( ( y  /  2 )  x.  2 ) ) ) )
220186, 192, 219rspcedvd 2870 . . . . . . . 8  |-  ( ( 2  ||  y  /\  ph 
/\  y  e.  ( 1 ... H ) )  ->  E. x  e.  ( 1 ... H
) y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) ) )
2212203expb 1206 . . . . . . 7  |-  ( ( 2  ||  y  /\  ( ph  /\  y  e.  ( 1 ... H
) ) )  ->  E. x  e.  (
1 ... H ) y  =  if ( ( x  x.  2 )  <  ( P  / 
2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2
) ) ) )
222221ancoms 268 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( 1 ... H
) )  /\  2  ||  y )  ->  E. x  e.  ( 1 ... H
) y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) ) )
22355, 56syl 14 . . . . . . . . . . . . . . . . . . 19  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  e.  ZZ )
224223ad2antrr 488 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  P  e.  ZZ )
2252013ad2ant1 1020 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H )  ->  y  e.  ZZ )
226225adantl 277 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  y  e.  ZZ )
227224, 226zsubcld 9434 . . . . . . . . . . . . . . . . 17  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( P  -  y )  e.  ZZ )
228166ad2antrl 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( P  e.  RR  /\  ( y  e.  NN  /\  H  e.  NN ) )  ->  y  e.  RR )
22968rehalfcld 9219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e.  RR  ->  (
( P  -  1 )  /  2 )  e.  RR )
230229adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( P  e.  RR  /\  ( y  e.  NN  /\  H  e.  NN ) )  ->  ( ( P  -  1 )  /  2 )  e.  RR )
231 simpl 109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( P  e.  RR  /\  ( y  e.  NN  /\  H  e.  NN ) )  ->  P  e.  RR )
232228, 230, 2313jca 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( P  e.  RR  /\  ( y  e.  NN  /\  H  e.  NN ) )  ->  ( y  e.  RR  /\  ( ( P  -  1 )  /  2 )  e.  RR  /\  P  e.  RR ) )
233232ex 115 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  RR  ->  (
( y  e.  NN  /\  H  e.  NN )  ->  ( y  e.  RR  /\  ( ( P  -  1 )  /  2 )  e.  RR  /\  P  e.  RR ) ) )
23455, 64, 2333syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( y  e.  NN  /\  H  e.  NN )  ->  (
y  e.  RR  /\  ( ( P  - 
1 )  /  2
)  e.  RR  /\  P  e.  RR )
) )
235234adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  ->  (
( y  e.  NN  /\  H  e.  NN )  ->  ( y  e.  RR  /\  ( ( P  -  1 )  /  2 )  e.  RR  /\  P  e.  RR ) ) )
236235impcom 125 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y ) )  ->  ( y  e.  RR  /\  ( ( P  -  1 )  /  2 )  e.  RR  /\  P  e.  RR ) )
237 lesub2 8466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  e.  RR  /\  ( ( P  - 
1 )  /  2
)  e.  RR  /\  P  e.  RR )  ->  ( y  <_  (
( P  -  1 )  /  2 )  <-> 
( P  -  (
( P  -  1 )  /  2 ) )  <_  ( P  -  y ) ) )
238236, 237syl 14 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y ) )  ->  ( y  <_ 
( ( P  - 
1 )  /  2
)  <->  ( P  -  ( ( P  - 
1 )  /  2
) )  <_  ( P  -  y )
) )
23956zcnd 9430 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  Prime  ->  P  e.  CC )
240 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e.  CC  ->  P  e.  CC )
241 1cnd 8025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e.  CC  ->  1  e.  CC )
242 2cnd 9045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e.  CC  ->  2  e.  CC )
243197a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e.  CC  ->  2 #  0 )
244240, 241, 242, 243divsubdirapd 8839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e.  CC  ->  (
( P  -  1 )  /  2 )  =  ( ( P  /  2 )  -  ( 1  /  2
) ) )
245244oveq2d 5926 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( P  e.  CC  ->  ( P  -  ( ( P  -  1 )  /  2 ) )  =  ( P  -  ( ( P  / 
2 )  -  (
1  /  2 ) ) ) )
246 halfcl 9198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e.  CC  ->  ( P  /  2 )  e.  CC )
247 halfcn 9186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 1  /  2 )  e.  CC
248247a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e.  CC  ->  (
1  /  2 )  e.  CC )
249240, 246, 248subsubd 8348 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( P  e.  CC  ->  ( P  -  ( ( P  /  2 )  -  ( 1  /  2
) ) )  =  ( ( P  -  ( P  /  2
) )  +  ( 1  /  2 ) ) )
250112oveq1d 5925 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( P  e.  CC  ->  (
( P  -  ( P  /  2 ) )  +  ( 1  / 
2 ) )  =  ( ( P  / 
2 )  +  ( 1  /  2 ) ) )
251245, 249, 2503eqtrd 2230 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  CC  ->  ( P  -  ( ( P  -  1 )  /  2 ) )  =  ( ( P  /  2 )  +  ( 1  /  2
) ) )
25255, 239, 2513syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( P  -  (
( P  -  1 )  /  2 ) )  =  ( ( P  /  2 )  +  ( 1  / 
2 ) ) )
253252ad2antrl 490 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y ) )  ->  ( P  -  ( ( P  - 
1 )  /  2
) )  =  ( ( P  /  2
)  +  ( 1  /  2 ) ) )
254253breq1d 4039 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y ) )  ->  ( ( P  -  ( ( P  -  1 )  / 
2 ) )  <_ 
( P  -  y
)  <->  ( ( P  /  2 )  +  ( 1  /  2
) )  <_  ( P  -  y )
) )
255 prmnn 12238 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  Prime  ->  P  e.  NN )
256 halfre 9185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 1  /  2 )  e.  RR
257256a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( P  e.  NN  ->  (
1  /  2 )  e.  RR )
258 nngt0 8997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e.  NN  ->  0  <  P )
25972a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e.  NN  ->  (
2  e.  RR  /\  0  <  2 ) )
260 divgt0 8881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( P  e.  RR  /\  0  <  P )  /\  ( 2  e.  RR  /\  0  <  2 ) )  -> 
0  <  ( P  /  2 ) )
261100, 258, 259, 260syl21anc 1248 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( P  e.  NN  ->  0  <  ( P  /  2
) )
262 halfgt0 9187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  0  <  ( 1  /  2
)
263262a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( P  e.  NN  ->  0  <  ( 1  /  2
) )
264101, 257, 261, 263addgt0d 8530 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( P  e.  NN  ->  0  <  ( ( P  / 
2 )  +  ( 1  /  2 ) ) )
26555, 255, 2643syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
0  <  ( ( P  /  2 )  +  ( 1  /  2
) ) )
266265ad2antrl 490 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y ) )  ->  0  <  (
( P  /  2
)  +  ( 1  /  2 ) ) )
267 0red 8010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  0  e.  RR )
268 simpr 110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  P  e.  RR )
269268rehalfcld 9219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( P  /  2
)  e.  RR )
270256a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( 1  /  2
)  e.  RR )
271269, 270readdcld 8039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( ( P  / 
2 )  +  ( 1  /  2 ) )  e.  RR )
272 resubcl 8273 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( P  e.  RR  /\  y  e.  RR )  ->  ( P  -  y
)  e.  RR )
273272ancoms 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( P  -  y
)  e.  RR )
274267, 271, 2733jca 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( 0  e.  RR  /\  ( ( P  / 
2 )  +  ( 1  /  2 ) )  e.  RR  /\  ( P  -  y
)  e.  RR ) )
275274ex 115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  e.  RR  ->  ( P  e.  RR  ->  ( 0  e.  RR  /\  ( ( P  / 
2 )  +  ( 1  /  2 ) )  e.  RR  /\  ( P  -  y
)  e.  RR ) ) )
276166, 275syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  NN  ->  ( P  e.  RR  ->  ( 0  e.  RR  /\  ( ( P  / 
2 )  +  ( 1  /  2 ) )  e.  RR  /\  ( P  -  y
)  e.  RR ) ) )
277276adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( y  e.  NN  /\  H  e.  NN )  ->  ( P  e.  RR  ->  ( 0  e.  RR  /\  ( ( P  / 
2 )  +  ( 1  /  2 ) )  e.  RR  /\  ( P  -  y
)  e.  RR ) ) )
278277com12 30 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e.  RR  ->  (
( y  e.  NN  /\  H  e.  NN )  ->  ( 0  e.  RR  /\  ( ( P  /  2 )  +  ( 1  / 
2 ) )  e.  RR  /\  ( P  -  y )  e.  RR ) ) )
27955, 64, 2783syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( y  e.  NN  /\  H  e.  NN )  ->  (
0  e.  RR  /\  ( ( P  / 
2 )  +  ( 1  /  2 ) )  e.  RR  /\  ( P  -  y
)  e.  RR ) ) )
280279adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  ->  (
( y  e.  NN  /\  H  e.  NN )  ->  ( 0  e.  RR  /\  ( ( P  /  2 )  +  ( 1  / 
2 ) )  e.  RR  /\  ( P  -  y )  e.  RR ) ) )
281280impcom 125 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y ) )  ->  ( 0  e.  RR  /\  ( ( P  /  2 )  +  ( 1  / 
2 ) )  e.  RR  /\  ( P  -  y )  e.  RR ) )
282 ltletr 8099 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 0  e.  RR  /\  ( ( P  / 
2 )  +  ( 1  /  2 ) )  e.  RR  /\  ( P  -  y
)  e.  RR )  ->  ( ( 0  <  ( ( P  /  2 )  +  ( 1  /  2
) )  /\  (
( P  /  2
)  +  ( 1  /  2 ) )  <_  ( P  -  y ) )  -> 
0  <  ( P  -  y ) ) )
283281, 282syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y ) )  ->  ( ( 0  <  ( ( P  /  2 )  +  ( 1  /  2
) )  /\  (
( P  /  2
)  +  ( 1  /  2 ) )  <_  ( P  -  y ) )  -> 
0  <  ( P  -  y ) ) )
284266, 283mpand 429 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y ) )  ->  ( ( ( P  /  2 )  +  ( 1  / 
2 ) )  <_ 
( P  -  y
)  ->  0  <  ( P  -  y ) ) )
285254, 284sylbid 150 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y ) )  ->  ( ( P  -  ( ( P  -  1 )  / 
2 ) )  <_ 
( P  -  y
)  ->  0  <  ( P  -  y ) ) )
286238, 285sylbid 150 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( y  e.  NN  /\  H  e.  NN )  /\  ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y ) )  ->  ( y  <_ 
( ( P  - 
1 )  /  2
)  ->  0  <  ( P  -  y ) ) )
287286ex 115 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  NN  /\  H  e.  NN )  ->  ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  -> 
( y  <_  (
( P  -  1 )  /  2 )  ->  0  <  ( P  -  y )
) ) )
288287com23 78 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  NN  /\  H  e.  NN )  ->  ( y  <_  (
( P  -  1 )  /  2 )  ->  ( ( P  e.  ( Prime  \  {
2 } )  /\  -.  2  ||  y )  ->  0  <  ( P  -  y )
) ) )
289200, 288biimtrid 152 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN  /\  H  e.  NN )  ->  ( y  <_  H  ->  ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  -> 
0  <  ( P  -  y ) ) ) )
2902893impia 1202 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H )  ->  (
( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  -> 
0  <  ( P  -  y ) ) )
291290impcom 125 . . . . . . . . . . . . . . . . 17  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  0  <  ( P  -  y )
)
292 elnnz 9317 . . . . . . . . . . . . . . . . 17  |-  ( ( P  -  y )  e.  NN  <->  ( ( P  -  y )  e.  ZZ  /\  0  < 
( P  -  y
) ) )
293227, 291, 292sylanbrc 417 . . . . . . . . . . . . . . . 16  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( P  -  y )  e.  NN )
29423adantr 276 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  ->  ( P  e.  ZZ  /\  -.  2  ||  P ) )
295 simpr 110 . . . . . . . . . . . . . . . . . 18  |-  ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  ->  -.  2  ||  y )
296295, 225anim12ci 339 . . . . . . . . . . . . . . . . 17  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( y  e.  ZZ  /\  -.  2  ||  y ) )
297 omoe 12027 . . . . . . . . . . . . . . . . 17  |-  ( ( ( P  e.  ZZ  /\ 
-.  2  ||  P
)  /\  ( y  e.  ZZ  /\  -.  2  ||  y ) )  -> 
2  ||  ( P  -  y ) )
298294, 296, 297syl2an2r 595 . . . . . . . . . . . . . . . 16  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  2  ||  ( P  -  y )
)
299 nnehalf 12035 . . . . . . . . . . . . . . . 16  |-  ( ( ( P  -  y
)  e.  NN  /\  2  ||  ( P  -  y ) )  -> 
( ( P  -  y )  /  2
)  e.  NN )
300293, 298, 299syl2anc 411 . . . . . . . . . . . . . . 15  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( ( P  -  y )  / 
2 )  e.  NN )
301 simpr2 1006 . . . . . . . . . . . . . . 15  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  H  e.  NN )
302 1red 8024 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  1  e.  RR )
3031663ad2ant1 1020 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H )  ->  y  e.  RR )
304303adantl 277 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  y  e.  RR )
30555, 64syl 14 . . . . . . . . . . . . . . . . . . 19  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  e.  RR )
306305ad2antrr 488 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  P  e.  RR )
307 nnge1 8995 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN  ->  1  <_  y )
3083073ad2ant1 1020 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H )  ->  1  <_  y )
309308adantl 277 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  1  <_  y
)
310302, 304, 306, 309lesub2dd 8571 . . . . . . . . . . . . . . . . 17  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( P  -  y )  <_  ( P  -  1 ) )
311306, 304resubcld 8390 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( P  -  y )  e.  RR )
31255, 64, 683syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( P  -  1 )  e.  RR )
313312ad2antrr 488 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( P  - 
1 )  e.  RR )
31472a1i 9 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( 2  e.  RR  /\  0  <  2 ) )
315 lediv1 8878 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( P  -  y
)  e.  RR  /\  ( P  -  1
)  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( ( P  -  y )  <_  ( P  -  1 )  <->  ( ( P  -  y )  / 
2 )  <_  (
( P  -  1 )  /  2 ) ) )
316311, 313, 314, 315syl3anc 1249 . . . . . . . . . . . . . . . . 17  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( ( P  -  y )  <_ 
( P  -  1 )  <->  ( ( P  -  y )  / 
2 )  <_  (
( P  -  1 )  /  2 ) ) )
317310, 316mpbid 147 . . . . . . . . . . . . . . . 16  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( ( P  -  y )  / 
2 )  <_  (
( P  -  1 )  /  2 ) )
31814breq2i 4037 . . . . . . . . . . . . . . . 16  |-  ( ( ( P  -  y
)  /  2 )  <_  H  <->  ( ( P  -  y )  /  2 )  <_ 
( ( P  - 
1 )  /  2
) )
319317, 318sylibr 134 . . . . . . . . . . . . . . 15  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( ( P  -  y )  / 
2 )  <_  H
)
320300, 301, 3193jca 1179 . . . . . . . . . . . . . 14  |-  ( ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  /\  ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H ) )  ->  ( ( ( P  -  y )  /  2 )  e.  NN  /\  H  e.  NN  /\  ( ( P  -  y )  /  2 )  <_  H ) )
321320ex 115 . . . . . . . . . . . . 13  |-  ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  ->  (
( y  e.  NN  /\  H  e.  NN  /\  y  <_  H )  -> 
( ( ( P  -  y )  / 
2 )  e.  NN  /\  H  e.  NN  /\  ( ( P  -  y )  /  2
)  <_  H )
) )
322 elfz1b 10146 . . . . . . . . . . . . 13  |-  ( ( ( P  -  y
)  /  2 )  e.  ( 1 ... H )  <->  ( (
( P  -  y
)  /  2 )  e.  NN  /\  H  e.  NN  /\  ( ( P  -  y )  /  2 )  <_  H ) )
323321, 160, 3223imtr4g 205 . . . . . . . . . . . 12  |-  ( ( P  e.  ( Prime  \  { 2 } )  /\  -.  2  ||  y )  ->  (
y  e.  ( 1 ... H )  -> 
( ( P  -  y )  /  2
)  e.  ( 1 ... H ) ) )
324323ex 115 . . . . . . . . . . 11  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( -.  2  ||  y  ->  ( y  e.  ( 1 ... H
)  ->  ( ( P  -  y )  /  2 )  e.  ( 1 ... H
) ) ) )
32519, 324syl 14 . . . . . . . . . 10  |-  ( ph  ->  ( -.  2  ||  y  ->  ( y  e.  ( 1 ... H
)  ->  ( ( P  -  y )  /  2 )  e.  ( 1 ... H
) ) ) )
3263253imp21 1200 . . . . . . . . 9  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  (
( P  -  y
)  /  2 )  e.  ( 1 ... H ) )
327 oveq1 5917 . . . . . . . . . . . . 13  |-  ( x  =  ( ( P  -  y )  / 
2 )  ->  (
x  x.  2 )  =  ( ( ( P  -  y )  /  2 )  x.  2 ) )
328327breq1d 4039 . . . . . . . . . . . 12  |-  ( x  =  ( ( P  -  y )  / 
2 )  ->  (
( x  x.  2 )  <  ( P  /  2 )  <->  ( (
( P  -  y
)  /  2 )  x.  2 )  < 
( P  /  2
) ) )
329327oveq2d 5926 . . . . . . . . . . . 12  |-  ( x  =  ( ( P  -  y )  / 
2 )  ->  ( P  -  ( x  x.  2 ) )  =  ( P  -  (
( ( P  -  y )  /  2
)  x.  2 ) ) )
330328, 327, 329ifbieq12d 3583 . . . . . . . . . . 11  |-  ( x  =  ( ( P  -  y )  / 
2 )  ->  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  =  if ( ( ( ( P  -  y )  /  2
)  x.  2 )  <  ( P  / 
2 ) ,  ( ( ( P  -  y )  /  2
)  x.  2 ) ,  ( P  -  ( ( ( P  -  y )  / 
2 )  x.  2 ) ) ) )
331330eqeq2d 2205 . . . . . . . . . 10  |-  ( x  =  ( ( P  -  y )  / 
2 )  ->  (
y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  <-> 
y  =  if ( ( ( ( P  -  y )  / 
2 )  x.  2 )  <  ( P  /  2 ) ,  ( ( ( P  -  y )  / 
2 )  x.  2 ) ,  ( P  -  ( ( ( P  -  y )  /  2 )  x.  2 ) ) ) ) )
332331adantl 277 . . . . . . . . 9  |-  ( ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  /\  x  =  ( ( P  -  y )  / 
2 ) )  -> 
( y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  <-> 
y  =  if ( ( ( ( P  -  y )  / 
2 )  x.  2 )  <  ( P  /  2 ) ,  ( ( ( P  -  y )  / 
2 )  x.  2 ) ,  ( P  -  ( ( ( P  -  y )  /  2 )  x.  2 ) ) ) ) )
33319, 55, 2393syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  P  e.  CC )
3343333ad2ant2 1021 . . . . . . . . . . . . . 14  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  P  e.  CC )
3351943ad2ant3 1022 . . . . . . . . . . . . . 14  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  y  e.  CC )
336334, 335subcld 8320 . . . . . . . . . . . . 13  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  ( P  -  y )  e.  CC )
337 2cnd 9045 . . . . . . . . . . . . 13  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  2  e.  CC )
338197a1i 9 . . . . . . . . . . . . 13  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  2 #  0 )
339336, 337, 338divcanap1d 8800 . . . . . . . . . . . 12  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  (
( ( P  -  y )  /  2
)  x.  2 )  =  ( P  -  y ) )
340 zre 9311 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  ZZ  ->  P  e.  RR )
341 halfge0 9188 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  <_  ( 1  /  2
)
342 rehalfcl 9199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e.  RR  ->  ( P  /  2 )  e.  RR )
343342adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( P  /  2
)  e.  RR )
344343, 270subge02d 8546 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( 0  <_  (
1  /  2 )  <-> 
( ( P  / 
2 )  -  (
1  /  2 ) )  <_  ( P  /  2 ) ) )
345341, 344mpbii 148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( ( P  / 
2 )  -  (
1  /  2 ) )  <_  ( P  /  2 ) )
346 simpl 109 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  y  e.  RR )
347256a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e.  RR  ->  (
1  /  2 )  e.  RR )
348342, 347resubcld 8390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e.  RR  ->  (
( P  /  2
)  -  ( 1  /  2 ) )  e.  RR )
349348adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( ( P  / 
2 )  -  (
1  /  2 ) )  e.  RR )
350 letr 8092 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( y  e.  RR  /\  ( ( P  / 
2 )  -  (
1  /  2 ) )  e.  RR  /\  ( P  /  2
)  e.  RR )  ->  ( ( y  <_  ( ( P  /  2 )  -  ( 1  /  2
) )  /\  (
( P  /  2
)  -  ( 1  /  2 ) )  <_  ( P  / 
2 ) )  -> 
y  <_  ( P  /  2 ) ) )
351346, 349, 343, 350syl3anc 1249 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( ( y  <_ 
( ( P  / 
2 )  -  (
1  /  2 ) )  /\  ( ( P  /  2 )  -  ( 1  / 
2 ) )  <_ 
( P  /  2
) )  ->  y  <_  ( P  /  2
) ) )
352345, 351mpan2d 428 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( y  <_  (
( P  /  2
)  -  ( 1  /  2 ) )  ->  y  <_  ( P  /  2 ) ) )
35381adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  P  e.  CC )
354353, 244syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( ( P  - 
1 )  /  2
)  =  ( ( P  /  2 )  -  ( 1  / 
2 ) ) )
355354breq2d 4041 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( y  <_  (
( P  -  1 )  /  2 )  <-> 
y  <_  ( ( P  /  2 )  -  ( 1  /  2
) ) ) )
356 lesub 8450 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( P  /  2
)  e.  RR  /\  P  e.  RR  /\  y  e.  RR )  ->  (
( P  /  2
)  <_  ( P  -  y )  <->  y  <_  ( P  -  ( P  /  2 ) ) ) )
357343, 268, 346, 356syl3anc 1249 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( ( P  / 
2 )  <_  ( P  -  y )  <->  y  <_  ( P  -  ( P  /  2
) ) ) )
358269, 273lenltd 8127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( ( P  / 
2 )  <_  ( P  -  y )  <->  -.  ( P  -  y
)  <  ( P  /  2 ) ) )
359 2cnd 9045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( P  e.  RR  ->  2  e.  CC )
360197a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( P  e.  RR  ->  2 #  0 )
36181, 359, 360divcanap1d 8800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( P  e.  RR  ->  (
( P  /  2
)  x.  2 )  =  P )
362361eqcomd 2199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( P  e.  RR  ->  P  =  ( ( P  /  2 )  x.  2 ) )
363362oveq1d 5925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e.  RR  ->  ( P  -  ( P  /  2 ) )  =  ( ( ( P  /  2 )  x.  2 )  -  ( P  /  2
) ) )
364342recnd 8038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( P  e.  RR  ->  ( P  /  2 )  e.  CC )
365364, 359mulcomd 8031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( P  e.  RR  ->  (
( P  /  2
)  x.  2 )  =  ( 2  x.  ( P  /  2
) ) )
366365oveq1d 5925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e.  RR  ->  (
( ( P  / 
2 )  x.  2 )  -  ( P  /  2 ) )  =  ( ( 2  x.  ( P  / 
2 ) )  -  ( P  /  2
) ) )
367359, 364mulsubfacd 8427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( P  e.  RR  ->  (
( 2  x.  ( P  /  2 ) )  -  ( P  / 
2 ) )  =  ( ( 2  -  1 )  x.  ( P  /  2 ) ) )
368 2m1e1 9090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 2  -  1 )  =  1
369368a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( P  e.  RR  ->  (
2  -  1 )  =  1 )
370369oveq1d 5925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( P  e.  RR  ->  (
( 2  -  1 )  x.  ( P  /  2 ) )  =  ( 1  x.  ( P  /  2
) ) )
371364mullidd 8027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( P  e.  RR  ->  (
1  x.  ( P  /  2 ) )  =  ( P  / 
2 ) )
372367, 370, 3713eqtrd 2230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( P  e.  RR  ->  (
( 2  x.  ( P  /  2 ) )  -  ( P  / 
2 ) )  =  ( P  /  2
) )
373363, 366, 3723eqtrd 2230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( P  e.  RR  ->  ( P  -  ( P  /  2 ) )  =  ( P  / 
2 ) )
374373adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( P  -  ( P  /  2 ) )  =  ( P  / 
2 ) )
375374breq2d 4041 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( y  <_  ( P  -  ( P  /  2 ) )  <-> 
y  <_  ( P  /  2 ) ) )
376357, 358, 3753bitr3d 218 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( -.  ( P  -  y )  < 
( P  /  2
)  <->  y  <_  ( P  /  2 ) ) )
377352, 355, 3763imtr4d 203 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( y  e.  RR  /\  P  e.  RR )  ->  ( y  <_  (
( P  -  1 )  /  2 )  ->  -.  ( P  -  y )  < 
( P  /  2
) ) )
378377ex 115 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  RR  ->  ( P  e.  RR  ->  ( y  <_  ( ( P  -  1 )  /  2 )  ->  -.  ( P  -  y
)  <  ( P  /  2 ) ) ) )
379166, 378syl 14 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  NN  ->  ( P  e.  RR  ->  ( y  <_  ( ( P  -  1 )  /  2 )  ->  -.  ( P  -  y
)  <  ( P  /  2 ) ) ) )
380379com3l 81 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( P  e.  RR  ->  (
y  <_  ( ( P  -  1 )  /  2 )  -> 
( y  e.  NN  ->  -.  ( P  -  y )  <  ( P  /  2 ) ) ) )
381340, 380syl 14 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e.  ZZ  ->  (
y  <_  ( ( P  -  1 )  /  2 )  -> 
( y  e.  NN  ->  -.  ( P  -  y )  <  ( P  /  2 ) ) ) )
38219, 55, 56, 3814syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( y  <_  (
( P  -  1 )  /  2 )  ->  ( y  e.  NN  ->  -.  ( P  -  y )  <  ( P  /  2
) ) ) )
383382adantl 277 . . . . . . . . . . . . . . . . . . 19  |-  ( ( -.  2  ||  y  /\  ph )  ->  (
y  <_  ( ( P  -  1 )  /  2 )  -> 
( y  e.  NN  ->  -.  ( P  -  y )  <  ( P  /  2 ) ) ) )
384383com13 80 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
y  <_  ( ( P  -  1 )  /  2 )  -> 
( ( -.  2  ||  y  /\  ph )  ->  -.  ( P  -  y )  <  ( P  /  2 ) ) ) )
385200, 384biimtrid 152 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
y  <_  H  ->  ( ( -.  2  ||  y  /\  ph )  ->  -.  ( P  -  y
)  <  ( P  /  2 ) ) ) )
386385a1d 22 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  ( H  e.  NN  ->  ( y  <_  H  ->  ( ( -.  2  ||  y  /\  ph )  ->  -.  ( P  -  y
)  <  ( P  /  2 ) ) ) ) )
3873863imp 1195 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN  /\  H  e.  NN  /\  y  <_  H )  ->  (
( -.  2  ||  y  /\  ph )  ->  -.  ( P  -  y
)  <  ( P  /  2 ) ) )
388387com12 30 . . . . . . . . . . . . . 14  |-  ( ( -.  2  ||  y  /\  ph )  ->  (
( y  e.  NN  /\  H  e.  NN  /\  y  <_  H )  ->  -.  ( P  -  y
)  <  ( P  /  2 ) ) )
389160, 388biimtrid 152 . . . . . . . . . . . . 13  |-  ( ( -.  2  ||  y  /\  ph )  ->  (
y  e.  ( 1 ... H )  ->  -.  ( P  -  y
)  <  ( P  /  2 ) ) )
3903893impia 1202 . . . . . . . . . . . 12  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  -.  ( P  -  y
)  <  ( P  /  2 ) )
391339, 390eqnbrtrd 4047 . . . . . . . . . . 11  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  -.  ( ( ( P  -  y )  / 
2 )  x.  2 )  <  ( P  /  2 ) )
392391iffalsed 3567 . . . . . . . . . 10  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  if ( ( ( ( P  -  y )  /  2 )  x.  2 )  <  ( P  /  2 ) ,  ( ( ( P  -  y )  / 
2 )  x.  2 ) ,  ( P  -  ( ( ( P  -  y )  /  2 )  x.  2 ) ) )  =  ( P  -  ( ( ( P  -  y )  / 
2 )  x.  2 ) ) )
393339oveq2d 5926 . . . . . . . . . 10  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  ( P  -  ( (
( P  -  y
)  /  2 )  x.  2 ) )  =  ( P  -  ( P  -  y
) ) )
394333, 194anim12i 338 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( 1 ... H
) )  ->  ( P  e.  CC  /\  y  e.  CC ) )
3953943adant1 1017 . . . . . . . . . . 11  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  ( P  e.  CC  /\  y  e.  CC ) )
396 nncan 8238 . . . . . . . . . . 11  |-  ( ( P  e.  CC  /\  y  e.  CC )  ->  ( P  -  ( P  -  y )
)  =  y )
397395, 396syl 14 . . . . . . . . . 10  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  ( P  -  ( P  -  y ) )  =  y )
398392, 393, 3973eqtrrd 2231 . . . . . . . . 9  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  y  =  if ( ( ( ( P  -  y
)  /  2 )  x.  2 )  < 
( P  /  2
) ,  ( ( ( P  -  y
)  /  2 )  x.  2 ) ,  ( P  -  (
( ( P  -  y )  /  2
)  x.  2 ) ) ) )
399326, 332, 398rspcedvd 2870 . . . . . . . 8  |-  ( ( -.  2  ||  y  /\  ph  /\  y  e.  ( 1 ... H
) )  ->  E. x  e.  ( 1 ... H
) y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) ) )
4003993expb 1206 . . . . . . 7  |-  ( ( -.  2  ||  y  /\  ( ph  /\  y  e.  ( 1 ... H
) ) )  ->  E. x  e.  (
1 ... H ) y  =  if ( ( x  x.  2 )  <  ( P  / 
2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2
) ) ) )
401400ancoms 268 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( 1 ... H
) )  /\  -.  2  ||  y )  ->  E. x  e.  (
1 ... H ) y  =  if ( ( x  x.  2 )  <  ( P  / 
2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2
) ) ) )
4029a1i 9 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 1 ... H
) )  ->  2  e.  NN )
403193adantl 277 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 1 ... H
) )  ->  y  e.  ZZ )
404 dvdsdc 11931 . . . . . . . 8  |-  ( ( 2  e.  NN  /\  y  e.  ZZ )  -> DECID  2 
||  y )
405402, 403, 404syl2anc 411 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( 1 ... H
) )  -> DECID  2  ||  y )
406 exmiddc 837 . . . . . . 7  |-  (DECID  2  ||  y  ->  ( 2  ||  y  \/  -.  2  ||  y ) )
407405, 406syl 14 . . . . . 6  |-  ( (
ph  /\  y  e.  ( 1 ... H
) )  ->  (
2  ||  y  \/  -.  2  ||  y ) )
408222, 401, 407mpjaodan 799 . . . . 5  |-  ( (
ph  /\  y  e.  ( 1 ... H
) )  ->  E. x  e.  ( 1 ... H
) y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) ) )
409408ex 115 . . . 4  |-  ( ph  ->  ( y  e.  ( 1 ... H )  ->  E. x  e.  ( 1 ... H ) y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) ) ) )
410159, 409impbid 129 . . 3  |-  ( ph  ->  ( E. x  e.  ( 1 ... H
) y  =  if ( ( x  x.  2 )  <  ( P  /  2 ) ,  ( x  x.  2 ) ,  ( P  -  ( x  x.  2 ) ) )  <-> 
y  e.  ( 1 ... H ) ) )
4113, 410bitrid 192 . 2  |-  ( ph  ->  ( y  e.  ran  R  <-> 
y  e.  ( 1 ... H ) ) )
412411eqrdv 2191 1  |-  ( ph  ->  ran  R  =  ( 1 ... H ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 709  DECID wdc 835    /\ w3a 980    = wceq 1364    e. wcel 2164   E.wrex 2473   _Vcvv 2760    \ cdif 3150   ifcif 3557   {csn 3618   class class class wbr 4029    |-> cmpt 4090   ran crn 4656  (class class class)co 5910   CCcc 7860   RRcr 7861   0cc0 7862   1c1 7863    + caddc 7865    x. cmul 7867    < clt 8044    <_ cle 8045    - cmin 8180   # cap 8590    / cdiv 8681   NNcn 8972   2c2 9023   ZZcz 9307   QQcq 9674   RR+crp 9709   ...cfz 10064    || cdvds 11920   Primecprime 12235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4462  ax-setind 4565  ax-iinf 4616  ax-cnex 7953  ax-resscn 7954  ax-1cn 7955  ax-1re 7956  ax-icn 7957  ax-addcl 7958  ax-addrcl 7959  ax-mulcl 7960  ax-mulrcl 7961  ax-addcom 7962  ax-mulcom 7963  ax-addass 7964  ax-mulass 7965  ax-distr 7966  ax-i2m1 7967  ax-0lt1 7968  ax-1rid 7969  ax-0id 7970  ax-rnegex 7971  ax-precex 7972  ax-cnre 7973  ax-pre-ltirr 7974  ax-pre-ltwlin 7975  ax-pre-lttrn 7976  ax-pre-apti 7977  ax-pre-ltadd 7978  ax-pre-mulgt0 7979  ax-pre-mulext 7980  ax-arch 7981  ax-caucvg 7982
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-xor 1387  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-if 3558  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-id 4322  df-po 4325  df-iso 4326  df-iord 4395  df-on 4397  df-ilim 4398  df-suc 4400  df-iom 4619  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-iota 5207  df-fun 5248  df-fn 5249  df-f 5250  df-f1 5251  df-fo 5252  df-f1o 5253  df-fv 5254  df-riota 5865  df-ov 5913  df-oprab 5914  df-mpo 5915  df-1st 6184  df-2nd 6185  df-recs 6349  df-frec 6435  df-1o 6460  df-2o 6461  df-er 6578  df-en 6786  df-pnf 8046  df-mnf 8047  df-xr 8048  df-ltxr 8049  df-le 8050  df-sub 8182  df-neg 8183  df-reap 8584  df-ap 8591  df-div 8682  df-inn 8973  df-2 9031  df-3 9032  df-4 9033  df-n0 9231  df-z 9308  df-uz 9583  df-q 9675  df-rp 9710  df-ioo 9948  df-fz 10065  df-fl 10329  df-mod 10384  df-seqfrec 10509  df-exp 10600  df-cj 10976  df-re 10977  df-im 10978  df-rsqrt 11132  df-abs 11133  df-dvds 11921  df-prm 12236
This theorem is referenced by:  gausslemma2dlem1f1o  15124
  Copyright terms: Public domain W3C validator