Metamath Proof Explorer

Theorem sumnnodd

Description: A series indexed by NN with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses 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 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 sumnnodd.1 
 |-  ( ph -> F : NN --> CC )
2 sumnnodd.even0 
 |-  ( ( ph /\ k e. NN /\ ( k / 2 ) e. NN ) -> ( F ` k ) = 0 )
3 sumnnodd.sc 
 |-  ( ph -> seq 1 ( + , F ) ~~> B )
4 nfv 
 |-  F/ k ph
5 nfcv 
 |-  F/_ k seq 1 ( + , F )
6 nfcv 
 |-  F/_ k 1
7 nfcv 
 |-  F/_ k +
8 nfmpt1 
 |-  F/_ k ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) )
9 6 7 8 nfseq 
 |-  F/_ k seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) )
10 nfmpt1 
 |-  F/_ k ( k e. NN |-> ( ( 2 x. k ) - 1 ) )
11 nnuz 
 |-  NN = ( ZZ>= ` 1 )
12 1zzd 
 |-  ( ph -> 1 e. ZZ )
13 seqex 
 |-  seq 1 ( + , F ) e. _V
14 13 a1i 
 |-  ( ph -> seq 1 ( + , F ) e. _V )
15 1 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )
16 11 12 15 serf 
 |-  ( ph -> seq 1 ( + , F ) : NN --> CC )
17 16 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , F ) ` k ) e. CC )
18 1nn 
 |-  1 e. NN
19 oveq2 
 |-  ( k = 1 -> ( 2 x. k ) = ( 2 x. 1 ) )
20 19 oveq1d 
 |-  ( k = 1 -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. 1 ) - 1 ) )
21 eqid 
 |-  ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) = ( k e. NN |-> ( ( 2 x. k ) - 1 ) )
22 ovex 
 |-  ( ( 2 x. 1 ) - 1 ) e. _V
23 20 21 22 fvmpt 
 |-  ( 1 e. NN -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` 1 ) = ( ( 2 x. 1 ) - 1 ) )
24 18 23 ax-mp 
 |-  ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` 1 ) = ( ( 2 x. 1 ) - 1 )
25 2t1e2 
 |-  ( 2 x. 1 ) = 2
26 25 oveq1i 
 |-  ( ( 2 x. 1 ) - 1 ) = ( 2 - 1 )
27 2m1e1 
 |-  ( 2 - 1 ) = 1
28 24 26 27 3eqtri 
 |-  ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` 1 ) = 1
29 28 18 eqeltri 
 |-  ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` 1 ) e. NN
30 29 a1i 
 |-  ( ph -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` 1 ) e. NN )
31 2z 
 |-  2 e. ZZ
32 31 a1i 
 |-  ( k e. NN -> 2 e. ZZ )
33 nnz 
 |-  ( k e. NN -> k e. ZZ )
34 32 33 zmulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. ZZ )
35 33 peano2zd 
 |-  ( k e. NN -> ( k + 1 ) e. ZZ )
36 32 35 zmulcld 
 |-  ( k e. NN -> ( 2 x. ( k + 1 ) ) e. ZZ )
37 1zzd 
 |-  ( k e. NN -> 1 e. ZZ )
38 36 37 zsubcld 
 |-  ( k e. NN -> ( ( 2 x. ( k + 1 ) ) - 1 ) e. ZZ )
39 2re 
 |-  2 e. RR
40 39 a1i 
 |-  ( k e. NN -> 2 e. RR )
41 nnre 
 |-  ( k e. NN -> k e. RR )
42 40 41 remulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. RR )
43 42 lep1d 
 |-  ( k e. NN -> ( 2 x. k ) <_ ( ( 2 x. k ) + 1 ) )
44 2cnd 
 |-  ( k e. NN -> 2 e. CC )
45 nncn 
 |-  ( k e. NN -> k e. CC )
46 1cnd 
 |-  ( k e. NN -> 1 e. CC )
47 44 45 46 adddid 
 |-  ( k e. NN -> ( 2 x. ( k + 1 ) ) = ( ( 2 x. k ) + ( 2 x. 1 ) ) )
48 25 oveq2i 
 |-  ( ( 2 x. k ) + ( 2 x. 1 ) ) = ( ( 2 x. k ) + 2 )
49 47 48 eqtrdi 
 |-  ( k e. NN -> ( 2 x. ( k + 1 ) ) = ( ( 2 x. k ) + 2 ) )
50 49 oveq1d 
 |-  ( k e. NN -> ( ( 2 x. ( k + 1 ) ) - 1 ) = ( ( ( 2 x. k ) + 2 ) - 1 ) )
51 44 45 mulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. CC )
52 51 44 46 addsubassd 
 |-  ( k e. NN -> ( ( ( 2 x. k ) + 2 ) - 1 ) = ( ( 2 x. k ) + ( 2 - 1 ) ) )
53 27 oveq2i 
 |-  ( ( 2 x. k ) + ( 2 - 1 ) ) = ( ( 2 x. k ) + 1 )
54 53 a1i 
 |-  ( k e. NN -> ( ( 2 x. k ) + ( 2 - 1 ) ) = ( ( 2 x. k ) + 1 ) )
55 50 52 54 3eqtrrd 
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. ( k + 1 ) ) - 1 ) )
56 43 55 breqtrd 
 |-  ( k e. NN -> ( 2 x. k ) <_ ( ( 2 x. ( k + 1 ) ) - 1 ) )
57 eluz2 
 |-  ( ( ( 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 ) ) )
58 34 38 56 57 syl3anbrc 
 |-  ( k e. NN -> ( ( 2 x. ( k + 1 ) ) - 1 ) e. ( ZZ>= ` ( 2 x. k ) ) )
59 oveq2 
 |-  ( k = j -> ( 2 x. k ) = ( 2 x. j ) )
60 59 oveq1d 
 |-  ( k = j -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. j ) - 1 ) )
61 60 cbvmptv 
 |-  ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) = ( j e. NN |-> ( ( 2 x. j ) - 1 ) )
62 oveq2 
 |-  ( j = ( k + 1 ) -> ( 2 x. j ) = ( 2 x. ( k + 1 ) ) )
63 62 oveq1d 
 |-  ( j = ( k + 1 ) -> ( ( 2 x. j ) - 1 ) = ( ( 2 x. ( k + 1 ) ) - 1 ) )
64 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
65 61 63 64 38 fvmptd3 
 |-  ( k e. NN -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` ( k + 1 ) ) = ( ( 2 x. ( k + 1 ) ) - 1 ) )
66 34 37 zsubcld 
 |-  ( k e. NN -> ( ( 2 x. k ) - 1 ) e. ZZ )
67 21 fvmpt2 
 |-  ( ( k e. NN /\ ( ( 2 x. k ) - 1 ) e. ZZ ) -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) = ( ( 2 x. k ) - 1 ) )
68 66 67 mpdan 
 |-  ( k e. NN -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) = ( ( 2 x. k ) - 1 ) )
69 68 oveq1d 
 |-  ( k e. NN -> ( ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) + 1 ) = ( ( ( 2 x. k ) - 1 ) + 1 ) )
70 51 46 npcand 
 |-  ( k e. NN -> ( ( ( 2 x. k ) - 1 ) + 1 ) = ( 2 x. k ) )
71 69 70 eqtrd 
 |-  ( k e. NN -> ( ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) + 1 ) = ( 2 x. k ) )
72 71 fveq2d 
 |-  ( k e. NN -> ( ZZ>= ` ( ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) + 1 ) ) = ( ZZ>= ` ( 2 x. k ) ) )
73 58 65 72 3eltr4d 
 |-  ( k e. NN -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` ( k + 1 ) ) e. ( ZZ>= ` ( ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) + 1 ) ) )
74 73 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` ( k + 1 ) ) e. ( ZZ>= ` ( ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) + 1 ) ) )
75 seqex 
 |-  seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) e. _V
76 75 a1i 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) e. _V )
77 incom 
 |-  ( ( ( 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 } ) )
78 inss2 
 |-  ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) C_ { n e. NN | ( n / 2 ) e. NN }
79 ssrin 
 |-  ( ( ( 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 } ) ) )
80 78 79 ax-mp 
 |-  ( ( ( 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 } ) )
81 77 80 eqsstri 
 |-  ( ( ( 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 } ) )
82 disjdif 
 |-  ( { n e. NN | ( n / 2 ) e. NN } i^i ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) = (/)
83 81 82 sseqtri 
 |-  ( ( ( 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_ (/)
84 ss0 
 |-  ( ( ( ( 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 } ) ) = (/) )
85 83 84 mp1i 
 |-  ( ( 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 } ) ) = (/) )
86 uncom 
 |-  ( ( ( 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 } ) )
87 inundif 
 |-  ( ( ( 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 ) )
88 86 87 eqtr2i 
 |-  ( 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 } ) )
89 88 a1i 
 |-  ( ( 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 } ) ) )
90 fzfid 
 |-  ( ( ph /\ k e. NN ) -> ( 1 ... ( ( 2 x. k ) - 1 ) ) e. Fin )
91 1 adantr 
 |-  ( ( ph /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> F : NN --> CC )
92 elfznn 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> j e. NN )
93 92 adantl 
 |-  ( ( ph /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> j e. NN )
94 91 93 ffvelrnd 
 |-  ( ( ph /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( F ` j ) e. CC )
95 94 adantlr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( F ` j ) e. CC )
96 85 89 90 95 fsumsplit 
 |-  ( ( 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 ) ) )
97 simpl 
 |-  ( ( ph /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) ) -> ph )
98 ssrab2 
 |-  { n e. NN | ( n / 2 ) e. NN } C_ NN
99 78 sseli 
 |-  ( 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 } )
100 98 99 sseldi 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) -> j e. NN )
101 100 adantl 
 |-  ( ( ph /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) ) -> j e. NN )
102 oveq1 
 |-  ( k = j -> ( k / 2 ) = ( j / 2 ) )
103 102 eleq1d 
 |-  ( k = j -> ( ( k / 2 ) e. NN <-> ( j / 2 ) e. NN ) )
104 oveq1 
 |-  ( n = k -> ( n / 2 ) = ( k / 2 ) )
105 104 eleq1d 
 |-  ( n = k -> ( ( n / 2 ) e. NN <-> ( k / 2 ) e. NN ) )
106 105 elrab 
 |-  ( k e. { n e. NN | ( n / 2 ) e. NN } <-> ( k e. NN /\ ( k / 2 ) e. NN ) )
107 106 simprbi 
 |-  ( k e. { n e. NN | ( n / 2 ) e. NN } -> ( k / 2 ) e. NN )
108 103 107 vtoclga 
 |-  ( j e. { n e. NN | ( n / 2 ) e. NN } -> ( j / 2 ) e. NN )
109 99 108 syl 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) -> ( j / 2 ) e. NN )
110 109 adantl 
 |-  ( ( ph /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) ) -> ( j / 2 ) e. NN )
111 eleq1w 
 |-  ( k = j -> ( k e. NN <-> j e. NN ) )
112 111 103 3anbi23d 
 |-  ( k = j -> ( ( ph /\ k e. NN /\ ( k / 2 ) e. NN ) <-> ( ph /\ j e. NN /\ ( j / 2 ) e. NN ) ) )
113 fveqeq2 
 |-  ( k = j -> ( ( F ` k ) = 0 <-> ( F ` j ) = 0 ) )
114 112 113 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. NN /\ ( k / 2 ) e. NN ) -> ( F ` k ) = 0 ) <-> ( ( ph /\ j e. NN /\ ( j / 2 ) e. NN ) -> ( F ` j ) = 0 ) ) )
115 114 2 chvarvv 
 |-  ( ( ph /\ j e. NN /\ ( j / 2 ) e. NN ) -> ( F ` j ) = 0 )
116 97 101 110 115 syl3anc 
 |-  ( ( ph /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) ) -> ( F ` j ) = 0 )
117 116 sumeq2dv 
 |-  ( 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 )
118 fzfid 
 |-  ( ph -> ( 1 ... ( ( 2 x. k ) - 1 ) ) e. Fin )
119 inss1 
 |-  ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) C_ ( 1 ... ( ( 2 x. k ) - 1 ) )
120 119 a1i 
 |-  ( ph -> ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) C_ ( 1 ... ( ( 2 x. k ) - 1 ) ) )
121 ssfi 
 |-  ( ( ( 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 )
122 118 120 121 syl2anc 
 |-  ( ph -> ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) e. Fin )
123 122 olcd 
 |-  ( 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 ) )
124 sumz 
 |-  ( ( ( ( 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 )
125 123 124 syl 
 |-  ( ph -> sum_ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) 0 = 0 )
126 117 125 eqtrd 
 |-  ( ph -> sum_ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) ( F ` j ) = 0 )
127 126 adantr 
 |-  ( ( ph /\ k e. NN ) -> sum_ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) i^i { n e. NN | ( n / 2 ) e. NN } ) ( F ` j ) = 0 )
128 127 oveq2d 
 |-  ( ( 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 ) )
129 fzfi 
 |-  ( 1 ... ( ( 2 x. k ) - 1 ) ) e. Fin
130 difss 
 |-  ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) C_ ( 1 ... ( ( 2 x. k ) - 1 ) )
131 ssfi 
 |-  ( ( ( 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 )
132 129 130 131 mp2an 
 |-  ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) e. Fin
133 132 a1i 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) e. Fin )
134 130 sseli 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) )
135 134 94 sylan2 
 |-  ( ( ph /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> ( F ` j ) e. CC )
136 135 adantlr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> ( F ` j ) e. CC )
137 133 136 fsumcl 
 |-  ( ( ph /\ k e. NN ) -> sum_ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ( F ` j ) e. CC )
138 137 addid1d 
 |-  ( ( 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 ) )
139 fveq2 
 |-  ( j = i -> ( F ` j ) = ( F ` i ) )
140 139 cbvsumv 
 |-  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 )
141 138 140 eqtrdi 
 |-  ( ( 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 ) )
142 128 141 eqtrd 
 |-  ( ( 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 ) )
143 fveq2 
 |-  ( i = ( ( 2 x. j ) - 1 ) -> ( F ` i ) = ( F ` ( ( 2 x. j ) - 1 ) ) )
144 fzfid 
 |-  ( ( ph /\ k e. NN ) -> ( 1 ... k ) e. Fin )
145 1zzd 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> 1 e. ZZ )
146 66 adantr 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( ( 2 x. k ) - 1 ) e. ZZ )
147 31 a1i 
 |-  ( i e. ( 1 ... k ) -> 2 e. ZZ )
148 elfzelz 
 |-  ( i e. ( 1 ... k ) -> i e. ZZ )
149 147 148 zmulcld 
 |-  ( i e. ( 1 ... k ) -> ( 2 x. i ) e. ZZ )
150 1zzd 
 |-  ( i e. ( 1 ... k ) -> 1 e. ZZ )
151 149 150 zsubcld 
 |-  ( i e. ( 1 ... k ) -> ( ( 2 x. i ) - 1 ) e. ZZ )
152 151 adantl 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( ( 2 x. i ) - 1 ) e. ZZ )
153 145 146 152 3jca 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( 1 e. ZZ /\ ( ( 2 x. k ) - 1 ) e. ZZ /\ ( ( 2 x. i ) - 1 ) e. ZZ ) )
154 26 27 eqtr2i 
 |-  1 = ( ( 2 x. 1 ) - 1 )
155 1re 
 |-  1 e. RR
156 39 155 remulcli 
 |-  ( 2 x. 1 ) e. RR
157 156 a1i 
 |-  ( i e. ( 1 ... k ) -> ( 2 x. 1 ) e. RR )
158 149 zred 
 |-  ( i e. ( 1 ... k ) -> ( 2 x. i ) e. RR )
159 1red 
 |-  ( i e. ( 1 ... k ) -> 1 e. RR )
160 148 zred 
 |-  ( i e. ( 1 ... k ) -> i e. RR )
161 39 a1i 
 |-  ( i e. ( 1 ... k ) -> 2 e. RR )
162 0le2 
 |-  0 <_ 2
163 162 a1i 
 |-  ( i e. ( 1 ... k ) -> 0 <_ 2 )
164 elfzle1 
 |-  ( i e. ( 1 ... k ) -> 1 <_ i )
165 159 160 161 163 164 lemul2ad 
 |-  ( i e. ( 1 ... k ) -> ( 2 x. 1 ) <_ ( 2 x. i ) )
166 157 158 159 165 lesub1dd 
 |-  ( i e. ( 1 ... k ) -> ( ( 2 x. 1 ) - 1 ) <_ ( ( 2 x. i ) - 1 ) )
167 154 166 eqbrtrid 
 |-  ( i e. ( 1 ... k ) -> 1 <_ ( ( 2 x. i ) - 1 ) )
168 167 adantl 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> 1 <_ ( ( 2 x. i ) - 1 ) )
169 158 adantl 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( 2 x. i ) e. RR )
170 42 adantr 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( 2 x. k ) e. RR )
171 1red 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> 1 e. RR )
172 160 adantl 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> i e. RR )
173 41 adantr 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> k e. RR )
174 39 a1i 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> 2 e. RR )
175 162 a1i 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> 0 <_ 2 )
176 elfzle2 
 |-  ( i e. ( 1 ... k ) -> i <_ k )
177 176 adantl 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> i <_ k )
178 172 173 174 175 177 lemul2ad 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( 2 x. i ) <_ ( 2 x. k ) )
179 169 170 171 178 lesub1dd 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( ( 2 x. i ) - 1 ) <_ ( ( 2 x. k ) - 1 ) )
180 168 179 jca 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( 1 <_ ( ( 2 x. i ) - 1 ) /\ ( ( 2 x. i ) - 1 ) <_ ( ( 2 x. k ) - 1 ) ) )
181 elfz2 
 |-  ( ( ( 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 ) ) ) )
182 153 180 181 sylanbrc 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( ( 2 x. i ) - 1 ) e. ( 1 ... ( ( 2 x. k ) - 1 ) ) )
183 149 zcnd 
 |-  ( i e. ( 1 ... k ) -> ( 2 x. i ) e. CC )
184 1cnd 
 |-  ( i e. ( 1 ... k ) -> 1 e. CC )
185 2cnd 
 |-  ( i e. ( 1 ... k ) -> 2 e. CC )
186 2ne0 
 |-  2 =/= 0
187 186 a1i 
 |-  ( i e. ( 1 ... k ) -> 2 =/= 0 )
188 183 184 185 187 divsubdird 
 |-  ( i e. ( 1 ... k ) -> ( ( ( 2 x. i ) - 1 ) / 2 ) = ( ( ( 2 x. i ) / 2 ) - ( 1 / 2 ) ) )
189 148 zcnd 
 |-  ( i e. ( 1 ... k ) -> i e. CC )
190 189 185 187 divcan3d 
 |-  ( i e. ( 1 ... k ) -> ( ( 2 x. i ) / 2 ) = i )
191 190 oveq1d 
 |-  ( i e. ( 1 ... k ) -> ( ( ( 2 x. i ) / 2 ) - ( 1 / 2 ) ) = ( i - ( 1 / 2 ) ) )
192 188 191 eqtrd 
 |-  ( i e. ( 1 ... k ) -> ( ( ( 2 x. i ) - 1 ) / 2 ) = ( i - ( 1 / 2 ) ) )
193 148 150 zsubcld 
 |-  ( i e. ( 1 ... k ) -> ( i - 1 ) e. ZZ )
194 161 187 rereccld 
 |-  ( i e. ( 1 ... k ) -> ( 1 / 2 ) e. RR )
195 halflt1 
 |-  ( 1 / 2 ) < 1
196 195 a1i 
 |-  ( i e. ( 1 ... k ) -> ( 1 / 2 ) < 1 )
197 194 159 160 196 ltsub2dd 
 |-  ( i e. ( 1 ... k ) -> ( i - 1 ) < ( i - ( 1 / 2 ) ) )
198 2rp 
 |-  2 e. RR+
199 rpreccl 
 |-  ( 2 e. RR+ -> ( 1 / 2 ) e. RR+ )
200 198 199 mp1i 
 |-  ( i e. ( 1 ... k ) -> ( 1 / 2 ) e. RR+ )
201 160 200 ltsubrpd 
 |-  ( i e. ( 1 ... k ) -> ( i - ( 1 / 2 ) ) < i )
202 189 184 npcand 
 |-  ( i e. ( 1 ... k ) -> ( ( i - 1 ) + 1 ) = i )
203 201 202 breqtrrd 
 |-  ( i e. ( 1 ... k ) -> ( i - ( 1 / 2 ) ) < ( ( i - 1 ) + 1 ) )
204 btwnnz 
 |-  ( ( ( i - 1 ) e. ZZ /\ ( i - 1 ) < ( i - ( 1 / 2 ) ) /\ ( i - ( 1 / 2 ) ) < ( ( i - 1 ) + 1 ) ) -> -. ( i - ( 1 / 2 ) ) e. ZZ )
205 193 197 203 204 syl3anc 
 |-  ( i e. ( 1 ... k ) -> -. ( i - ( 1 / 2 ) ) e. ZZ )
206 nnz 
 |-  ( ( i - ( 1 / 2 ) ) e. NN -> ( i - ( 1 / 2 ) ) e. ZZ )
207 205 206 nsyl 
 |-  ( i e. ( 1 ... k ) -> -. ( i - ( 1 / 2 ) ) e. NN )
208 192 207 eqneltrd 
 |-  ( i e. ( 1 ... k ) -> -. ( ( ( 2 x. i ) - 1 ) / 2 ) e. NN )
209 208 intnand 
 |-  ( i e. ( 1 ... k ) -> -. ( ( ( 2 x. i ) - 1 ) e. NN /\ ( ( ( 2 x. i ) - 1 ) / 2 ) e. NN ) )
210 oveq1 
 |-  ( n = ( ( 2 x. i ) - 1 ) -> ( n / 2 ) = ( ( ( 2 x. i ) - 1 ) / 2 ) )
211 210 eleq1d 
 |-  ( n = ( ( 2 x. i ) - 1 ) -> ( ( n / 2 ) e. NN <-> ( ( ( 2 x. i ) - 1 ) / 2 ) e. NN ) )
212 211 elrab 
 |-  ( ( ( 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 ) )
213 209 212 sylnibr 
 |-  ( i e. ( 1 ... k ) -> -. ( ( 2 x. i ) - 1 ) e. { n e. NN | ( n / 2 ) e. NN } )
214 213 adantl 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> -. ( ( 2 x. i ) - 1 ) e. { n e. NN | ( n / 2 ) e. NN } )
215 182 214 eldifd 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( ( 2 x. i ) - 1 ) e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) )
216 215 fmpttd 
 |-  ( 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 } ) )
217 eqidd 
 |-  ( x e. ( 1 ... k ) -> ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) = ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) )
218 oveq2 
 |-  ( i = x -> ( 2 x. i ) = ( 2 x. x ) )
219 218 oveq1d 
 |-  ( i = x -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. x ) - 1 ) )
220 219 adantl 
 |-  ( ( x e. ( 1 ... k ) /\ i = x ) -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. x ) - 1 ) )
221 id 
 |-  ( x e. ( 1 ... k ) -> x e. ( 1 ... k ) )
222 ovexd 
 |-  ( x e. ( 1 ... k ) -> ( ( 2 x. x ) - 1 ) e. _V )
223 217 220 221 222 fvmptd 
 |-  ( x e. ( 1 ... k ) -> ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` x ) = ( ( 2 x. x ) - 1 ) )
224 223 eqcomd 
 |-  ( x e. ( 1 ... k ) -> ( ( 2 x. x ) - 1 ) = ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` x ) )
225 224 ad2antrr 
 |-  ( ( ( 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 ) )
226 simpr 
 |-  ( ( ( 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 ) )
227 eqidd 
 |-  ( y e. ( 1 ... k ) -> ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) = ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) )
228 oveq2 
 |-  ( i = y -> ( 2 x. i ) = ( 2 x. y ) )
229 228 oveq1d 
 |-  ( i = y -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. y ) - 1 ) )
230 229 adantl 
 |-  ( ( y e. ( 1 ... k ) /\ i = y ) -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. y ) - 1 ) )
231 id 
 |-  ( y e. ( 1 ... k ) -> y e. ( 1 ... k ) )
232 ovexd 
 |-  ( y e. ( 1 ... k ) -> ( ( 2 x. y ) - 1 ) e. _V )
233 227 230 231 232 fvmptd 
 |-  ( y e. ( 1 ... k ) -> ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` y ) = ( ( 2 x. y ) - 1 ) )
234 233 ad2antlr 
 |-  ( ( ( 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 ) )
235 225 226 234 3eqtrd 
 |-  ( ( ( 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 ) )
236 2cnd 
 |-  ( x e. ( 1 ... k ) -> 2 e. CC )
237 elfzelz 
 |-  ( x e. ( 1 ... k ) -> x e. ZZ )
238 237 zcnd 
 |-  ( x e. ( 1 ... k ) -> x e. CC )
239 236 238 mulcld 
 |-  ( x e. ( 1 ... k ) -> ( 2 x. x ) e. CC )
240 239 ad2antrr 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) ) -> ( 2 x. x ) e. CC )
241 2cnd 
 |-  ( y e. ( 1 ... k ) -> 2 e. CC )
242 elfzelz 
 |-  ( y e. ( 1 ... k ) -> y e. ZZ )
243 242 zcnd 
 |-  ( y e. ( 1 ... k ) -> y e. CC )
244 241 243 mulcld 
 |-  ( y e. ( 1 ... k ) -> ( 2 x. y ) e. CC )
245 244 ad2antlr 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) ) -> ( 2 x. y ) e. CC )
246 1cnd 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) ) -> 1 e. CC )
247 simpr 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) ) -> ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) )
248 240 245 246 247 subcan2d 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) ) -> ( 2 x. x ) = ( 2 x. y ) )
249 238 ad2antrr 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> x e. CC )
250 243 ad2antlr 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> y e. CC )
251 2cnd 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> 2 e. CC )
252 186 a1i 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> 2 =/= 0 )
253 simpr 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> ( 2 x. x ) = ( 2 x. y ) )
254 249 250 251 252 253 mulcanad 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> x = y )
255 248 254 syldan 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) ) -> x = y )
256 235 255 syldan 
 |-  ( ( ( 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 )
257 256 adantll 
 |-  ( ( ( 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 )
258 257 ex 
 |-  ( ( 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 ) )
259 258 ralrimivva 
 |-  ( 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 ) )
260 dff13 
 |-  ( ( 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 ) ) )
261 216 259 260 sylanbrc 
 |-  ( 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 } ) )
262 1zzd 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> 1 e. ZZ )
263 33 adantr 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> k e. ZZ )
264 fzssz 
 |-  ( 1 ... ( ( 2 x. k ) - 1 ) ) C_ ZZ
265 264 134 sseldi 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> j e. ZZ )
266 zeo 
 |-  ( j e. ZZ -> ( ( j / 2 ) e. ZZ \/ ( ( j + 1 ) / 2 ) e. ZZ ) )
267 265 266 syl 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> ( ( j / 2 ) e. ZZ \/ ( ( j + 1 ) / 2 ) e. ZZ ) )
268 267 adantl 
 |-  ( ( 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 ) )
269 eldifn 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> -. j e. { n e. NN | ( n / 2 ) e. NN } )
270 134 92 syl 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> j e. NN )
271 270 adantr 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> j e. NN )
272 simpr 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> ( j / 2 ) e. ZZ )
273 271 nnred 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> j e. RR )
274 39 a1i 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> 2 e. RR )
275 271 nngt0d 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> 0 < j )
276 2pos 
 |-  0 < 2
277 276 a1i 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> 0 < 2 )
278 273 274 275 277 divgt0d 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> 0 < ( j / 2 ) )
279 elnnz 
 |-  ( ( j / 2 ) e. NN <-> ( ( j / 2 ) e. ZZ /\ 0 < ( j / 2 ) ) )
280 272 278 279 sylanbrc 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> ( j / 2 ) e. NN )
281 oveq1 
 |-  ( n = j -> ( n / 2 ) = ( j / 2 ) )
282 281 eleq1d 
 |-  ( n = j -> ( ( n / 2 ) e. NN <-> ( j / 2 ) e. NN ) )
283 282 elrab 
 |-  ( j e. { n e. NN | ( n / 2 ) e. NN } <-> ( j e. NN /\ ( j / 2 ) e. NN ) )
284 271 280 283 sylanbrc 
 |-  ( ( 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 } )
285 269 284 mtand 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> -. ( j / 2 ) e. ZZ )
286 285 adantl 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> -. ( j / 2 ) e. ZZ )
287 pm2.53 
 |-  ( ( ( j / 2 ) e. ZZ \/ ( ( j + 1 ) / 2 ) e. ZZ ) -> ( -. ( j / 2 ) e. ZZ -> ( ( j + 1 ) / 2 ) e. ZZ ) )
288 268 286 287 sylc 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> ( ( j + 1 ) / 2 ) e. ZZ )
289 262 263 288 3jca 
 |-  ( ( 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 ) )
290 1p1e2 
 |-  ( 1 + 1 ) = 2
291 290 oveq1i 
 |-  ( ( 1 + 1 ) / 2 ) = ( 2 / 2 )
292 2div2e1 
 |-  ( 2 / 2 ) = 1
293 291 292 eqtr2i 
 |-  1 = ( ( 1 + 1 ) / 2 )
294 1red 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> 1 e. RR )
295 294 294 readdcld 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( 1 + 1 ) e. RR )
296 92 nnred 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> j e. RR )
297 296 294 readdcld 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( j + 1 ) e. RR )
298 198 a1i 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> 2 e. RR+ )
299 elfzle1 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> 1 <_ j )
300 294 296 294 299 leadd1dd 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( 1 + 1 ) <_ ( j + 1 ) )
301 295 297 298 300 lediv1dd 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( ( 1 + 1 ) / 2 ) <_ ( ( j + 1 ) / 2 ) )
302 293 301 eqbrtrid 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> 1 <_ ( ( j + 1 ) / 2 ) )
303 134 302 syl 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> 1 <_ ( ( j + 1 ) / 2 ) )
304 303 adantl 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> 1 <_ ( ( j + 1 ) / 2 ) )
305 elfzel2 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( ( 2 x. k ) - 1 ) e. ZZ )
306 305 zred 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( ( 2 x. k ) - 1 ) e. RR )
307 306 294 readdcld 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( ( ( 2 x. k ) - 1 ) + 1 ) e. RR )
308 elfzle2 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> j <_ ( ( 2 x. k ) - 1 ) )
309 296 306 294 308 leadd1dd 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( j + 1 ) <_ ( ( ( 2 x. k ) - 1 ) + 1 ) )
310 297 307 298 309 lediv1dd 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( ( j + 1 ) / 2 ) <_ ( ( ( ( 2 x. k ) - 1 ) + 1 ) / 2 ) )
311 310 adantl 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( j + 1 ) / 2 ) <_ ( ( ( ( 2 x. k ) - 1 ) + 1 ) / 2 ) )
312 51 adantr 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( 2 x. k ) e. CC )
313 1cnd 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> 1 e. CC )
314 312 313 npcand 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( ( 2 x. k ) - 1 ) + 1 ) = ( 2 x. k ) )
315 314 oveq1d 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( ( ( 2 x. k ) - 1 ) + 1 ) / 2 ) = ( ( 2 x. k ) / 2 ) )
316 186 a1i 
 |-  ( k e. NN -> 2 =/= 0 )
317 45 44 316 divcan3d 
 |-  ( k e. NN -> ( ( 2 x. k ) / 2 ) = k )
318 317 adantr 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( 2 x. k ) / 2 ) = k )
319 315 318 eqtrd 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( ( ( 2 x. k ) - 1 ) + 1 ) / 2 ) = k )
320 311 319 breqtrd 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( j + 1 ) / 2 ) <_ k )
321 134 320 sylan2 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> ( ( j + 1 ) / 2 ) <_ k )
322 289 304 321 jca32 
 |-  ( ( 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 ) ) )
323 elfz2 
 |-  ( ( ( 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 ) ) )
324 322 323 sylibr 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> ( ( j + 1 ) / 2 ) e. ( 1 ... k ) )
325 270 nncnd 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> j e. CC )
326 peano2cn 
 |-  ( j e. CC -> ( j + 1 ) e. CC )
327 2cnd 
 |-  ( j e. CC -> 2 e. CC )
328 186 a1i 
 |-  ( j e. CC -> 2 =/= 0 )
329 326 327 328 divcan2d 
 |-  ( j e. CC -> ( 2 x. ( ( j + 1 ) / 2 ) ) = ( j + 1 ) )
330 329 oveq1d 
 |-  ( j e. CC -> ( ( 2 x. ( ( j + 1 ) / 2 ) ) - 1 ) = ( ( j + 1 ) - 1 ) )
331 pncan1 
 |-  ( j e. CC -> ( ( j + 1 ) - 1 ) = j )
332 330 331 eqtr2d 
 |-  ( j e. CC -> j = ( ( 2 x. ( ( j + 1 ) / 2 ) ) - 1 ) )
333 325 332 syl 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> j = ( ( 2 x. ( ( j + 1 ) / 2 ) ) - 1 ) )
334 333 adantl 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> j = ( ( 2 x. ( ( j + 1 ) / 2 ) ) - 1 ) )
335 oveq2 
 |-  ( m = ( ( j + 1 ) / 2 ) -> ( 2 x. m ) = ( 2 x. ( ( j + 1 ) / 2 ) ) )
336 335 oveq1d 
 |-  ( m = ( ( j + 1 ) / 2 ) -> ( ( 2 x. m ) - 1 ) = ( ( 2 x. ( ( j + 1 ) / 2 ) ) - 1 ) )
337 336 rspceeqv 
 |-  ( ( ( ( j + 1 ) / 2 ) e. ( 1 ... k ) /\ j = ( ( 2 x. ( ( j + 1 ) / 2 ) ) - 1 ) ) -> E. m e. ( 1 ... k ) j = ( ( 2 x. m ) - 1 ) )
338 324 334 337 syl2anc 
 |-  ( ( 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 ) )
339 eqidd 
 |-  ( ( 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 ) ) )
340 oveq2 
 |-  ( i = m -> ( 2 x. i ) = ( 2 x. m ) )
341 340 oveq1d 
 |-  ( i = m -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. m ) - 1 ) )
342 341 adantl 
 |-  ( ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) /\ i = m ) -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. m ) - 1 ) )
343 simpl 
 |-  ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) -> m e. ( 1 ... k ) )
344 ovexd 
 |-  ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) -> ( ( 2 x. m ) - 1 ) e. _V )
345 339 342 343 344 fvmptd 
 |-  ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) -> ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` m ) = ( ( 2 x. m ) - 1 ) )
346 id 
 |-  ( j = ( ( 2 x. m ) - 1 ) -> j = ( ( 2 x. m ) - 1 ) )
347 346 eqcomd 
 |-  ( j = ( ( 2 x. m ) - 1 ) -> ( ( 2 x. m ) - 1 ) = j )
348 347 adantl 
 |-  ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) -> ( ( 2 x. m ) - 1 ) = j )
349 345 348 eqtr2d 
 |-  ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) -> j = ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` m ) )
350 349 ex 
 |-  ( m e. ( 1 ... k ) -> ( j = ( ( 2 x. m ) - 1 ) -> j = ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` m ) ) )
351 350 adantl 
 |-  ( ( ( 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 ) ) )
352 351 reximdva 
 |-  ( ( 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 ) ) )
353 338 352 mpd 
 |-  ( ( 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 ) )
354 353 ralrimiva 
 |-  ( 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 ) )
355 dffo3 
 |-  ( ( 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 ) ) )
356 216 354 355 sylanbrc 
 |-  ( 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 } ) )
357 df-f1o 
 |-  ( ( 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 } ) ) )
358 261 356 357 sylanbrc 
 |-  ( 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 } ) )
359 358 adantl 
 |-  ( ( 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 } ) )
360 eqidd 
 |-  ( j e. ( 1 ... k ) -> ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) = ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) )
361 oveq2 
 |-  ( i = j -> ( 2 x. i ) = ( 2 x. j ) )
362 361 oveq1d 
 |-  ( i = j -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. j ) - 1 ) )
363 362 adantl 
 |-  ( ( j e. ( 1 ... k ) /\ i = j ) -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. j ) - 1 ) )
364 id 
 |-  ( j e. ( 1 ... k ) -> j e. ( 1 ... k ) )
365 ovexd 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. j ) - 1 ) e. _V )
366 360 363 364 365 fvmptd 
 |-  ( j e. ( 1 ... k ) -> ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` j ) = ( ( 2 x. j ) - 1 ) )
367 366 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` j ) = ( ( 2 x. j ) - 1 ) )
368 eleq1w 
 |-  ( 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 } ) ) )
369 368 anbi2d 
 |-  ( 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 } ) ) ) )
370 139 eleq1d 
 |-  ( j = i -> ( ( F ` j ) e. CC <-> ( F ` i ) e. CC ) )
371 369 370 imbi12d 
 |-  ( 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 ) ) )
372 371 136 chvarvv 
 |-  ( ( ( ph /\ k e. NN ) /\ i e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> ( F ` i ) e. CC )
373 143 144 359 367 372 fsumf1o 
 |-  ( ( 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 ) ) )
374 96 142 373 3eqtrrd 
 |-  ( ( ph /\ k e. NN ) -> sum_ j e. ( 1 ... k ) ( F ` ( ( 2 x. j ) - 1 ) ) = sum_ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ( F ` j ) )
375 ovex 
 |-  ( ( 2 x. k ) - 1 ) e. _V
376 21 fvmpt2 
 |-  ( ( k e. NN /\ ( ( 2 x. k ) - 1 ) e. _V ) -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) = ( ( 2 x. k ) - 1 ) )
377 375 376 mpan2 
 |-  ( k e. NN -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) = ( ( 2 x. k ) - 1 ) )
378 377 oveq2d 
 |-  ( k e. NN -> ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) = ( 1 ... ( ( 2 x. k ) - 1 ) ) )
379 378 eqcomd 
 |-  ( k e. NN -> ( 1 ... ( ( 2 x. k ) - 1 ) ) = ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) )
380 379 sumeq1d 
 |-  ( 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 ) )
381 380 adantl 
 |-  ( ( 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 ) )
382 374 381 eqtrd 
 |-  ( ( 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 ) )
383 elfznn 
 |-  ( j e. ( 1 ... k ) -> j e. NN )
384 383 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> j e. NN )
385 1 adantr 
 |-  ( ( ph /\ j e. ( 1 ... k ) ) -> F : NN --> CC )
386 31 a1i 
 |-  ( j e. ( 1 ... k ) -> 2 e. ZZ )
387 elfzelz 
 |-  ( j e. ( 1 ... k ) -> j e. ZZ )
388 386 387 zmulcld 
 |-  ( j e. ( 1 ... k ) -> ( 2 x. j ) e. ZZ )
389 1zzd 
 |-  ( j e. ( 1 ... k ) -> 1 e. ZZ )
390 388 389 zsubcld 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. j ) - 1 ) e. ZZ )
391 0red 
 |-  ( j e. ( 1 ... k ) -> 0 e. RR )
392 39 a1i 
 |-  ( j e. ( 1 ... k ) -> 2 e. RR )
393 25 392 eqeltrid 
 |-  ( j e. ( 1 ... k ) -> ( 2 x. 1 ) e. RR )
394 1red 
 |-  ( j e. ( 1 ... k ) -> 1 e. RR )
395 393 394 resubcld 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. 1 ) - 1 ) e. RR )
396 390 zred 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. j ) - 1 ) e. RR )
397 0lt1 
 |-  0 < 1
398 154 a1i 
 |-  ( j e. ( 1 ... k ) -> 1 = ( ( 2 x. 1 ) - 1 ) )
399 397 398 breqtrid 
 |-  ( j e. ( 1 ... k ) -> 0 < ( ( 2 x. 1 ) - 1 ) )
400 388 zred 
 |-  ( j e. ( 1 ... k ) -> ( 2 x. j ) e. RR )
401 383 nnred 
 |-  ( j e. ( 1 ... k ) -> j e. RR )
402 162 a1i 
 |-  ( j e. ( 1 ... k ) -> 0 <_ 2 )
403 elfzle1 
 |-  ( j e. ( 1 ... k ) -> 1 <_ j )
404 394 401 392 402 403 lemul2ad 
 |-  ( j e. ( 1 ... k ) -> ( 2 x. 1 ) <_ ( 2 x. j ) )
405 393 400 394 404 lesub1dd 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. 1 ) - 1 ) <_ ( ( 2 x. j ) - 1 ) )
406 391 395 396 399 405 ltletrd 
 |-  ( j e. ( 1 ... k ) -> 0 < ( ( 2 x. j ) - 1 ) )
407 elnnz 
 |-  ( ( ( 2 x. j ) - 1 ) e. NN <-> ( ( ( 2 x. j ) - 1 ) e. ZZ /\ 0 < ( ( 2 x. j ) - 1 ) ) )
408 390 406 407 sylanbrc 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. j ) - 1 ) e. NN )
409 408 adantl 
 |-  ( ( ph /\ j e. ( 1 ... k ) ) -> ( ( 2 x. j ) - 1 ) e. NN )
410 385 409 ffvelrnd 
 |-  ( ( ph /\ j e. ( 1 ... k ) ) -> ( F ` ( ( 2 x. j ) - 1 ) ) e. CC )
411 410 adantlr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( F ` ( ( 2 x. j ) - 1 ) ) e. CC )
412 60 fveq2d 
 |-  ( k = j -> ( F ` ( ( 2 x. k ) - 1 ) ) = ( F ` ( ( 2 x. j ) - 1 ) ) )
413 412 cbvmptv 
 |-  ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) = ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) )
414 413 fvmpt2 
 |-  ( ( j e. NN /\ ( F ` ( ( 2 x. j ) - 1 ) ) e. CC ) -> ( ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ` j ) = ( F ` ( ( 2 x. j ) - 1 ) ) )
415 384 411 414 syl2anc 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ` j ) = ( F ` ( ( 2 x. j ) - 1 ) ) )
416 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
417 416 11 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
418 415 417 411 fsumser 
 |-  ( ( 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 ) )
419 eqidd 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> ( F ` j ) = ( F ` j ) )
420 156 a1i 
 |-  ( k e. NN -> ( 2 x. 1 ) e. RR )
421 1red 
 |-  ( k e. NN -> 1 e. RR )
422 162 a1i 
 |-  ( k e. NN -> 0 <_ 2 )
423 nnge1 
 |-  ( k e. NN -> 1 <_ k )
424 421 41 40 422 423 lemul2ad 
 |-  ( k e. NN -> ( 2 x. 1 ) <_ ( 2 x. k ) )
425 420 42 421 424 lesub1dd 
 |-  ( k e. NN -> ( ( 2 x. 1 ) - 1 ) <_ ( ( 2 x. k ) - 1 ) )
426 154 425 eqbrtrid 
 |-  ( k e. NN -> 1 <_ ( ( 2 x. k ) - 1 ) )
427 eluz2 
 |-  ( ( ( 2 x. k ) - 1 ) e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ ( ( 2 x. k ) - 1 ) e. ZZ /\ 1 <_ ( ( 2 x. k ) - 1 ) ) )
428 37 66 426 427 syl3anbrc 
 |-  ( k e. NN -> ( ( 2 x. k ) - 1 ) e. ( ZZ>= ` 1 ) )
429 68 428 eqeltrd 
 |-  ( k e. NN -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) e. ( ZZ>= ` 1 ) )
430 429 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) e. ( ZZ>= ` 1 ) )
431 simpll 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> ph )
432 simpr 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) )
433 378 adantr 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) = ( 1 ... ( ( 2 x. k ) - 1 ) ) )
434 432 433 eleqtrd 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) )
435 434 adantll 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) )
436 431 435 94 syl2anc 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> ( F ` j ) e. CC )
437 419 430 436 fsumser 
 |-  ( ( ph /\ k e. NN ) -> sum_ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ( F ` j ) = ( seq 1 ( + , F ) ` ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) )
438 382 418 437 3eqtr3d 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ` k ) = ( seq 1 ( + , F ) ` ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) )
439 4 5 9 10 11 12 14 17 3 30 74 76 438 climsuse 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> B )
440 eqidd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
441 11 12 440 15 isum 
 |-  ( ph -> sum_ k e. NN ( F ` k ) = ( ~~> ` seq 1 ( + , F ) ) )
442 climrel 
 |-  Rel ~~>
443 442 releldmi 
 |-  ( seq 1 ( + , F ) ~~> B -> seq 1 ( + , F ) e. dom ~~> )
444 3 443 syl 
 |-  ( ph -> seq 1 ( + , F ) e. dom ~~> )
445 climdm 
 |-  ( seq 1 ( + , F ) e. dom ~~> <-> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
446 444 445 sylib 
 |-  ( ph -> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
447 climuni 
 |-  ( ( seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) /\ seq 1 ( + , F ) ~~> B ) -> ( ~~> ` seq 1 ( + , F ) ) = B )
448 446 3 447 syl2anc 
 |-  ( ph -> ( ~~> ` seq 1 ( + , F ) ) = B )
449 442 a1i 
 |-  ( ph -> Rel ~~> )
450 releldm 
 |-  ( ( Rel ~~> /\ seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> B ) -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) e. dom ~~> )
451 449 439 450 syl2anc 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) e. dom ~~> )
452 climdm 
 |-  ( seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) e. dom ~~> <-> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> ( ~~> ` seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ) )
453 451 452 sylib 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> ( ~~> ` seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ) )
454 413 a1i 
 |-  ( ph -> ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) = ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) )
455 454 seqeq3d 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) = seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) )
456 455 fveq2d 
 |-  ( ph -> ( ~~> ` seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ) = ( ~~> ` seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) ) )
457 453 456 breqtrd 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> ( ~~> ` seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) ) )
458 climuni 
 |-  ( ( seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> B /\ seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> ( ~~> ` seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) ) ) -> B = ( ~~> ` seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) ) )
459 439 457 458 syl2anc 
 |-  ( ph -> B = ( ~~> ` seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) ) )
460 eqidd 
 |-  ( ( ph /\ k e. NN ) -> ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) = ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) )
461 eqcom 
 |-  ( k = j <-> j = k )
462 eqcom 
 |-  ( ( F ` ( ( 2 x. k ) - 1 ) ) = ( F ` ( ( 2 x. j ) - 1 ) ) <-> ( F ` ( ( 2 x. j ) - 1 ) ) = ( F ` ( ( 2 x. k ) - 1 ) ) )
463 412 461 462 3imtr3i 
 |-  ( j = k -> ( F ` ( ( 2 x. j ) - 1 ) ) = ( F ` ( ( 2 x. k ) - 1 ) ) )
464 463 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ j = k ) -> ( F ` ( ( 2 x. j ) - 1 ) ) = ( F ` ( ( 2 x. k ) - 1 ) ) )
465 1 adantr 
 |-  ( ( ph /\ k e. NN ) -> F : NN --> CC )
466 428 11 eleqtrrdi 
 |-  ( k e. NN -> ( ( 2 x. k ) - 1 ) e. NN )
467 466 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2 x. k ) - 1 ) e. NN )
468 465 467 ffvelrnd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( ( 2 x. k ) - 1 ) ) e. CC )
469 460 464 416 468 fvmptd 
 |-  ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ` k ) = ( F ` ( ( 2 x. k ) - 1 ) ) )
470 11 12 469 468 isum 
 |-  ( ph -> sum_ k e. NN ( F ` ( ( 2 x. k ) - 1 ) ) = ( ~~> ` seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) ) )
471 459 470 eqtr4d 
 |-  ( ph -> B = sum_ k e. NN ( F ` ( ( 2 x. k ) - 1 ) ) )
472 441 448 471 3eqtrd 
 |-  ( ph -> sum_ k e. NN ( F ` k ) = sum_ k e. NN ( F ` ( ( 2 x. k ) - 1 ) ) )
473 439 472 jca 
 |-  ( 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 ) ) ) )