Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sumnnodd Structured version   Unicode version

Theorem sumnnodd 31839
Description: A series indexed by  NN with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
sumnnodd.1  |-  ( ph  ->  F : NN --> CC )
sumnnodd.even0  |-  ( (
ph  /\  k  e.  NN  /\  ( k  / 
2 )  e.  NN )  ->  ( F `  k )  =  0 )
sumnnodd.sc  |-  ( ph  ->  seq 1 (  +  ,  F )  ~~>  B )
Assertion
Ref Expression
sumnnodd  |-  ( ph  ->  (  seq 1 (  +  ,  ( k  e.  NN  |->  ( F `
 ( ( 2  x.  k )  - 
1 ) ) ) )  ~~>  B  /\  sum_ k  e.  NN  ( F `  k )  =  sum_ k  e.  NN  ( F `  ( ( 2  x.  k )  -  1 ) ) ) )
Distinct variable groups:    k, F    ph, k
Allowed substitution hint:    B( k)

Proof of Theorem sumnnodd
Dummy variables  C  j  i  n  m  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1708 . . 3  |-  F/ k
ph
2 nfcv 2619 . . 3  |-  F/_ k  seq 1 (  +  ,  F )
3 nfcv 2619 . . . 4  |-  F/_ k
1
4 nfcv 2619 . . . 4  |-  F/_ k  +
5 nfmpt1 4546 . . . 4  |-  F/_ k
( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) )
63, 4, 5nfseq 12120 . . 3  |-  F/_ k  seq 1 (  +  , 
( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) ) )
7 nfmpt1 4546 . . 3  |-  F/_ k
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) )
8 nnuz 11141 . . 3  |-  NN  =  ( ZZ>= `  1 )
9 1zzd 10916 . . 3  |-  ( ph  ->  1  e.  ZZ )
10 seqex 12112 . . . 4  |-  seq 1
(  +  ,  F
)  e.  _V
1110a1i 11 . . 3  |-  ( ph  ->  seq 1 (  +  ,  F )  e. 
_V )
12 sumnnodd.1 . . . . . 6  |-  ( ph  ->  F : NN --> CC )
1312ffvelrnda 6032 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 k )  e.  CC )
148, 9, 13serf 12138 . . . 4  |-  ( ph  ->  seq 1 (  +  ,  F ) : NN --> CC )
1514ffvelrnda 6032 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq 1 (  +  ,  F ) `  k
)  e.  CC )
16 sumnnodd.sc . . 3  |-  ( ph  ->  seq 1 (  +  ,  F )  ~~>  B )
17 1nn 10567 . . . . . . 7  |-  1  e.  NN
18 oveq2 6304 . . . . . . . . 9  |-  ( k  =  1  ->  (
2  x.  k )  =  ( 2  x.  1 ) )
1918oveq1d 6311 . . . . . . . 8  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  1 )  - 
1 ) )
20 eqid 2457 . . . . . . . 8  |-  ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) )  =  ( k  e.  NN  |->  ( ( 2  x.  k )  - 
1 ) )
21 ovex 6324 . . . . . . . 8  |-  ( ( 2  x.  1 )  -  1 )  e. 
_V
2219, 20, 21fvmpt 5956 . . . . . . 7  |-  ( 1  e.  NN  ->  (
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `  1
)  =  ( ( 2  x.  1 )  -  1 ) )
2317, 22ax-mp 5 . . . . . 6  |-  ( ( k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) ) `  1 )  =  ( ( 2  x.  1 )  - 
1 )
24 2t1e2 10705 . . . . . . 7  |-  ( 2  x.  1 )  =  2
2524oveq1i 6306 . . . . . 6  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
26 2m1e1 10671 . . . . . 6  |-  ( 2  -  1 )  =  1
2723, 25, 263eqtri 2490 . . . . 5  |-  ( ( k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) ) `  1 )  =  1
2827, 17eqeltri 2541 . . . 4  |-  ( ( k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) ) `  1 )  e.  NN
2928a1i 11 . . 3  |-  ( ph  ->  ( ( k  e.  NN  |->  ( ( 2  x.  k )  - 
1 ) ) ` 
1 )  e.  NN )
30 2z 10917 . . . . . . . 8  |-  2  e.  ZZ
3130a1i 11 . . . . . . 7  |-  ( k  e.  NN  ->  2  e.  ZZ )
32 nnz 10907 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
3331, 32zmulcld 10996 . . . . . 6  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  ZZ )
3432peano2zd 10993 . . . . . . . 8  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  ZZ )
3531, 34zmulcld 10996 . . . . . . 7  |-  ( k  e.  NN  ->  (
2  x.  ( k  +  1 ) )  e.  ZZ )
36 1zzd 10916 . . . . . . 7  |-  ( k  e.  NN  ->  1  e.  ZZ )
3735, 36zsubcld 10995 . . . . . 6  |-  ( k  e.  NN  ->  (
( 2  x.  (
k  +  1 ) )  -  1 )  e.  ZZ )
38 2re 10626 . . . . . . . . . 10  |-  2  e.  RR
3938a1i 11 . . . . . . . . 9  |-  ( k  e.  NN  ->  2  e.  RR )
40 nnre 10563 . . . . . . . . 9  |-  ( k  e.  NN  ->  k  e.  RR )
4139, 40remulcld 9641 . . . . . . . 8  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  RR )
4241lep1d 10497 . . . . . . 7  |-  ( k  e.  NN  ->  (
2  x.  k )  <_  ( ( 2  x.  k )  +  1 ) )
43 2cnd 10629 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  2  e.  CC )
44 nncn 10564 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  k  e.  CC )
45 1cnd 9629 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  1  e.  CC )
4643, 44, 45adddid 9637 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
2  x.  ( k  +  1 ) )  =  ( ( 2  x.  k )  +  ( 2  x.  1 ) ) )
4724oveq2i 6307 . . . . . . . . . 10  |-  ( ( 2  x.  k )  +  ( 2  x.  1 ) )  =  ( ( 2  x.  k )  +  2 )
4846, 47syl6eq 2514 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
2  x.  ( k  +  1 ) )  =  ( ( 2  x.  k )  +  2 ) )
4948oveq1d 6311 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( 2  x.  (
k  +  1 ) )  -  1 )  =  ( ( ( 2  x.  k )  +  2 )  - 
1 ) )
5043, 44mulcld 9633 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  CC )
5150, 43, 45addsubassd 9970 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( ( 2  x.  k )  +  2 )  -  1 )  =  ( ( 2  x.  k )  +  ( 2  -  1 ) ) )
5226oveq2i 6307 . . . . . . . . 9  |-  ( ( 2  x.  k )  +  ( 2  -  1 ) )  =  ( ( 2  x.  k )  +  1 )
5352a1i 11 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  +  ( 2  -  1 ) )  =  ( ( 2  x.  k )  +  1 ) )
5449, 51, 533eqtrrd 2503 . . . . . . 7  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  ( k  +  1 ) )  - 
1 ) )
5542, 54breqtrd 4480 . . . . . 6  |-  ( k  e.  NN  ->  (
2  x.  k )  <_  ( ( 2  x.  ( k  +  1 ) )  - 
1 ) )
56 eluz2 11112 . . . . . 6  |-  ( ( ( 2  x.  (
k  +  1 ) )  -  1 )  e.  ( ZZ>= `  (
2  x.  k ) )  <->  ( ( 2  x.  k )  e.  ZZ  /\  ( ( 2  x.  ( k  +  1 ) )  -  1 )  e.  ZZ  /\  ( 2  x.  k )  <_ 
( ( 2  x.  ( k  +  1 ) )  -  1 ) ) )
5733, 37, 55, 56syl3anbrc 1180 . . . . 5  |-  ( k  e.  NN  ->  (
( 2  x.  (
k  +  1 ) )  -  1 )  e.  ( ZZ>= `  (
2  x.  k ) ) )
58 oveq2 6304 . . . . . . . . 9  |-  ( k  =  j  ->  (
2  x.  k )  =  ( 2  x.  j ) )
5958oveq1d 6311 . . . . . . . 8  |-  ( k  =  j  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  j )  - 
1 ) )
6059cbvmptv 4548 . . . . . . 7  |-  ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) )  =  ( j  e.  NN  |->  ( ( 2  x.  j )  - 
1 ) )
6160a1i 11 . . . . . 6  |-  ( k  e.  NN  ->  (
k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) )  =  ( j  e.  NN  |->  ( ( 2  x.  j )  -  1 ) ) )
62 oveq2 6304 . . . . . . . 8  |-  ( j  =  ( k  +  1 )  ->  (
2  x.  j )  =  ( 2  x.  ( k  +  1 ) ) )
6362oveq1d 6311 . . . . . . 7  |-  ( j  =  ( k  +  1 )  ->  (
( 2  x.  j
)  -  1 )  =  ( ( 2  x.  ( k  +  1 ) )  - 
1 ) )
6463adantl 466 . . . . . 6  |-  ( ( k  e.  NN  /\  j  =  ( k  +  1 ) )  ->  ( ( 2  x.  j )  - 
1 )  =  ( ( 2  x.  (
k  +  1 ) )  -  1 ) )
65 peano2nn 10568 . . . . . 6  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
6661, 64, 65, 37fvmptd 5961 . . . . 5  |-  ( k  e.  NN  ->  (
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `  (
k  +  1 ) )  =  ( ( 2  x.  ( k  +  1 ) )  -  1 ) )
6733, 36zsubcld 10995 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  e.  ZZ )
6820fvmpt2 5964 . . . . . . . . 9  |-  ( ( k  e.  NN  /\  ( ( 2  x.  k )  -  1 )  e.  ZZ )  ->  ( ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `
 k )  =  ( ( 2  x.  k )  -  1 ) )
6967, 68mpdan 668 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `  k
)  =  ( ( 2  x.  k )  -  1 ) )
7069oveq1d 6311 . . . . . . 7  |-  ( k  e.  NN  ->  (
( ( k  e.  NN  |->  ( ( 2  x.  k )  - 
1 ) ) `  k )  +  1 )  =  ( ( ( 2  x.  k
)  -  1 )  +  1 ) )
7150, 45npcand 9954 . . . . . . 7  |-  ( k  e.  NN  ->  (
( ( 2  x.  k )  -  1 )  +  1 )  =  ( 2  x.  k ) )
7270, 71eqtrd 2498 . . . . . 6  |-  ( k  e.  NN  ->  (
( ( k  e.  NN  |->  ( ( 2  x.  k )  - 
1 ) ) `  k )  +  1 )  =  ( 2  x.  k ) )
7372fveq2d 5876 . . . . 5  |-  ( k  e.  NN  ->  ( ZZ>=
`  ( ( ( k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) ) `  k )  +  1 ) )  =  ( ZZ>= `  (
2  x.  k ) ) )
7457, 66, 733eltr4d 2560 . . . 4  |-  ( k  e.  NN  ->  (
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `  (
k  +  1 ) )  e.  ( ZZ>= `  ( ( ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `
 k )  +  1 ) ) )
7574adantl 466 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) ) `  ( k  +  1 ) )  e.  ( ZZ>= `  (
( ( k  e.  NN  |->  ( ( 2  x.  k )  - 
1 ) ) `  k )  +  1 ) ) )
76 seqex 12112 . . . 4  |-  seq 1
(  +  ,  ( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) ) )  e.  _V
7776a1i 11 . . 3  |-  ( ph  ->  seq 1 (  +  ,  ( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) ) )  e.  _V )
78 incom 3687 . . . . . . . . . 10  |-  ( ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  i^i  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  =  ( ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)  i^i  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )
79 inss2 3715 . . . . . . . . . . 11  |-  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  C_  { n  e.  NN  | 
( n  /  2
)  e.  NN }
80 ssrin 3719 . . . . . . . . . . 11  |-  ( ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  C_  { n  e.  NN  | 
( n  /  2
)  e.  NN }  ->  ( ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  i^i 
{ n  e.  NN  |  ( n  / 
2 )  e.  NN } )  i^i  (
( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ) 
C_  ( { n  e.  NN  |  ( n  /  2 )  e.  NN }  i^i  (
( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ) )
8179, 80ax-mp 5 . . . . . . . . . 10  |-  ( ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  i^i  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  C_  ( { n  e.  NN  |  ( n  / 
2 )  e.  NN }  i^i  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )
8278, 81eqsstri 3529 . . . . . . . . 9  |-  ( ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  i^i  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  C_  ( { n  e.  NN  |  ( n  / 
2 )  e.  NN }  i^i  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )
83 disjdif 3903 . . . . . . . . 9  |-  ( { n  e.  NN  | 
( n  /  2
)  e.  NN }  i^i  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  =  (/)
8482, 83sseqtri 3531 . . . . . . . 8  |-  ( ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  i^i  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  C_  (/)
85 ss0 3825 . . . . . . . 8  |-  ( ( ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)  i^i  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  i^i 
{ n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  C_  (/) 
->  ( ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  i^i  (
( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )  =  (/) )
8684, 85mp1i 12 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  i^i  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  =  (/) )
87 uncom 3644 . . . . . . . . 9  |-  ( ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  u.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  =  ( ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)  u.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )
88 inundif 3909 . . . . . . . . 9  |-  ( ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  u.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  =  ( 1 ... ( ( 2  x.  k )  -  1 ) )
8987, 88eqtr2i 2487 . . . . . . . 8  |-  ( 1 ... ( ( 2  x.  k )  - 
1 ) )  =  ( ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  u.  (
( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )
9089a1i 11 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1 ... ( ( 2  x.  k )  - 
1 ) )  =  ( ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  u.  (
( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ) )
91 fzfid 12086 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1 ... ( ( 2  x.  k )  - 
1 ) )  e. 
Fin )
9212adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) )  ->  F : NN --> CC )
93 elfznn 11739 . . . . . . . . . 10  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  j  e.  NN )
9493adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) )  ->  j  e.  NN )
9592, 94ffvelrnd 6033 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) )  ->  ( F `  j )  e.  CC )
9695adantlr 714 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) )  ->  ( F `  j )  e.  CC )
9786, 90, 91, 96fsumsplit 13574 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  sum_ j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) ( F `  j )  =  (
sum_ j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ( F `  j )  +  sum_ j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ( F `  j ) ) )
98 simpl 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  ph )
99 ssrab2 3581 . . . . . . . . . . . . . 14  |-  { n  e.  NN  |  ( n  /  2 )  e.  NN }  C_  NN
10079sseli 3495 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  i^i 
{ n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  e.  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )
10199, 100sseldi 3497 . . . . . . . . . . . . 13  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  i^i 
{ n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  e.  NN )
102101adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  j  e.  NN )
103 oveq1 6303 . . . . . . . . . . . . . . . 16  |-  ( k  =  j  ->  (
k  /  2 )  =  ( j  / 
2 ) )
104103eleq1d 2526 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
( k  /  2
)  e.  NN  <->  ( j  /  2 )  e.  NN ) )
105 oveq1 6303 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  (
n  /  2 )  =  ( k  / 
2 ) )
106105eleq1d 2526 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  (
( n  /  2
)  e.  NN  <->  ( k  /  2 )  e.  NN ) )
107106elrab 3257 . . . . . . . . . . . . . . . 16  |-  ( k  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN }  <->  ( k  e.  NN  /\  ( k  /  2 )  e.  NN ) )
108107simprbi 464 . . . . . . . . . . . . . . 15  |-  ( k  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN }  ->  (
k  /  2 )  e.  NN )
109104, 108vtoclga 3173 . . . . . . . . . . . . . 14  |-  ( j  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN }  ->  (
j  /  2 )  e.  NN )
110100, 109syl 16 . . . . . . . . . . . . 13  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  i^i 
{ n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  (
j  /  2 )  e.  NN )
111110adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  (
j  /  2 )  e.  NN )
112 eleq1 2529 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
k  e.  NN  <->  j  e.  NN ) )
113112, 1043anbi23d 1302 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( ph  /\  k  e.  NN  /\  ( k  /  2 )  e.  NN )  <->  ( ph  /\  j  e.  NN  /\  ( j  /  2
)  e.  NN ) ) )
114 fveq2 5872 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  ( F `  k )  =  ( F `  j ) )
115114eqeq1d 2459 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( F `  k
)  =  0  <->  ( F `  j )  =  0 ) )
116113, 115imbi12d 320 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  (
( ( ph  /\  k  e.  NN  /\  (
k  /  2 )  e.  NN )  -> 
( F `  k
)  =  0 )  <-> 
( ( ph  /\  j  e.  NN  /\  (
j  /  2 )  e.  NN )  -> 
( F `  j
)  =  0 ) ) )
117 sumnnodd.even0 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN  /\  ( k  / 
2 )  e.  NN )  ->  ( F `  k )  =  0 )
118116, 117chvarv 2015 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN  /\  ( j  / 
2 )  e.  NN )  ->  ( F `  j )  =  0 )
11998, 102, 111, 118syl3anc 1228 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  ( F `  j )  =  0 )
120119sumeq2dv 13537 . . . . . . . . . 10  |-  ( ph  -> 
sum_ j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ( F `  j )  =  sum_ j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) 0 )
121 fzfid 12086 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... (
( 2  x.  k
)  -  1 ) )  e.  Fin )
122 inss1 3714 . . . . . . . . . . . . . 14  |-  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  C_  ( 1 ... (
( 2  x.  k
)  -  1 ) )
123122a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)  C_  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )
124 ssfi 7759 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  e.  Fin  /\  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)  C_  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  i^i 
{ n  e.  NN  |  ( n  / 
2 )  e.  NN } )  e.  Fin )
125121, 123, 124syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)  e.  Fin )
126125olcd 393 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  i^i 
{ n  e.  NN  |  ( n  / 
2 )  e.  NN } )  C_  ( ZZ>=
`  C )  \/  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)  e.  Fin )
)
127 sumz 13556 . . . . . . . . . . 11  |-  ( ( ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)  C_  ( ZZ>= `  C )  \/  (
( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  e. 
Fin )  ->  sum_ j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) 0  =  0 )
128126, 127syl 16 . . . . . . . . . 10  |-  ( ph  -> 
sum_ j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) 0  =  0 )
129120, 128eqtrd 2498 . . . . . . . . 9  |-  ( ph  -> 
sum_ j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ( F `  j )  =  0 )
130129adantr 465 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  sum_ j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) ( F `  j )  =  0 )
131130oveq2d 6312 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( sum_ j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) ( F `
 j )  + 
sum_ j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ( F `  j ) )  =  ( sum_ j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) ( F `
 j )  +  0 ) )
132 fzfi 12085 . . . . . . . . . . . 12  |-  ( 1 ... ( ( 2  x.  k )  - 
1 ) )  e. 
Fin
133 difss 3627 . . . . . . . . . . . 12  |-  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  C_  ( 1 ... (
( 2  x.  k
)  -  1 ) )
134 ssfi 7759 . . . . . . . . . . . 12  |-  ( ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  e.  Fin  /\  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)  C_  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  e.  Fin )
135132, 133, 134mp2an 672 . . . . . . . . . . 11  |-  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  e. 
Fin
136135a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  e. 
Fin )
137133sseli 3495 . . . . . . . . . . . 12  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) )
138137, 95sylan2 474 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  ( F `  j )  e.  CC )
139138adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  ( F `  j )  e.  CC )
140136, 139fsumcl 13567 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  sum_ j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) ( F `  j )  e.  CC )
141140addid1d 9797 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  ( sum_ j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) ( F `
 j )  +  0 )  =  sum_ j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) ( F `
 j ) )
142 fveq2 5872 . . . . . . . . 9  |-  ( j  =  i  ->  ( F `  j )  =  ( F `  i ) )
143142cbvsumv 13530 . . . . . . . 8  |-  sum_ j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) ( F `  j )  =  sum_ i  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) ( F `
 i )
144141, 143syl6eq 2514 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( sum_ j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) ( F `
 j )  +  0 )  =  sum_ i  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) ( F `
 i ) )
145131, 144eqtrd 2498 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( sum_ j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) ( F `
 j )  + 
sum_ j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ( F `  j ) )  =  sum_ i  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) ( F `  i ) )
146 fveq2 5872 . . . . . . 7  |-  ( i  =  ( ( 2  x.  j )  - 
1 )  ->  ( F `  i )  =  ( F `  ( ( 2  x.  j )  -  1 ) ) )
147 fzfid 12086 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1 ... k )  e. 
Fin )
148 1zzd 10916 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  1  e.  ZZ )
14967adantr 465 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( ( 2  x.  k )  - 
1 )  e.  ZZ )
15030a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... k )  ->  2  e.  ZZ )
151 elfzelz 11713 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... k )  ->  i  e.  ZZ )
152150, 151zmulcld 10996 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... k )  ->  (
2  x.  i )  e.  ZZ )
153 1zzd 10916 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... k )  ->  1  e.  ZZ )
154152, 153zsubcld 10995 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... k )  ->  (
( 2  x.  i
)  -  1 )  e.  ZZ )
155154adantl 466 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( ( 2  x.  i )  - 
1 )  e.  ZZ )
156148, 149, 1553jca 1176 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( 1  e.  ZZ  /\  ( ( 2  x.  k )  -  1 )  e.  ZZ  /\  ( ( 2  x.  i )  -  1 )  e.  ZZ ) )
15725, 26eqtr2i 2487 . . . . . . . . . . . . . . . 16  |-  1  =  ( ( 2  x.  1 )  - 
1 )
158 1re 9612 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  RR
15938, 158remulcli 9627 . . . . . . . . . . . . . . . . . 18  |-  ( 2  x.  1 )  e.  RR
160159a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... k )  ->  (
2  x.  1 )  e.  RR )
161152zred 10990 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... k )  ->  (
2  x.  i )  e.  RR )
162 1red 9628 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... k )  ->  1  e.  RR )
163151zred 10990 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  i  e.  RR )
16438a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  2  e.  RR )
165 0le2 10647 . . . . . . . . . . . . . . . . . . 19  |-  0  <_  2
166165a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  0  <_  2 )
167 elfzle1 11714 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  1  <_  i )
168162, 163, 164, 166, 167lemul2ad 10506 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... k )  ->  (
2  x.  1 )  <_  ( 2  x.  i ) )
169160, 161, 162, 168lesub1dd 10189 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... k )  ->  (
( 2  x.  1 )  -  1 )  <_  ( ( 2  x.  i )  - 
1 ) )
170157, 169syl5eqbr 4489 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... k )  ->  1  <_  ( ( 2  x.  i )  -  1 ) )
171170adantl 466 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  1  <_  (
( 2  x.  i
)  -  1 ) )
172161adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( 2  x.  i )  e.  RR )
17341adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( 2  x.  k )  e.  RR )
174 1red 9628 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  1  e.  RR )
175163adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  i  e.  RR )
17640adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  k  e.  RR )
17738a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  2  e.  RR )
178165a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  0  <_  2
)
179 elfzle2 11715 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... k )  ->  i  <_  k )
180179adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  i  <_  k
)
181175, 176, 177, 178, 180lemul2ad 10506 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( 2  x.  i )  <_  (
2  x.  k ) )
182172, 173, 174, 181lesub1dd 10189 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( ( 2  x.  i )  - 
1 )  <_  (
( 2  x.  k
)  -  1 ) )
183171, 182jca 532 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( 1  <_ 
( ( 2  x.  i )  -  1 )  /\  ( ( 2  x.  i )  -  1 )  <_ 
( ( 2  x.  k )  -  1 ) ) )
184 elfz2 11704 . . . . . . . . . . . . 13  |-  ( ( ( 2  x.  i
)  -  1 )  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  <->  ( (
1  e.  ZZ  /\  ( ( 2  x.  k )  -  1 )  e.  ZZ  /\  ( ( 2  x.  i )  -  1 )  e.  ZZ )  /\  ( 1  <_ 
( ( 2  x.  i )  -  1 )  /\  ( ( 2  x.  i )  -  1 )  <_ 
( ( 2  x.  k )  -  1 ) ) ) )
185156, 183, 184sylanbrc 664 . . . . . . . . . . . 12  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( ( 2  x.  i )  - 
1 )  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) ) )
186152zcnd 10991 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  (
2  x.  i )  e.  CC )
187 1cnd 9629 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  1  e.  CC )
188 2cnd 10629 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  2  e.  CC )
189 2ne0 10649 . . . . . . . . . . . . . . . . . . 19  |-  2  =/=  0
190189a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  2  =/=  0 )
191186, 187, 188, 190divsubdird 10380 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... k )  ->  (
( ( 2  x.  i )  -  1 )  /  2 )  =  ( ( ( 2  x.  i )  /  2 )  -  ( 1  /  2
) ) )
192151zcnd 10991 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  i  e.  CC )
193192, 188, 190divcan3d 10346 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  (
( 2  x.  i
)  /  2 )  =  i )
194193oveq1d 6311 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... k )  ->  (
( ( 2  x.  i )  /  2
)  -  ( 1  /  2 ) )  =  ( i  -  ( 1  /  2
) ) )
195191, 194eqtrd 2498 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... k )  ->  (
( ( 2  x.  i )  -  1 )  /  2 )  =  ( i  -  ( 1  /  2
) ) )
196151, 153zsubcld 10995 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  (
i  -  1 )  e.  ZZ )
197164, 190rereccld 10392 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  (
1  /  2 )  e.  RR )
198 halflt1 10778 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  2 )  <  1
199198a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  (
1  /  2 )  <  1 )
200197, 162, 163, 199ltsub2dd 10186 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  (
i  -  1 )  <  ( i  -  ( 1  /  2
) ) )
201 2rp 11250 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR+
202 rpreccl 11268 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  e.  RR+  ->  ( 1  /  2 )  e.  RR+ )
203201, 202mp1i 12 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  (
1  /  2 )  e.  RR+ )
204163, 203ltsubrpd 11309 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  (
i  -  ( 1  /  2 ) )  <  i )
205192, 187npcand 9954 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  (
( i  -  1 )  +  1 )  =  i )
206204, 205breqtrrd 4482 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  (
i  -  ( 1  /  2 ) )  <  ( ( i  -  1 )  +  1 ) )
207 btwnnz 10960 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( i  -  1 )  e.  ZZ  /\  ( i  -  1 )  <  ( i  -  ( 1  / 
2 ) )  /\  ( i  -  (
1  /  2 ) )  <  ( ( i  -  1 )  +  1 ) )  ->  -.  ( i  -  ( 1  / 
2 ) )  e.  ZZ )
208196, 200, 206, 207syl3anc 1228 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... k )  ->  -.  ( i  -  (
1  /  2 ) )  e.  ZZ )
209 nnz 10907 . . . . . . . . . . . . . . . . 17  |-  ( ( i  -  ( 1  /  2 ) )  e.  NN  ->  (
i  -  ( 1  /  2 ) )  e.  ZZ )
210208, 209nsyl 121 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... k )  ->  -.  ( i  -  (
1  /  2 ) )  e.  NN )
211195, 210eqneltrd 2566 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... k )  ->  -.  ( ( ( 2  x.  i )  - 
1 )  /  2
)  e.  NN )
212211intnand 916 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 1 ... k )  ->  -.  ( ( ( 2  x.  i )  - 
1 )  e.  NN  /\  ( ( ( 2  x.  i )  - 
1 )  /  2
)  e.  NN ) )
213 oveq1 6303 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( ( 2  x.  i )  - 
1 )  ->  (
n  /  2 )  =  ( ( ( 2  x.  i )  -  1 )  / 
2 ) )
214213eleq1d 2526 . . . . . . . . . . . . . . 15  |-  ( n  =  ( ( 2  x.  i )  - 
1 )  ->  (
( n  /  2
)  e.  NN  <->  ( (
( 2  x.  i
)  -  1 )  /  2 )  e.  NN ) )
215214elrab 3257 . . . . . . . . . . . . . 14  |-  ( ( ( 2  x.  i
)  -  1 )  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN }  <->  ( (
( 2  x.  i
)  -  1 )  e.  NN  /\  (
( ( 2  x.  i )  -  1 )  /  2 )  e.  NN ) )
216212, 215sylnibr 305 . . . . . . . . . . . . 13  |-  ( i  e.  ( 1 ... k )  ->  -.  ( ( 2  x.  i )  -  1 )  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN } )
217216adantl 466 . . . . . . . . . . . 12  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  -.  ( (
2  x.  i )  -  1 )  e. 
{ n  e.  NN  |  ( n  / 
2 )  e.  NN } )
218185, 217eldifd 3482 . . . . . . . . . . 11  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( ( 2  x.  i )  - 
1 )  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )
219 eqid 2457 . . . . . . . . . . 11  |-  ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) )  =  ( i  e.  ( 1 ... k
)  |->  ( ( 2  x.  i )  - 
1 ) )
220218, 219fmptd 6056 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) : ( 1 ... k ) --> ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )
221 eqidd 2458 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( 1 ... k )  ->  (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) )  =  ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) )
222 oveq2 6304 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  x  ->  (
2  x.  i )  =  ( 2  x.  x ) )
223222oveq1d 6311 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  x  ->  (
( 2  x.  i
)  -  1 )  =  ( ( 2  x.  x )  - 
1 ) )
224223adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ( 1 ... k )  /\  i  =  x )  ->  ( ( 2  x.  i )  -  1 )  =  ( ( 2  x.  x )  -  1 ) )
225 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( 1 ... k )  ->  x  e.  ( 1 ... k
) )
226 ovex 6324 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2  x.  x )  -  1 )  e. 
_V
227226a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( 1 ... k )  ->  (
( 2  x.  x
)  -  1 )  e.  _V )
228221, 224, 225, 227fvmptd 5961 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 1 ... k )  ->  (
( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  x
)  =  ( ( 2  x.  x )  -  1 ) )
229228eqcomd 2465 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 1 ... k )  ->  (
( 2  x.  x
)  -  1 )  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 x ) )
230229ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) `  x )  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 y ) )  ->  ( ( 2  x.  x )  - 
1 )  =  ( ( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  x
) )
231 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) `  x )  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 y ) )  ->  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 x )  =  ( ( i  e.  ( 1 ... k
)  |->  ( ( 2  x.  i )  - 
1 ) ) `  y ) )
232 eqidd 2458 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 ... k )  ->  (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) )  =  ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) )
233 oveq2 6304 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  y  ->  (
2  x.  i )  =  ( 2  x.  y ) )
234233oveq1d 6311 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  y  ->  (
( 2  x.  i
)  -  1 )  =  ( ( 2  x.  y )  - 
1 ) )
235234adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  ( 1 ... k )  /\  i  =  y )  ->  ( ( 2  x.  i )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )
236 id 22 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 ... k )  ->  y  e.  ( 1 ... k
) )
237 ovex 6324 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  x.  y )  -  1 )  e. 
_V
238237a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 ... k )  ->  (
( 2  x.  y
)  -  1 )  e.  _V )
239232, 235, 236, 238fvmptd 5961 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 1 ... k )  ->  (
( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  y
)  =  ( ( 2  x.  y )  -  1 ) )
240239ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) `  x )  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 y ) )  ->  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 y )  =  ( ( 2  x.  y )  -  1 ) )
241230, 231, 2403eqtrd 2502 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) `  x )  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 y ) )  ->  ( ( 2  x.  x )  - 
1 )  =  ( ( 2  x.  y
)  -  1 ) )
242 2cnd 10629 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( 1 ... k )  ->  2  e.  CC )
243 elfzelz 11713 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( 1 ... k )  ->  x  e.  ZZ )
244243zcnd 10991 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( 1 ... k )  ->  x  e.  CC )
245242, 244mulcld 9633 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 1 ... k )  ->  (
2  x.  x )  e.  CC )
246245ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  (
2  x.  x )  e.  CC )
247 2cnd 10629 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 ... k )  ->  2  e.  CC )
248 elfzelz 11713 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 ... k )  ->  y  e.  ZZ )
249248zcnd 10991 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 ... k )  ->  y  e.  CC )
250247, 249mulcld 9633 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 ... k )  ->  (
2  x.  y )  e.  CC )
251250ad2antlr 726 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  (
2  x.  y )  e.  CC )
252 1cnd 9629 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  1  e.  CC )
253 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  (
( 2  x.  x
)  -  1 )  =  ( ( 2  x.  y )  - 
1 ) )
254246, 251, 252, 253subcan2d 9992 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  (
2  x.  x )  =  ( 2  x.  y ) )
255244ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  x  e.  CC )
256249ad2antlr 726 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  y  e.  CC )
257 2cnd 10629 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  2  e.  CC )
258189a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  2  =/=  0 )
259 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  (
2  x.  x )  =  ( 2  x.  y ) )
260255, 256, 257, 258, 259mulcanad 10205 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  x  =  y )
261254, 260syldan 470 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  x  =  y )
262241, 261syldan 470 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) `  x )  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 y ) )  ->  x  =  y )
263262adantll 713 . . . . . . . . . . . 12  |-  ( ( ( k  e.  NN  /\  ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) ) )  /\  (
( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  x
)  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) `  y ) )  ->  x  =  y )
264263ex 434 . . . . . . . . . . 11  |-  ( ( k  e.  NN  /\  ( x  e.  (
1 ... k )  /\  y  e.  ( 1 ... k ) ) )  ->  ( (
( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  x
)  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) `  y )  ->  x  =  y ) )
265264ralrimivva 2878 . . . . . . . . . 10  |-  ( k  e.  NN  ->  A. x  e.  ( 1 ... k
) A. y  e.  ( 1 ... k
) ( ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) `  x )  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 y )  ->  x  =  y )
)
266 dff13 6167 . . . . . . . . . 10  |-  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) : ( 1 ... k ) -1-1-> ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  <->  ( (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) : ( 1 ... k ) --> ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  A. x  e.  ( 1 ... k ) A. y  e.  ( 1 ... k ) ( ( ( i  e.  ( 1 ... k
)  |->  ( ( 2  x.  i )  - 
1 ) ) `  x )  =  ( ( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  y
)  ->  x  =  y ) ) )
267220, 265, 266sylanbrc 664 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) : ( 1 ... k ) -1-1-> ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )
268 1zzd 10916 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
1  e.  ZZ )
26932adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
k  e.  ZZ )
270 fzssz 31669 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1 ... ( ( 2  x.  k )  - 
1 ) )  C_  ZZ
271270, 137sseldi 3497 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  e.  ZZ )
272 zeo 10969 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ZZ  ->  (
( j  /  2
)  e.  ZZ  \/  ( ( j  +  1 )  /  2
)  e.  ZZ ) )
273271, 272syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  (
( j  /  2
)  e.  ZZ  \/  ( ( j  +  1 )  /  2
)  e.  ZZ ) )
274273adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
( ( j  / 
2 )  e.  ZZ  \/  ( ( j  +  1 )  /  2
)  e.  ZZ ) )
275 eldifn 3623 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  -.  j  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN } )
276137, 93syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  e.  NN )
277276adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  j  e.  NN )
278 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  ( j  / 
2 )  e.  ZZ )
279277nnred 10571 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  j  e.  RR )
28038a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  2  e.  RR )
281277nngt0d 10600 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  0  <  j
)
282 2pos 10648 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  <  2
283282a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  0  <  2
)
284279, 280, 281, 283divgt0d 10501 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  0  <  (
j  /  2 ) )
285 elnnz 10895 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( j  /  2 )  e.  NN  <->  ( (
j  /  2 )  e.  ZZ  /\  0  <  ( j  /  2
) ) )
286278, 284, 285sylanbrc 664 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  ( j  / 
2 )  e.  NN )
287 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  j  ->  (
n  /  2 )  =  ( j  / 
2 ) )
288287eleq1d 2526 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  j  ->  (
( n  /  2
)  e.  NN  <->  ( j  /  2 )  e.  NN ) )
289288elrab 3257 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN }  <->  ( j  e.  NN  /\  ( j  /  2 )  e.  NN ) )
290277, 286, 289sylanbrc 664 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  j  e.  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)
291275, 290mtand 659 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  -.  ( j  /  2
)  e.  ZZ )
292291adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  ->  -.  ( j  /  2
)  e.  ZZ )
293 pm2.53 373 . . . . . . . . . . . . . . . . 17  |-  ( ( ( j  /  2
)  e.  ZZ  \/  ( ( j  +  1 )  /  2
)  e.  ZZ )  ->  ( -.  (
j  /  2 )  e.  ZZ  ->  (
( j  +  1 )  /  2 )  e.  ZZ ) )
294274, 292, 293sylc 60 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
( ( j  +  1 )  /  2
)  e.  ZZ )
295268, 269, 2943jca 1176 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
( 1  e.  ZZ  /\  k  e.  ZZ  /\  ( ( j  +  1 )  /  2
)  e.  ZZ ) )
296 1p1e2 10670 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  +  1 )  =  2
297296oveq1i 6306 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  +  1 )  /  2 )  =  ( 2  /  2
)
298 2div2e1 10679 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  /  2 )  =  1
299297, 298eqtr2i 2487 . . . . . . . . . . . . . . . . . 18  |-  1  =  ( ( 1  +  1 )  / 
2 )
300 1red 9628 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  1  e.  RR )
301300, 300readdcld 9640 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
1  +  1 )  e.  RR )
30293nnred 10571 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  j  e.  RR )
303302, 300readdcld 9640 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
j  +  1 )  e.  RR )
304201a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  2  e.  RR+ )
305 elfzle1 11714 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  1  <_  j )
306300, 302, 300, 305leadd1dd 10187 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
1  +  1 )  <_  ( j  +  1 ) )
307301, 303, 304, 306lediv1dd 11335 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
( 1  +  1 )  /  2 )  <_  ( ( j  +  1 )  / 
2 ) )
308299, 307syl5eqbr 4489 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  1  <_  ( ( j  +  1 )  /  2
) )
309137, 308syl 16 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  1  <_  ( ( j  +  1 )  /  2
) )
310309adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
1  <_  ( (
j  +  1 )  /  2 ) )
311 elfzel2 11711 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
( 2  x.  k
)  -  1 )  e.  ZZ )
312311zred 10990 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
( 2  x.  k
)  -  1 )  e.  RR )
313312, 300readdcld 9640 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
( ( 2  x.  k )  -  1 )  +  1 )  e.  RR )
314 elfzle2 11715 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  j  <_  ( ( 2  x.  k )  -  1 ) )
315302, 312, 300, 314leadd1dd 10187 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
j  +  1 )  <_  ( ( ( 2  x.  k )  -  1 )  +  1 ) )
316303, 313, 304, 315lediv1dd 11335 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
( j  +  1 )  /  2 )  <_  ( ( ( ( 2  x.  k
)  -  1 )  +  1 )  / 
2 ) )
317316adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( j  +  1 )  / 
2 )  <_  (
( ( ( 2  x.  k )  - 
1 )  +  1 )  /  2 ) )
31850adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( 2  x.  k )  e.  CC )
319 1cnd 9629 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  1  e.  CC )
320318, 319npcand 9954 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( ( 2  x.  k )  -  1 )  +  1 )  =  ( 2  x.  k ) )
321320oveq1d 6311 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( ( ( 2  x.  k
)  -  1 )  +  1 )  / 
2 )  =  ( ( 2  x.  k
)  /  2 ) )
322189a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN  ->  2  =/=  0 )
32344, 43, 322divcan3d 10346 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  /  2 )  =  k )
324323adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( 2  x.  k )  / 
2 )  =  k )
325321, 324eqtrd 2498 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( ( ( 2  x.  k
)  -  1 )  +  1 )  / 
2 )  =  k )
326317, 325breqtrd 4480 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( j  +  1 )  / 
2 )  <_  k
)
327137, 326sylan2 474 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
( ( j  +  1 )  /  2
)  <_  k )
328295, 310, 327jca32 535 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
( ( 1  e.  ZZ  /\  k  e.  ZZ  /\  ( ( j  +  1 )  /  2 )  e.  ZZ )  /\  (
1  <_  ( (
j  +  1 )  /  2 )  /\  ( ( j  +  1 )  /  2
)  <_  k )
) )
329 elfz2 11704 . . . . . . . . . . . . . 14  |-  ( ( ( j  +  1 )  /  2 )  e.  ( 1 ... k )  <->  ( (
1  e.  ZZ  /\  k  e.  ZZ  /\  (
( j  +  1 )  /  2 )  e.  ZZ )  /\  ( 1  <_  (
( j  +  1 )  /  2 )  /\  ( ( j  +  1 )  / 
2 )  <_  k
) ) )
330328, 329sylibr 212 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
( ( j  +  1 )  /  2
)  e.  ( 1 ... k ) )
331276nncnd 10572 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  e.  CC )
332 peano2cn 9769 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  CC  ->  (
j  +  1 )  e.  CC )
333 2cnd 10629 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  CC  ->  2  e.  CC )
334189a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  CC  ->  2  =/=  0 )
335332, 333, 334divcan2d 10343 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  CC  ->  (
2  x.  ( ( j  +  1 )  /  2 ) )  =  ( j  +  1 ) )
336335oveq1d 6311 . . . . . . . . . . . . . . . 16  |-  ( j  e.  CC  ->  (
( 2  x.  (
( j  +  1 )  /  2 ) )  -  1 )  =  ( ( j  +  1 )  - 
1 ) )
337 pncan1 10004 . . . . . . . . . . . . . . . 16  |-  ( j  e.  CC  ->  (
( j  +  1 )  -  1 )  =  j )
338336, 337eqtr2d 2499 . . . . . . . . . . . . . . 15  |-  ( j  e.  CC  ->  j  =  ( ( 2  x.  ( ( j  +  1 )  / 
2 ) )  - 
1 ) )
339331, 338syl 16 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  =  ( ( 2  x.  ( ( j  +  1 )  / 
2 ) )  - 
1 ) )
340339adantl 466 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
j  =  ( ( 2  x.  ( ( j  +  1 )  /  2 ) )  -  1 ) )
341 oveq2 6304 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( ( j  +  1 )  / 
2 )  ->  (
2  x.  m )  =  ( 2  x.  ( ( j  +  1 )  /  2
) ) )
342341oveq1d 6311 . . . . . . . . . . . . . . 15  |-  ( m  =  ( ( j  +  1 )  / 
2 )  ->  (
( 2  x.  m
)  -  1 )  =  ( ( 2  x.  ( ( j  +  1 )  / 
2 ) )  - 
1 ) )
343342eqeq2d 2471 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( j  +  1 )  / 
2 )  ->  (
j  =  ( ( 2  x.  m )  -  1 )  <->  j  =  ( ( 2  x.  ( ( j  +  1 )  /  2
) )  -  1 ) ) )
344343rspcev 3210 . . . . . . . . . . . . 13  |-  ( ( ( ( j  +  1 )  /  2
)  e.  ( 1 ... k )  /\  j  =  ( (
2  x.  ( ( j  +  1 )  /  2 ) )  -  1 ) )  ->  E. m  e.  ( 1 ... k ) j  =  ( ( 2  x.  m )  -  1 ) )
345330, 340, 344syl2anc 661 . . . . . . . . . . . 12  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  ->  E. m  e.  (
1 ... k ) j  =  ( ( 2  x.  m )  - 
1 ) )
346 eqidd 2458 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  ( 1 ... k )  /\  j  =  ( (
2  x.  m )  -  1 ) )  ->  ( i  e.  ( 1 ... k
)  |->  ( ( 2  x.  i )  - 
1 ) )  =  ( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) )
347 oveq2 6304 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  m  ->  (
2  x.  i )  =  ( 2  x.  m ) )
348347oveq1d 6311 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  m  ->  (
( 2  x.  i
)  -  1 )  =  ( ( 2  x.  m )  - 
1 ) )
349348adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  ( 1 ... k )  /\  j  =  ( ( 2  x.  m
)  -  1 ) )  /\  i  =  m )  ->  (
( 2  x.  i
)  -  1 )  =  ( ( 2  x.  m )  - 
1 ) )
350 simpl 457 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  ( 1 ... k )  /\  j  =  ( (
2  x.  m )  -  1 ) )  ->  m  e.  ( 1 ... k ) )
351 ovex 6324 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  x.  m )  -  1 )  e. 
_V
352351a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  ( 1 ... k )  /\  j  =  ( (
2  x.  m )  -  1 ) )  ->  ( ( 2  x.  m )  - 
1 )  e.  _V )
353346, 349, 350, 352fvmptd 5961 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  ( 1 ... k )  /\  j  =  ( (
2  x.  m )  -  1 ) )  ->  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 m )  =  ( ( 2  x.  m )  -  1 ) )
354 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  ( ( 2  x.  m )  - 
1 )  ->  j  =  ( ( 2  x.  m )  - 
1 ) )
355354eqcomd 2465 . . . . . . . . . . . . . . . . 17  |-  ( j  =  ( ( 2  x.  m )  - 
1 )  ->  (
( 2  x.  m
)  -  1 )  =  j )
356355adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  ( 1 ... k )  /\  j  =  ( (
2  x.  m )  -  1 ) )  ->  ( ( 2  x.  m )  - 
1 )  =  j )
357353, 356eqtr2d 2499 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  ( 1 ... k )  /\  j  =  ( (
2  x.  m )  -  1 ) )  ->  j  =  ( ( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  m
) )
358357ex 434 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 ... k )  ->  (
j  =  ( ( 2  x.  m )  -  1 )  -> 
j  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) `  m ) ) )
359358adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( k  e.  NN  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )  /\  m  e.  ( 1 ... k ) )  ->  ( j  =  ( ( 2  x.  m )  - 
1 )  ->  j  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 m ) ) )
360359reximdva 2932 . . . . . . . . . . . 12  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
( E. m  e.  ( 1 ... k
) j  =  ( ( 2  x.  m
)  -  1 )  ->  E. m  e.  ( 1 ... k ) j  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) `  m ) ) )
361345, 360mpd 15 . . . . . . . . . . 11  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  ->  E. m  e.  (
1 ... k ) j  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 m ) )
362361ralrimiva 2871 . . . . . . . . . 10  |-  ( k  e.  NN  ->  A. j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) E. m  e.  ( 1 ... k
) j  =  ( ( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  m
) )
363 dffo3 6047 . . . . . . . . . 10  |-  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) : ( 1 ... k ) -onto-> ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  <->  ( (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) : ( 1 ... k ) --> ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  A. j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) E. m  e.  ( 1 ... k ) j  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 m ) ) )
364220, 362, 363sylanbrc 664 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) : ( 1 ... k ) -onto-> ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )
365 df-f1o 5601 . . . . . . . . 9  |-  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) : ( 1 ... k ) -1-1-onto-> ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  <->  ( (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) : ( 1 ... k ) -1-1-> ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) : ( 1 ... k )
-onto-> ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) ) )
366267, 364, 365sylanbrc 664 . . . . . . . 8  |-  ( k  e.  NN  ->  (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) ) : ( 1 ... k ) -1-1-onto-> ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )
367366adantl 466 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) : ( 1 ... k ) -1-1-onto-> ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )
368 eqidd 2458 . . . . . . . . 9  |-  ( j  e.  ( 1 ... k )  ->  (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) )  =  ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) )
369 oveq2 6304 . . . . . . . . . . 11  |-  ( i  =  j  ->  (
2  x.  i )  =  ( 2  x.  j ) )
370369oveq1d 6311 . . . . . . . . . 10  |-  ( i  =  j  ->  (
( 2  x.  i
)  -  1 )  =  ( ( 2  x.  j )  - 
1 ) )
371370adantl 466 . . . . . . . . 9  |-  ( ( j  e.  ( 1 ... k )  /\  i  =  j )  ->  ( ( 2  x.  i )  -  1 )  =  ( ( 2  x.  j )  -  1 ) )
372 id 22 . . . . . . . . 9  |-  ( j  e.  ( 1 ... k )  ->  j  e.  ( 1 ... k
) )
373 ovex 6324 . . . . . . . . . 10  |-  ( ( 2  x.  j )  -  1 )  e. 
_V
374373a1i 11 . . . . . . . . 9  |-  ( j  e.  ( 1 ... k )  ->  (
( 2  x.  j
)  -  1 )  e.  _V )
375368, 371, 372, 374fvmptd 5961 . . . . . . . 8  |-  ( j  e.  ( 1 ... k )  ->  (
( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  j
)  =  ( ( 2  x.  j )  -  1 ) )
376375adantl 466 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 1 ... k
) )  ->  (
( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  j
)  =  ( ( 2  x.  j )  -  1 ) )
377 eleq1 2529 . . . . . . . . . 10  |-  ( j  =  i  ->  (
j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  <->  i  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) ) )
378377anbi2d 703 . . . . . . . . 9  |-  ( j  =  i  ->  (
( ( ph  /\  k  e.  NN )  /\  j  e.  (
( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )  <-> 
( ( ph  /\  k  e.  NN )  /\  i  e.  (
( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ) ) )
379142eleq1d 2526 . . . . . . . . 9  |-  ( j  =  i  ->  (
( F `  j
)  e.  CC  <->  ( F `  i )  e.  CC ) )
380378, 379imbi12d 320 . . . . . . . 8  |-  ( j  =  i  ->  (
( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )  ->  ( F `  j )  e.  CC ) 
<->  ( ( ( ph  /\  k  e.  NN )  /\  i  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )  ->  ( F `  i )  e.  CC ) ) )
381380, 139chvarv 2015 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  i  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  ( F `  i )  e.  CC )
382146, 147, 367, 376, 381fsumf1o 13557 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  sum_ i  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) ( F `  i )  =  sum_ j  e.  ( 1 ... k ) ( F `  ( ( 2  x.  j )  -  1 ) ) )
38397, 145, 3823eqtrrd 2503 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  sum_ j  e.  ( 1 ... k
) ( F `  ( ( 2  x.  j )  -  1 ) )  =  sum_ j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) ( F `  j ) )
384 ovex 6324 . . . . . . . . . 10  |-  ( ( 2  x.  k )  -  1 )  e. 
_V
38520fvmpt2 5964 . . . . . . . . . 10  |-  ( ( k  e.  NN  /\  ( ( 2  x.  k )  -  1 )  e.  _V )  ->  ( ( k  e.  NN  |->  ( ( 2  x.  k )  - 
1 ) ) `  k )  =  ( ( 2  x.  k
)  -  1 ) )
386384, 385mpan2 671 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `  k
)  =  ( ( 2  x.  k )  -  1 ) )
387386oveq2d 6312 . . . . . . . 8  |-  ( k  e.  NN  ->  (
1 ... ( ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `
 k ) )  =  ( 1 ... ( ( 2  x.  k )  -  1 ) ) )
388387eqcomd 2465 . . . . . . 7  |-  ( k  e.  NN  ->  (
1 ... ( ( 2  x.  k )  - 
1 ) )  =  ( 1 ... (
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `  k
) ) )
389388sumeq1d 13535 . . . . . 6  |-  ( k  e.  NN  ->  sum_ j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) ( F `  j )  =  sum_ j  e.  ( 1 ... ( ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `
 k ) ) ( F `  j
) )
390389adantl 466 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  sum_ j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) ( F `  j )  =  sum_ j  e.  ( 1 ... ( ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `
 k ) ) ( F `  j
) )
391383, 390eqtrd 2498 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  sum_ j  e.  ( 1 ... k
) ( F `  ( ( 2  x.  j )  -  1 ) )  =  sum_ j  e.  ( 1 ... ( ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `
 k ) ) ( F `  j
) )
392 elfznn 11739 . . . . . . 7  |-  ( j  e.  ( 1 ... k )  ->  j  e.  NN )
393392adantl 466 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 1 ... k
) )  ->  j  e.  NN )
39412adantr 465 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 1 ... k
) )  ->  F : NN --> CC )
39530a1i 11 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... k )  ->  2  e.  ZZ )
396 elfzelz 11713 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... k )  ->  j  e.  ZZ )
397395, 396zmulcld 10996 . . . . . . . . . . 11  |-  ( j  e.  ( 1 ... k )  ->  (
2  x.  j )  e.  ZZ )
398 1zzd 10916 . . . . . . . . . . 11  |-  ( j  e.  ( 1 ... k )  ->  1  e.  ZZ )
399397, 398zsubcld 10995 . . . . . . . . . 10  |-  ( j  e.  ( 1 ... k )  ->  (
( 2  x.  j
)  -  1 )  e.  ZZ )
400 0red 9614 . . . . . . . . . . 11  |-  ( j  e.  ( 1 ... k )  ->  0  e.  RR )
40138a1i 11 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... k )  ->  2  e.  RR )
40224, 401syl5eqel 2549 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... k )  ->  (
2  x.  1 )  e.  RR )
403 1red 9628 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... k )  ->  1  e.  RR )
404402, 403resubcld 10008 . . . . . . . . . . 11  |-  ( j  e.  ( 1 ... k )  ->  (
( 2  x.  1 )  -  1 )  e.  RR )
405399zred 10990 . . . . . . . . . . 11  |-  ( j  e.  ( 1 ... k )  ->  (
( 2  x.  j
)  -  1 )  e.  RR )
406 0lt1 10096 . . . . . . . . . . . 12  |-  0  <  1
407157a1i 11 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... k )  ->  1  =  ( ( 2  x.  1 )  - 
1 ) )
408406, 407syl5breq 4491 . . . . . . . . . . 11  |-  ( j  e.  ( 1 ... k )  ->  0  <  ( ( 2  x.  1 )  -  1 ) )
409397zred 10990 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... k )  ->  (
2  x.  j )  e.  RR )
410392nnred 10571 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... k )  ->  j  e.  RR )
411165a1i 11 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... k )  ->  0  <_  2 )
412 elfzle1 11714 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... k )  ->  1  <_  j )
413403, 410, 401, 411, 412lemul2ad 10506 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... k )  ->  (
2  x.  1 )  <_  ( 2  x.  j ) )
414402, 409, 403, 413lesub1dd 10189 . . . . . . . . . . 11  |-  ( j  e.  ( 1 ... k )  ->  (
( 2  x.  1 )  -  1 )  <_  ( ( 2  x.  j )  - 
1 ) )
415400, 404, 405, 408, 414ltletrd 9759 . . . . . . . . . 10  |-  ( j  e.  ( 1 ... k )  ->  0  <  ( ( 2  x.  j )  -  1 ) )
416 elnnz 10895 . . . . . . . . . 10  |-  ( ( ( 2  x.  j
)  -  1 )  e.  NN  <->  ( (
( 2  x.  j
)  -  1 )  e.  ZZ  /\  0  <  ( ( 2  x.  j )  -  1 ) ) )
417399, 415, 416sylanbrc 664 . . . . . . . . 9  |-  ( j  e.  ( 1 ... k )  ->  (
( 2  x.  j
)  -  1 )  e.  NN )
418417adantl 466 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 1 ... k
) )  ->  (
( 2  x.  j
)  -  1 )  e.  NN )
419394, 418ffvelrnd 6033 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 1 ... k
) )  ->  ( F `  ( (
2  x.  j )  -  1 ) )  e.  CC )
420419adantlr 714 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 1 ... k
) )  ->  ( F `  ( (
2  x.  j )  -  1 ) )  e.  CC )
42159fveq2d 5876 . . . . . . . 8  |-  ( k  =  j  ->  ( F `  ( (
2  x.  k )  -  1 ) )  =  ( F `  ( ( 2  x.  j )  -  1 ) ) )
422421cbvmptv 4548 . . . . . . 7  |-  ( k  e.  NN  |->  ( F `
 ( ( 2  x.  k )  - 
1 ) ) )  =  ( j  e.  NN  |->  ( F `  ( ( 2  x.  j )  -  1 ) ) )
423422fvmpt2 5964 . . . . . 6  |-  ( ( j  e.  NN  /\  ( F `  ( ( 2  x.  j )  -  1 ) )  e.  CC )  -> 
( ( k