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

Theorem sumnnodd 31495
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 1683 . . 3  |-  F/ k
ph
2 nfcv 2629 . . 3  |-  F/_ k  seq 1 (  +  ,  F )
3 nfcv 2629 . . . 4  |-  F/_ k
1
4 nfcv 2629 . . . 4  |-  F/_ k  +
5 nfmpt1 4542 . . . 4  |-  F/_ k
( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) )
63, 4, 5nfseq 12097 . . 3  |-  F/_ k  seq 1 (  +  , 
( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) ) )
7 nfmpt1 4542 . . 3  |-  F/_ k
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) )
8 nnuz 11129 . . 3  |-  NN  =  ( ZZ>= `  1 )
9 1zzd 10907 . . 3  |-  ( ph  ->  1  e.  ZZ )
10 seqex 12089 . . . 4  |-  seq 1
(  +  ,  F
)  e.  _V
1110a1i 11 . . 3  |-  ( ph  ->  seq 1 (  +  ,  F )  e. 
_V )
12 sumnnodd.1 . . . . . . 7  |-  ( ph  ->  F : NN --> CC )
1312adantr 465 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  F : NN
--> CC )
14 simpr 461 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
1513, 14ffvelrnd 6033 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 k )  e.  CC )
16 addcl 9586 . . . . . 6  |-  ( ( k  e.  CC  /\  n  e.  CC )  ->  ( k  +  n
)  e.  CC )
1716adantl 466 . . . . 5  |-  ( (
ph  /\  ( k  e.  CC  /\  n  e.  CC ) )  -> 
( k  +  n
)  e.  CC )
188, 9, 15, 17seqf 12108 . . . 4  |-  ( ph  ->  seq 1 (  +  ,  F ) : NN --> CC )
1918ffvelrnda 6032 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq 1 (  +  ,  F ) `  k
)  e.  CC )
20 sumnnodd.sc . . 3  |-  ( ph  ->  seq 1 (  +  ,  F )  ~~>  B )
21 1nn 10559 . . . . . . 7  |-  1  e.  NN
22 oveq2 6303 . . . . . . . . 9  |-  ( k  =  1  ->  (
2  x.  k )  =  ( 2  x.  1 ) )
2322oveq1d 6310 . . . . . . . 8  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  1 )  - 
1 ) )
24 eqid 2467 . . . . . . . 8  |-  ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) )  =  ( k  e.  NN  |->  ( ( 2  x.  k )  - 
1 ) )
25 ovex 6320 . . . . . . . 8  |-  ( ( 2  x.  1 )  -  1 )  e. 
_V
2623, 24, 25fvmpt 5957 . . . . . . 7  |-  ( 1  e.  NN  ->  (
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `  1
)  =  ( ( 2  x.  1 )  -  1 ) )
2721, 26ax-mp 5 . . . . . 6  |-  ( ( k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) ) `  1 )  =  ( ( 2  x.  1 )  - 
1 )
28 2t1e2 10696 . . . . . . 7  |-  ( 2  x.  1 )  =  2
2928oveq1i 6305 . . . . . 6  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
30 2m1e1 10662 . . . . . 6  |-  ( 2  -  1 )  =  1
3127, 29, 303eqtri 2500 . . . . 5  |-  ( ( k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) ) `  1 )  =  1
3231, 21eqeltri 2551 . . . 4  |-  ( ( k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) ) `  1 )  e.  NN
3332a1i 11 . . 3  |-  ( ph  ->  ( ( k  e.  NN  |->  ( ( 2  x.  k )  - 
1 ) ) ` 
1 )  e.  NN )
34 2z 10908 . . . . . . . . 9  |-  2  e.  ZZ
3534a1i 11 . . . . . . . 8  |-  ( k  e.  NN  ->  2  e.  ZZ )
36 nnz 10898 . . . . . . . 8  |-  ( k  e.  NN  ->  k  e.  ZZ )
3735, 36zmulcld 10984 . . . . . . 7  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  ZZ )
3836peano2zd 10981 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  ZZ )
3935, 38zmulcld 10984 . . . . . . . 8  |-  ( k  e.  NN  ->  (
2  x.  ( k  +  1 ) )  e.  ZZ )
40 1zzd 10907 . . . . . . . 8  |-  ( k  e.  NN  ->  1  e.  ZZ )
4139, 40zsubcld 10983 . . . . . . 7  |-  ( k  e.  NN  ->  (
( 2  x.  (
k  +  1 ) )  -  1 )  e.  ZZ )
42 2re 10617 . . . . . . . . . . 11  |-  2  e.  RR
4342a1i 11 . . . . . . . . . 10  |-  ( k  e.  NN  ->  2  e.  RR )
44 nnre 10555 . . . . . . . . . 10  |-  ( k  e.  NN  ->  k  e.  RR )
4543, 44remulcld 9636 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  RR )
4645lep1d 10489 . . . . . . . 8  |-  ( k  e.  NN  ->  (
2  x.  k )  <_  ( ( 2  x.  k )  +  1 ) )
47 2cnd 10620 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  2  e.  CC )
48 nncn 10556 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  k  e.  CC )
49 1cnd 9624 . . . . . . . . . . . 12  |-  ( k  e.  NN  ->  1  e.  CC )
5047, 48, 49adddid 9632 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
2  x.  ( k  +  1 ) )  =  ( ( 2  x.  k )  +  ( 2  x.  1 ) ) )
5128oveq2i 6306 . . . . . . . . . . . 12  |-  ( ( 2  x.  k )  +  ( 2  x.  1 ) )  =  ( ( 2  x.  k )  +  2 )
5251a1i 11 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  +  ( 2  x.  1 ) )  =  ( ( 2  x.  k )  +  2 ) )
5350, 52eqtrd 2508 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
2  x.  ( k  +  1 ) )  =  ( ( 2  x.  k )  +  2 ) )
5453oveq1d 6310 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( 2  x.  (
k  +  1 ) )  -  1 )  =  ( ( ( 2  x.  k )  +  2 )  - 
1 ) )
5547, 48mulcld 9628 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  CC )
5655, 47, 49addsubassd 9962 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( ( 2  x.  k )  +  2 )  -  1 )  =  ( ( 2  x.  k )  +  ( 2  -  1 ) ) )
5730oveq2i 6306 . . . . . . . . . 10  |-  ( ( 2  x.  k )  +  ( 2  -  1 ) )  =  ( ( 2  x.  k )  +  1 )
5857a1i 11 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  +  ( 2  -  1 ) )  =  ( ( 2  x.  k )  +  1 ) )
5954, 56, 583eqtrrd 2513 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  ( k  +  1 ) )  - 
1 ) )
6046, 59breqtrd 4477 . . . . . . 7  |-  ( k  e.  NN  ->  (
2  x.  k )  <_  ( ( 2  x.  ( k  +  1 ) )  - 
1 ) )
6137, 41, 603jca 1176 . . . . . 6  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  e.  ZZ  /\  ( ( 2  x.  ( k  +  1 ) )  -  1 )  e.  ZZ  /\  ( 2  x.  k
)  <_  ( (
2  x.  ( k  +  1 ) )  -  1 ) ) )
62 eluz2 11100 . . . . . 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 ) ) )
6361, 62sylibr 212 . . . . 5  |-  ( k  e.  NN  ->  (
( 2  x.  (
k  +  1 ) )  -  1 )  e.  ( ZZ>= `  (
2  x.  k ) ) )
64 oveq2 6303 . . . . . . . . . 10  |-  ( k  =  j  ->  (
2  x.  k )  =  ( 2  x.  j ) )
6564oveq1d 6310 . . . . . . . . 9  |-  ( k  =  j  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  j )  - 
1 ) )
6665cbvmptv 4544 . . . . . . . 8  |-  ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) )  =  ( j  e.  NN  |->  ( ( 2  x.  j )  - 
1 ) )
6766a1i 11 . . . . . . 7  |-  ( k  e.  NN  ->  (
k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) )  =  ( j  e.  NN  |->  ( ( 2  x.  j )  -  1 ) ) )
68 oveq2 6303 . . . . . . . . 9  |-  ( j  =  ( k  +  1 )  ->  (
2  x.  j )  =  ( 2  x.  ( k  +  1 ) ) )
6968oveq1d 6310 . . . . . . . 8  |-  ( j  =  ( k  +  1 )  ->  (
( 2  x.  j
)  -  1 )  =  ( ( 2  x.  ( k  +  1 ) )  - 
1 ) )
7069adantl 466 . . . . . . 7  |-  ( ( k  e.  NN  /\  j  =  ( k  +  1 ) )  ->  ( ( 2  x.  j )  - 
1 )  =  ( ( 2  x.  (
k  +  1 ) )  -  1 ) )
71 peano2nn 10560 . . . . . . 7  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
7267, 70, 71, 41fvmptd 5962 . . . . . 6  |-  ( k  e.  NN  ->  (
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `  (
k  +  1 ) )  =  ( ( 2  x.  ( k  +  1 ) )  -  1 ) )
73 id 22 . . . . . . . . . 10  |-  ( k  e.  NN  ->  k  e.  NN )
7437, 40zsubcld 10983 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  -  1 )  e.  ZZ )
7524fvmpt2 5964 . . . . . . . . . 10  |-  ( ( k  e.  NN  /\  ( ( 2  x.  k )  -  1 )  e.  ZZ )  ->  ( ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `
 k )  =  ( ( 2  x.  k )  -  1 ) )
7673, 74, 75syl2anc 661 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `  k
)  =  ( ( 2  x.  k )  -  1 ) )
7776oveq1d 6310 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( ( k  e.  NN  |->  ( ( 2  x.  k )  - 
1 ) ) `  k )  +  1 )  =  ( ( ( 2  x.  k
)  -  1 )  +  1 ) )
7855, 49npcand 9946 . . . . . . . 8  |-  ( k  e.  NN  ->  (
( ( 2  x.  k )  -  1 )  +  1 )  =  ( 2  x.  k ) )
7977, 78eqtrd 2508 . . . . . . 7  |-  ( k  e.  NN  ->  (
( ( k  e.  NN  |->  ( ( 2  x.  k )  - 
1 ) ) `  k )  +  1 )  =  ( 2  x.  k ) )
8079fveq2d 5876 . . . . . 6  |-  ( k  e.  NN  ->  ( ZZ>=
`  ( ( ( k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) ) `  k )  +  1 ) )  =  ( ZZ>= `  (
2  x.  k ) ) )
8172, 80eleq12d 2549 . . . . 5  |-  ( k  e.  NN  ->  (
( ( k  e.  NN  |->  ( ( 2  x.  k )  - 
1 ) ) `  ( k  +  1 ) )  e.  (
ZZ>= `  ( ( ( k  e.  NN  |->  ( ( 2  x.  k
)  -  1 ) ) `  k )  +  1 ) )  <-> 
( ( 2  x.  ( k  +  1 ) )  -  1 )  e.  ( ZZ>= `  ( 2  x.  k
) ) ) )
8263, 81mpbird 232 . . . 4  |-  ( k  e.  NN  ->  (
( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `  (
k  +  1 ) )  e.  ( ZZ>= `  ( ( ( k  e.  NN  |->  ( ( 2  x.  k )  -  1 ) ) `
 k )  +  1 ) ) )
8382adantl 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 ) ) )
84 seqex 12089 . . . 4  |-  seq 1
(  +  ,  ( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) ) )  e.  _V
8584a1i 11 . . 3  |-  ( ph  ->  seq 1 (  +  ,  ( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) ) )  e.  _V )
86 elfznn 11726 . . . . . . . 8  |-  ( j  e.  ( 1 ... k )  ->  j  e.  NN )
8786adantl 466 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 1 ... k
) )  ->  j  e.  NN )
8812adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... k
) )  ->  F : NN --> CC )
8934a1i 11 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... k )  ->  2  e.  ZZ )
90 elfzelz 11700 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... k )  ->  j  e.  ZZ )
9189, 90zmulcld 10984 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... k )  ->  (
2  x.  j )  e.  ZZ )
92 1zzd 10907 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... k )  ->  1  e.  ZZ )
9391, 92zsubcld 10983 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... k )  ->  (
( 2  x.  j
)  -  1 )  e.  ZZ )
94 0red 9609 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... k )  ->  0  e.  RR )
9542a1i 11 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... k )  ->  2  e.  RR )
9628, 95syl5eqel 2559 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... k )  ->  (
2  x.  1 )  e.  RR )
97 1red 9623 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... k )  ->  1  e.  RR )
9896, 97resubcld 9999 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... k )  ->  (
( 2  x.  1 )  -  1 )  e.  RR )
9993zred 10978 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... k )  ->  (
( 2  x.  j
)  -  1 )  e.  RR )
100 0lt1 10087 . . . . . . . . . . . . . . 15  |-  0  <  1
101100a1i 11 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... k )  ->  0  <  1 )
10229, 30eqtr2i 2497 . . . . . . . . . . . . . . 15  |-  1  =  ( ( 2  x.  1 )  - 
1 )
103102a1i 11 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... k )  ->  1  =  ( ( 2  x.  1 )  - 
1 ) )
104101, 103breqtrd 4477 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... k )  ->  0  <  ( ( 2  x.  1 )  -  1 ) )
10591zred 10978 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... k )  ->  (
2  x.  j )  e.  RR )
10686nnred 10563 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... k )  ->  j  e.  RR )
107 0le2 10638 . . . . . . . . . . . . . . . 16  |-  0  <_  2
108107a1i 11 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... k )  ->  0  <_  2 )
10986nnge1d 10590 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... k )  ->  1  <_  j )
11097, 106, 95, 108, 109lemul2ad 10498 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... k )  ->  (
2  x.  1 )  <_  ( 2  x.  j ) )
11196, 105, 97, 110lesub1dd 10180 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... k )  ->  (
( 2  x.  1 )  -  1 )  <_  ( ( 2  x.  j )  - 
1 ) )
11294, 98, 99, 104, 111ltletrd 9753 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... k )  ->  0  <  ( ( 2  x.  j )  -  1 ) )
11393, 112jca 532 . . . . . . . . . . 11  |-  ( j  e.  ( 1 ... k )  ->  (
( ( 2  x.  j )  -  1 )  e.  ZZ  /\  0  <  ( ( 2  x.  j )  - 
1 ) ) )
114 elnnz 10886 . . . . . . . . . . 11  |-  ( ( ( 2  x.  j
)  -  1 )  e.  NN  <->  ( (
( 2  x.  j
)  -  1 )  e.  ZZ  /\  0  <  ( ( 2  x.  j )  -  1 ) ) )
115113, 114sylibr 212 . . . . . . . . . 10  |-  ( j  e.  ( 1 ... k )  ->  (
( 2  x.  j
)  -  1 )  e.  NN )
116115adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... k
) )  ->  (
( 2  x.  j
)  -  1 )  e.  NN )
11788, 116ffvelrnd 6033 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 1 ... k
) )  ->  ( F `  ( (
2  x.  j )  -  1 ) )  e.  CC )
118117adantlr 714 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 1 ... k
) )  ->  ( F `  ( (
2  x.  j )  -  1 ) )  e.  CC )
11965fveq2d 5876 . . . . . . . . 9  |-  ( k  =  j  ->  ( F `  ( (
2  x.  k )  -  1 ) )  =  ( F `  ( ( 2  x.  j )  -  1 ) ) )
120119cbvmptv 4544 . . . . . . . 8  |-  ( k  e.  NN  |->  ( F `
 ( ( 2  x.  k )  - 
1 ) ) )  =  ( j  e.  NN  |->  ( F `  ( ( 2  x.  j )  -  1 ) ) )
121120fvmpt2 5964 . . . . . . 7  |-  ( ( j  e.  NN  /\  ( F `  ( ( 2  x.  j )  -  1 ) )  e.  CC )  -> 
( ( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) ) `  j )  =  ( F `  ( ( 2  x.  j )  -  1 ) ) )
12287, 118, 121syl2anc 661 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 1 ... k
) )  ->  (
( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) ) `  j )  =  ( F `  ( ( 2  x.  j )  -  1 ) ) )
12314, 8syl6eleq 2565 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ( ZZ>= `  1 )
)
124122, 123, 118fsumser 13532 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  sum_ j  e.  ( 1 ... k
) ( F `  ( ( 2  x.  j )  -  1 ) )  =  (  seq 1 (  +  ,  ( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) ) ) `
 k ) )
125124eqcomd 2475 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq 1 (  +  , 
( k  e.  NN  |->  ( F `  ( ( 2  x.  k )  -  1 ) ) ) ) `  k
)  =  sum_ j  e.  ( 1 ... k
) ( F `  ( ( 2  x.  j )  -  1 ) ) )
126 incom 3696 . . . . . . . . . . 11  |-  ( ( ( 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 } ) )
127 inss2 3724 . . . . . . . . . . . 12  |-  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  C_  { n  e.  NN  | 
( n  /  2
)  e.  NN }
128 ssrin 3728 . . . . . . . . . . . 12  |-  ( ( ( 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 } ) ) )
129127, 128ax-mp 5 . . . . . . . . . . 11  |-  ( ( ( 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 } ) )
130126, 129eqsstri 3539 . . . . . . . . . 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 }
) )  C_  ( { n  e.  NN  |  ( n  / 
2 )  e.  NN }  i^i  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )
131 disjdif 3905 . . . . . . . . . 10  |-  ( { n  e.  NN  | 
( n  /  2
)  e.  NN }  i^i  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  =  (/)
132130, 131sseqtri 3541 . . . . . . . . 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_  (/)
133 ss0 3821 . . . . . . . . 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_  (/) 
->  ( ( ( 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 } ) )  =  (/) )
134132, 133ax-mp 5 . . . . . . . 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 }
) )  =  (/)
135134a1i 11 . . . . . . 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 }
) )  =  (/) )
136 uncom 3653 . . . . . . . . . 10  |-  ( ( ( 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 } ) )
137 inundif 3911 . . . . . . . . . 10  |-  ( ( ( 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 ) )
138136, 137eqtri 2496 . . . . . . . . 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 ) )
139138eqcomi 2480 . . . . . . . 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 } ) )
140139a1i 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 } ) ) )
141 fzfid 12063 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1 ... ( ( 2  x.  k )  - 
1 ) )  e. 
Fin )
14212adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) )  ->  F : NN --> CC )
143 elfznn 11726 . . . . . . . . . 10  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  j  e.  NN )
144143adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) )  ->  j  e.  NN )
145142, 144ffvelrnd 6033 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) )  ->  ( F `  j )  e.  CC )
146145adantlr 714 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) )  ->  ( F `  j )  e.  CC )
147135, 140, 141, 146fsumsplit 13542 . . . . . 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 ) ) )
148 simpl 457 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  ph )
149127sseli 3505 . . . . . . . . . . . . . . 15  |-  ( 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 } )
150 ssrab2 3590 . . . . . . . . . . . . . . . 16  |-  { n  e.  NN  |  ( n  /  2 )  e.  NN }  C_  NN
151150sseli 3505 . . . . . . . . . . . . . . 15  |-  ( j  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN }  ->  j  e.  NN )
152149, 151syl 16 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  i^i 
{ n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  e.  NN )
153152adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  j  e.  NN )
154 oveq1 6302 . . . . . . . . . . . . . . . . 17  |-  ( k  =  j  ->  (
k  /  2 )  =  ( j  / 
2 ) )
155154eleq1d 2536 . . . . . . . . . . . . . . . 16  |-  ( k  =  j  ->  (
( k  /  2
)  e.  NN  <->  ( j  /  2 )  e.  NN ) )
156 oveq1 6302 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  (
n  /  2 )  =  ( k  / 
2 ) )
157156eleq1d 2536 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  (
( n  /  2
)  e.  NN  <->  ( k  /  2 )  e.  NN ) )
158157elrab 3266 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN }  <->  ( k  e.  NN  /\  ( k  /  2 )  e.  NN ) )
159158simprbi 464 . . . . . . . . . . . . . . . 16  |-  ( k  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN }  ->  (
k  /  2 )  e.  NN )
160155, 159vtoclga 3182 . . . . . . . . . . . . . . 15  |-  ( j  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN }  ->  (
j  /  2 )  e.  NN )
161149, 160syl 16 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  i^i 
{ n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  (
j  /  2 )  e.  NN )
162161adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  (
j  /  2 )  e.  NN )
163 eleq1 2539 . . . . . . . . . . . . . . . 16  |-  ( k  =  j  ->  (
k  e.  NN  <->  j  e.  NN ) )
164163, 1553anbi23d 1302 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
( ph  /\  k  e.  NN  /\  ( k  /  2 )  e.  NN )  <->  ( ph  /\  j  e.  NN  /\  ( j  /  2
)  e.  NN ) ) )
165 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( k  =  j  ->  ( F `  k )  =  ( F `  j ) )
166165eqeq1d 2469 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
( F `  k
)  =  0  <->  ( F `  j )  =  0 ) )
167164, 166imbi12d 320 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( ( ph  /\  k  e.  NN  /\  (
k  /  2 )  e.  NN )  -> 
( F `  k
)  =  0 )  <-> 
( ( ph  /\  j  e.  NN  /\  (
j  /  2 )  e.  NN )  -> 
( F `  j
)  =  0 ) ) )
168 sumnnodd.even0 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN  /\  ( k  / 
2 )  e.  NN )  ->  ( F `  k )  =  0 )
169167, 168chvarv 1983 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  NN  /\  ( j  / 
2 )  e.  NN )  ->  ( F `  j )  =  0 )
170148, 153, 162, 169syl3anc 1228 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  ( F `  j )  =  0 )
171170ralrimiva 2881 . . . . . . . . . . 11  |-  ( ph  ->  A. j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ( F `  j )  =  0 )
172171sumeq2d 13504 . . . . . . . . . 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 )
173 fzfid 12063 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... (
( 2  x.  k
)  -  1 ) )  e.  Fin )
174 inss1 3723 . . . . . . . . . . . . . 14  |-  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  C_  ( 1 ... (
( 2  x.  k
)  -  1 ) )
175174a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)  C_  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )
176 ssfi 7752 . . . . . . . . . . . . 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 )
177173, 175, 176syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  i^i  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
)  e.  Fin )
178 olc 384 . . . . . . . . . . . 12  |-  ( ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  e. 
Fin  ->  ( ( ( 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 )
)
179177, 178syl 16 . . . . . . . . . . 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 )
)
180 sumz 13524 . . . . . . . . . . 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 )
181179, 180syl 16 . . . . . . . . . 10  |-  ( ph  -> 
sum_ j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) 0  =  0 )
182172, 181eqtrd 2508 . . . . . . . . 9  |-  ( ph  -> 
sum_ j  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  i^i  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) ( F `  j )  =  0 )
183182adantr 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 )
184183oveq2d 6311 . . . . . . 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 ) )
185 fzfi 12062 . . . . . . . . . . . . 13  |-  ( 1 ... ( ( 2  x.  k )  - 
1 ) )  e. 
Fin
186 difss 3636 . . . . . . . . . . . . 13  |-  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  C_  ( 1 ... (
( 2  x.  k
)  -  1 ) )
187185, 186pm3.2i 455 . . . . . . . . . . . 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 ) ) )
188 ssfi 7752 . . . . . . . . . . . 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 )
189187, 188ax-mp 5 . . . . . . . . . . 11  |-  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  e. 
Fin
190189a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  e. 
Fin )
191 simpl 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  ph )
192186sseli 3505 . . . . . . . . . . . . 13  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) )
193192adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  j  e.  ( 1 ... (
( 2  x.  k
)  -  1 ) ) )
194191, 193, 145syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  ( F `  j )  e.  CC )
195194adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) )  ->  ( F `  j )  e.  CC )
196190, 195fsumcl 13535 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  sum_ j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) )  \  {
n  e.  NN  | 
( n  /  2
)  e.  NN }
) ( F `  j )  e.  CC )
197196addid1d 9791 . . . . . . . 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 ) )
198 fveq2 5872 . . . . . . . . . 10  |-  ( j  =  i  ->  ( F `  j )  =  ( F `  i ) )
199198cbvsumv 13498 . . . . . . . . 9  |-  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 )
200199a1i 11 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  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 ) )
201197, 200eqtrd 2508 . . . . . . 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 ) )
202184, 201eqtrd 2508 . . . . . 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 ) )
203 fveq2 5872 . . . . . . 7  |-  ( i  =  ( ( 2  x.  j )  - 
1 )  ->  ( F `  i )  =  ( F `  ( ( 2  x.  j )  -  1 ) ) )
204 fzfid 12063 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1 ... k )  e. 
Fin )
20540adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  1  e.  ZZ )
20674adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( ( 2  x.  k )  - 
1 )  e.  ZZ )
20734a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  2  e.  ZZ )
208 elfzelz 11700 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  i  e.  ZZ )
209207, 208zmulcld 10984 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  (
2  x.  i )  e.  ZZ )
210 1zzd 10907 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  1  e.  ZZ )
211209, 210zsubcld 10983 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  (
( 2  x.  i
)  -  1 )  e.  ZZ )
212211adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( ( 2  x.  i )  - 
1 )  e.  ZZ )
213205, 206, 2123jca 1176 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( 1  e.  ZZ  /\  ( ( 2  x.  k )  -  1 )  e.  ZZ  /\  ( ( 2  x.  i )  -  1 )  e.  ZZ ) )
214102a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  1  =  ( ( 2  x.  1 )  - 
1 ) )
215 1re 9607 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  RR
21642, 215remulcli 9622 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 2  x.  1 )  e.  RR
217216a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  (
2  x.  1 )  e.  RR )
218209zred 10978 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  (
2  x.  i )  e.  RR )
219 1red 9623 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  1  e.  RR )
220208zred 10978 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 1 ... k )  ->  i  e.  RR )
22142a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 1 ... k )  ->  2  e.  RR )
222107a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 1 ... k )  ->  0  <_  2 )
223 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 1 ... k )  ->  1  <_  i )
224219, 220, 221, 222, 223lemul2ad 10498 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  (
2  x.  1 )  <_  ( 2  x.  i ) )
225217, 218, 219, 224lesub1dd 10180 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  (
( 2  x.  1 )  -  1 )  <_  ( ( 2  x.  i )  - 
1 ) )
226214, 225eqbrtrd 4473 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  1  <_  ( ( 2  x.  i )  -  1 ) )
227226adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  1  <_  (
( 2  x.  i
)  -  1 ) )
228218adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( 2  x.  i )  e.  RR )
22945adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( 2  x.  k )  e.  RR )
230215a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  1  e.  RR )
231220adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  i  e.  RR )
23244adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  k  e.  RR )
23342a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  2  e.  RR )
234107a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  0  <_  2
)
235 elfzle2 11702 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  i  <_  k )
236235adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  i  <_  k
)
237231, 232, 233, 234, 236lemul2ad 10498 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( 2  x.  i )  <_  (
2  x.  k ) )
238228, 229, 230, 237lesub1dd 10180 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( ( 2  x.  i )  - 
1 )  <_  (
( 2  x.  k
)  -  1 ) )
239227, 238jca 532 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( 1  <_ 
( ( 2  x.  i )  -  1 )  /\  ( ( 2  x.  i )  -  1 )  <_ 
( ( 2  x.  k )  -  1 ) ) )
240213, 239jca 532 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( ( 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 ) ) ) )
241 elfz2 11691 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) ) )
242240, 241sylibr 212 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( ( 2  x.  i )  - 
1 )  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) ) )
243218recnd 9634 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  (
2  x.  i )  e.  CC )
244 1cnd 9624 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  1  e.  CC )
245221recnd 9634 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  2  e.  CC )
246 2ne0 10640 . . . . . . . . . . . . . . . . . . . . 21  |-  2  =/=  0
247246a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  2  =/=  0 )
248243, 244, 245, 247divsubdird 10371 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  (
( ( 2  x.  i )  -  1 )  /  2 )  =  ( ( ( 2  x.  i )  /  2 )  -  ( 1  /  2
) ) )
249220recnd 9634 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 1 ... k )  ->  i  e.  CC )
250249, 245, 247divcan3d 10337 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  (
( 2  x.  i
)  /  2 )  =  i )
251250oveq1d 6310 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  (
( ( 2  x.  i )  /  2
)  -  ( 1  /  2 ) )  =  ( i  -  ( 1  /  2
) ) )
252248, 251eqtrd 2508 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  (
( ( 2  x.  i )  -  1 )  /  2 )  =  ( i  -  ( 1  /  2
) ) )
253208, 210zsubcld 10983 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  (
i  -  1 )  e.  ZZ )
254221, 247rereccld 10383 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 1 ... k )  ->  (
1  /  2 )  e.  RR )
255 halflt1 10769 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  /  2 )  <  1
256255a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 1 ... k )  ->  (
1  /  2 )  <  1 )
257254, 219, 220, 256ltsub2dd 10177 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  (
i  -  1 )  <  ( i  -  ( 1  /  2
) ) )
258 2rp 11237 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  e.  RR+
259 rpreccl 11255 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 2  e.  RR+  ->  ( 1  /  2 )  e.  RR+ )
260258, 259ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 1  /  2 )  e.  RR+
261260a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 1 ... k )  ->  (
1  /  2 )  e.  RR+ )
262220, 261ltsubrpd 11296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 1 ... k )  ->  (
i  -  ( 1  /  2 ) )  <  i )
263249, 244npcand 9946 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 1 ... k )  ->  (
( i  -  1 )  +  1 )  =  i )
264263eqcomd 2475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 1 ... k )  ->  i  =  ( ( i  -  1 )  +  1 ) )
265262, 264breqtrd 4477 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... k )  ->  (
i  -  ( 1  /  2 ) )  <  ( ( i  -  1 )  +  1 ) )
266 btwnnz 10949 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( i  -  1 )  e.  ZZ  /\  ( i  -  1 )  <  ( i  -  ( 1  / 
2 ) )  /\  ( i  -  (
1  /  2 ) )  <  ( ( i  -  1 )  +  1 ) )  ->  -.  ( i  -  ( 1  / 
2 ) )  e.  ZZ )
267253, 257, 265, 266syl3anc 1228 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... k )  ->  -.  ( i  -  (
1  /  2 ) )  e.  ZZ )
268 nnz 10898 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  -  ( 1  /  2 ) )  e.  NN  ->  (
i  -  ( 1  /  2 ) )  e.  ZZ )
269268con3i 135 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( i  -  (
1  /  2 ) )  e.  ZZ  ->  -.  ( i  -  (
1  /  2 ) )  e.  NN )
270267, 269syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... k )  ->  -.  ( i  -  (
1  /  2 ) )  e.  NN )
271252, 270eqneltrd 2576 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... k )  ->  -.  ( ( ( 2  x.  i )  - 
1 )  /  2
)  e.  NN )
272 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 2  x.  i )  -  1 )  e.  NN  /\  ( ( ( 2  x.  i )  - 
1 )  /  2
)  e.  NN )  ->  ( ( ( 2  x.  i )  -  1 )  / 
2 )  e.  NN )
273272con3i 135 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( 2  x.  i )  - 
1 )  /  2
)  e.  NN  ->  -.  ( ( ( 2  x.  i )  - 
1 )  e.  NN  /\  ( ( ( 2  x.  i )  - 
1 )  /  2
)  e.  NN ) )
274271, 273syl 16 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... k )  ->  -.  ( ( ( 2  x.  i )  - 
1 )  e.  NN  /\  ( ( ( 2  x.  i )  - 
1 )  /  2
)  e.  NN ) )
275 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( ( 2  x.  i )  - 
1 )  ->  (
n  /  2 )  =  ( ( ( 2  x.  i )  -  1 )  / 
2 ) )
276275eleq1d 2536 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( ( 2  x.  i )  - 
1 )  ->  (
( n  /  2
)  e.  NN  <->  ( (
( 2  x.  i
)  -  1 )  /  2 )  e.  NN ) )
277276elrab 3266 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) )
278274, 277sylnibr 305 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... k )  ->  -.  ( ( 2  x.  i )  -  1 )  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN } )
279278adantl 466 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  -.  ( (
2  x.  i )  -  1 )  e. 
{ n  e.  NN  |  ( n  / 
2 )  e.  NN } )
280242, 279eldifd 3492 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN  /\  i  e.  ( 1 ... k ) )  ->  ( ( 2  x.  i )  - 
1 )  e.  ( ( 1 ... (
( 2  x.  k
)  -  1 ) )  \  { n  e.  NN  |  ( n  /  2 )  e.  NN } ) )
281 eqid 2467 . . . . . . . . . . . . 13  |-  ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) )  =  ( i  e.  ( 1 ... k
)  |->  ( ( 2  x.  i )  - 
1 ) )
282280, 281fmptd 6056 . . . . . . . . . . . 12  |-  ( 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 } ) )
283 simpl 457 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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  e.  ( 1 ... k
)  /\  y  e.  ( 1 ... k
) ) )
284 eqidd 2468 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( 1 ... k )  ->  (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) )  =  ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) )
285 oveq2 6303 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  x  ->  (
2  x.  i )  =  ( 2  x.  x ) )
286285oveq1d 6310 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  x  ->  (
( 2  x.  i
)  -  1 )  =  ( ( 2  x.  x )  - 
1 ) )
287286adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ( 1 ... k )  /\  i  =  x )  ->  ( ( 2  x.  i )  -  1 )  =  ( ( 2  x.  x )  -  1 ) )
288 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( 1 ... k )  ->  x  e.  ( 1 ... k
) )
289 ovex 6320 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  x.  x )  -  1 )  e. 
_V
290289a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( 1 ... k )  ->  (
( 2  x.  x
)  -  1 )  e.  _V )
291284, 287, 288, 290fvmptd 5962 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( 1 ... k )  ->  (
( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  x
)  =  ( ( 2  x.  x )  -  1 ) )
292291eqcomd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( 1 ... k )  ->  (
( 2  x.  x
)  -  1 )  =  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 x ) )
293292ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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
) )
294 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
295 eqidd 2468 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 ... k )  ->  (
i  e.  ( 1 ... k )  |->  ( ( 2  x.  i
)  -  1 ) )  =  ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) )
296 oveq2 6303 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  y  ->  (
2  x.  i )  =  ( 2  x.  y ) )
297296oveq1d 6310 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  y  ->  (
( 2  x.  i
)  -  1 )  =  ( ( 2  x.  y )  - 
1 ) )
298297adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  ( 1 ... k )  /\  i  =  y )  ->  ( ( 2  x.  i )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )
299 id 22 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 ... k )  ->  y  e.  ( 1 ... k
) )
300 ovex 6320 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2  x.  y )  -  1 )  e. 
_V
301300a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 ... k )  ->  (
( 2  x.  y
)  -  1 )  e.  _V )
302295, 298, 299, 301fvmptd 5962 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( 1 ... k )  ->  (
( i  e.  ( 1 ... k ) 
|->  ( ( 2  x.  i )  -  1 ) ) `  y
)  =  ( ( 2  x.  y )  -  1 ) )
303302ad2antlr 726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
304293, 294, 3033eqtrd 2512 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) )
305 simpl 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  (
x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) ) )
306 2cnd 10620 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( 1 ... k )  ->  2  e.  CC )
307 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( 1 ... k )  ->  x  e.  ZZ )
308307zcnd 10979 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( 1 ... k )  ->  x  e.  CC )
309306, 308mulcld 9628 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( 1 ... k )  ->  (
2  x.  x )  e.  CC )
310309ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  (
2  x.  x )  e.  CC )
311 2cnd 10620 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( 1 ... k )  ->  2  e.  CC )
312 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( 1 ... k )  ->  y  e.  ZZ )
313312zcnd 10979 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( 1 ... k )  ->  y  e.  CC )
314311, 313mulcld 9628 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 1 ... k )  ->  (
2  x.  y )  e.  CC )
315314ad2antlr 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  (
2  x.  y )  e.  CC )
316 1cnd 9624 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  1  e.  CC )
317 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  (
( 2  x.  x
)  -  1 )  =  ( ( 2  x.  y )  - 
1 ) )
318310, 315, 316, 317subcan2d 9984 . . . . . . . . . . . . . . . . 17  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  (
2  x.  x )  =  ( 2  x.  y ) )
319 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  (
2  x.  x )  =  ( 2  x.  y ) )
320308ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  x  e.  CC )
321313ad2antlr 726 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  y  e.  CC )
322306ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  2  e.  CC )
323246a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  2  =/=  0 )
324320, 321, 322, 323mulcand 10194 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  (
( 2  x.  x
)  =  ( 2  x.  y )  <->  x  =  y ) )
325319, 324mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( 2  x.  x )  =  ( 2  x.  y
) )  ->  x  =  y )
326305, 318, 325syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  ( 1 ... k )  /\  y  e.  ( 1 ... k ) )  /\  ( ( 2  x.  x )  -  1 )  =  ( ( 2  x.  y )  -  1 ) )  ->  x  =  y )
327283, 304, 326syl2anc 661 . . . . . . . . . . . . . . 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 ) )  ->  x  =  y )
328327adantll 713 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
329328ex 434 . . . . . . . . . . . . 13  |-  ( ( 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 ) )
330329ralrimivva 2888 . . . . . . . . . . . 12  |-  ( 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 )
)
331282, 330jca 532 . . . . . . . . . . 11  |-  ( 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 }
)  /\  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 )
) )
332 dff13 6165 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
333331, 332sylibr 212 . . . . . . . . . 10  |-  ( 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 } ) )
33440adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
1  e.  ZZ )
33536adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
k  e.  ZZ )
336 fzssz 31366 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 1 ... ( ( 2  x.  k )  - 
1 ) )  C_  ZZ
337336a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  (
1 ... ( ( 2  x.  k )  - 
1 ) )  C_  ZZ )
338337, 192sseldd 3510 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  e.  ZZ )
339 zeo 10958 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ZZ  ->  (
( j  /  2
)  e.  ZZ  \/  ( ( j  +  1 )  /  2
)  e.  ZZ ) )
340338, 339syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  (
( j  /  2
)  e.  ZZ  \/  ( ( j  +  1 )  /  2
)  e.  ZZ ) )
341340adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) )
342192, 143syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  e.  NN )
343342adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  j  e.  NN )
344 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  ( j  / 
2 )  e.  ZZ )
345343nnred 10563 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  j  e.  RR )
34642a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  2  e.  RR )
347343nngt0d 10591 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  0  <  j
)
348 2pos 10639 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  <  2
349348a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  0  <  2
)
350345, 346, 347, 349divgt0d 10493 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  0  <  (
j  /  2 ) )
351344, 350jca 532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  ( ( j  /  2 )  e.  ZZ  /\  0  < 
( j  /  2
) ) )
352 elnnz 10886 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( j  /  2 )  e.  NN  <->  ( (
j  /  2 )  e.  ZZ  /\  0  <  ( j  /  2
) ) )
353351, 352sylibr 212 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  ( j  / 
2 )  e.  NN )
354343, 353jca 532 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( j  e.  ( ( 1 ... ( ( 2  x.  k )  -  1 ) ) 
\  { n  e.  NN  |  ( n  /  2 )  e.  NN } )  /\  ( j  /  2
)  e.  ZZ )  ->  ( j  e.  NN  /\  ( j  /  2 )  e.  NN ) )
355 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  j  ->  (
n  /  2 )  =  ( j  / 
2 ) )
356355eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  j  ->  (
( n  /  2
)  e.  NN  <->  ( j  /  2 )  e.  NN ) )
357356elrab 3266 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN }  <->  ( j  e.  NN  /\  ( j  /  2 )  e.  NN ) )
358354, 357sylibr 212 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 }
)
359 eldifn 3632 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  -.  j  e.  { n  e.  NN  |  ( n  /  2 )  e.  NN } )
360359adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 }
)
361358, 360pm2.65da 576 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  -.  ( j  /  2
)  e.  ZZ )
362361adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  ->  -.  ( j  /  2
)  e.  ZZ )
363 pm2.53 373 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( j  /  2
)  e.  ZZ  \/  ( ( j  +  1 )  /  2
)  e.  ZZ )  ->  ( -.  (
j  /  2 )  e.  ZZ  ->  (
( j  +  1 )  /  2 )  e.  ZZ ) )
364363imp 429 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( j  / 
2 )  e.  ZZ  \/  ( ( j  +  1 )  /  2
)  e.  ZZ )  /\  -.  ( j  /  2 )  e.  ZZ )  ->  (
( j  +  1 )  /  2 )  e.  ZZ )
365341, 362, 364syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
( ( j  +  1 )  /  2
)  e.  ZZ )
366334, 335, 3653jca 1176 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) )
367 1p1e2 10661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 1  +  1 )  =  2
368367oveq1i 6305 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1  +  1 )  /  2 )  =  ( 2  /  2
)
369 2div2e1 10670 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 2  /  2 )  =  1
370368, 369eqtr2i 2497 . . . . . . . . . . . . . . . . . . . . 21  |-  1  =  ( ( 1  +  1 )  / 
2 )
371370a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  1  =  ( ( 1  +  1 )  / 
2 ) )
372215a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  1  e.  RR )
373372, 372readdcld 9635 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
1  +  1 )  e.  RR )
374143nnred 10563 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  j  e.  RR )
375374, 372readdcld 9635 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
j  +  1 )  e.  RR )
376258a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  2  e.  RR+ )
377143nnge1d 10590 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  1  <_  j )
378372, 374, 372, 377leadd1dd 10178 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
1  +  1 )  <_  ( j  +  1 ) )
379373, 375, 376, 378lediv1dd 11322 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
( 1  +  1 )  /  2 )  <_  ( ( j  +  1 )  / 
2 ) )
380371, 379eqbrtrd 4473 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  1  <_  ( ( j  +  1 )  /  2
) )
381192, 380syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  1  <_  ( ( j  +  1 )  /  2
) )
382381adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
1  <_  ( (
j  +  1 )  /  2 ) )
383 simpl 457 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
k  e.  NN )
384192adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )
385 elfzel2 11698 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
( 2  x.  k
)  -  1 )  e.  ZZ )
386385zred 10978 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
( 2  x.  k
)  -  1 )  e.  RR )
387386, 372readdcld 9635 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
( ( 2  x.  k )  -  1 )  +  1 )  e.  RR )
388 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  j  <_  ( ( 2  x.  k )  -  1 ) )
389374, 386, 372, 388leadd1dd 10178 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
j  +  1 )  <_  ( ( ( 2  x.  k )  -  1 )  +  1 ) )
390375, 387, 376, 389lediv1dd 11322 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 1 ... ( ( 2  x.  k )  -  1 ) )  ->  (
( j  +  1 )  /  2 )  <_  ( ( ( ( 2  x.  k
)  -  1 )  +  1 )  / 
2 ) )
391390adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( j  +  1 )  / 
2 )  <_  (
( ( ( 2  x.  k )  - 
1 )  +  1 )  /  2 ) )
39255adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( 2  x.  k )  e.  CC )
39349adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  1  e.  CC )
394392, 393npcand 9946 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( ( 2  x.  k )  -  1 )  +  1 )  =  ( 2  x.  k ) )
395394oveq1d 6310 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( ( ( 2  x.  k
)  -  1 )  +  1 )  / 
2 )  =  ( ( 2  x.  k
)  /  2 ) )
396246a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  NN  ->  2  =/=  0 )
39748, 47, 396divcan3d 10337 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  NN  ->  (
( 2  x.  k
)  /  2 )  =  k )
398397adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( 2  x.  k )  / 
2 )  =  k )
399395, 398eqtrd 2508 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( ( ( 2  x.  k
)  -  1 )  +  1 )  / 
2 )  =  k )
400391, 399breqtrd 4477 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN  /\  j  e.  ( 1 ... ( ( 2  x.  k )  - 
1 ) ) )  ->  ( ( j  +  1 )  / 
2 )  <_  k
)
401383, 384, 400syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
( ( j  +  1 )  /  2
)  <_  k )
402366, 382, 401jca32 535 . . . . . . . . . . . . . . . 16  |-  ( ( 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 )
) )
403 elfz2 11691 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) ) )
404402, 403sylibr 212 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
( ( j  +  1 )  /  2
)  e.  ( 1 ... k ) )
405342nncnd 10564 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  e.  CC )
406 peano2cn 9763 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  CC  ->  (
j  +  1 )  e.  CC )
407 2cnd 10620 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  CC  ->  2  e.  CC )
408246a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  CC  ->  2  =/=  0 )
409406, 407, 408divcan2d 10334 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  CC  ->  (
2  x.  ( ( j  +  1 )  /  2 ) )  =  ( j  +  1 ) )
410409oveq1d 6310 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  CC  ->  (
( 2  x.  (
( j  +  1 )  /  2 ) )  -  1 )  =  ( ( j  +  1 )  - 
1 ) )
411 id 22 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  CC  ->  j  e.  CC )
412 1cnd 9624 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  CC  ->  1  e.  CC )
413411, 412pncand 9943 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  CC  ->  (
( j  +  1 )  -  1 )  =  j )
414 eqidd 2468 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  CC  ->  j  =  j )
415410, 413, 4143eqtrrd 2513 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  CC  ->  j  =  ( ( 2  x.  ( ( j  +  1 )  / 
2 ) )  - 
1 ) )
416405, 415syl 16 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( ( 1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } )  ->  j  =  ( ( 2  x.  ( ( j  +  1 )  / 
2 ) )  - 
1 ) )
417416adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN  /\  j  e.  ( (
1 ... ( ( 2  x.  k )  - 
1 ) )  \  { n  e.  NN  |  ( n  / 
2 )  e.  NN } ) )  -> 
j  =  ( ( 2  x.  ( ( j  +  1 )  /  2 ) )  -  1 ) )
418 oveq2 6303 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  ( ( j  +  1 )  / 
2 )  ->  (
2  x.  m )  =  ( 2  x.  ( ( j  +  1 )  /  2
) ) )
419418oveq1d 6310 . . . . . . . . . . . . . . . . 17  |-  ( m  =  ( ( j  +  1 )  / 
2 )  ->  (
( 2  x.  m
)  -  1 )  =  ( ( 2  x.  ( ( j  +  1 )  / 
2 ) )  - 
1 ) )
420419eqeq2d 2481 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( ( j  +  1 )  / 
2 )  ->  (
j  =  ( ( 2  x.  m )  -  1 )  <->  j  =  ( ( 2  x.  ( ( j  +  1 )  /  2
) )  -  1 ) ) )
421420rspcev 3219 . . . . . . . . . . . . . . 15  |-  ( ( ( ( j  +  1 )  /  2
)  e.  ( 1 ... k )  /\  j  =  ( (
2  x.  ( ( j  +  1 )  /  2 ) )  -  1 ) )  ->  E. m  e.  ( 1 ... k ) j  =  ( ( 2  x.  m )  -  1 ) )
422404, 417, 421syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( 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 ) )
423 eqidd 2468 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) )
424 oveq2 6303 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  m  ->  (
2  x.  i )  =  ( 2  x.  m ) )
425424oveq1d 6310 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  m  ->  (
( 2  x.  i
)  -  1 )  =  ( ( 2  x.  m )  - 
1 ) )
426425adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( m  e.  ( 1 ... k )  /\  j  =  ( ( 2  x.  m
)  -  1 ) )  /\  i  =  m )  ->  (
( 2  x.  i
)  -  1 )  =  ( ( 2  x.  m )  - 
1 ) )
427 simpl 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  e.  ( 1 ... k )  /\  j  =  ( (
2  x.  m )  -  1 ) )  ->  m  e.  ( 1 ... k ) )
428 ovex 6320 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2  x.  m )  -  1 )  e. 
_V
429428a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  e.  ( 1 ... k )  /\  j  =  ( (
2  x.  m )  -  1 ) )  ->  ( ( 2  x.  m )  - 
1 )  e.  _V )
430423, 426, 427, 429fvmptd 5962 . . . . . . . . . . . . . . . . . 18  |-  ( ( m  e.  ( 1 ... k )  /\  j  =  ( (
2  x.  m )  -  1 ) )  ->  ( ( i  e.  ( 1 ... k )  |->  ( ( 2  x.  i )  -  1 ) ) `
 m )  =  ( ( 2  x.  m )  -  1 ) )
431 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  (