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 sselid 
 |-  ( 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 26 27 eqtr2i 
 |-  1 = ( ( 2 x. 1 ) - 1 )
154 1re 
 |-  1 e. RR
155 39 154 remulcli 
 |-  ( 2 x. 1 ) e. RR
156 155 a1i 
 |-  ( i e. ( 1 ... k ) -> ( 2 x. 1 ) e. RR )
157 149 zred 
 |-  ( i e. ( 1 ... k ) -> ( 2 x. i ) e. RR )
158 1red 
 |-  ( i e. ( 1 ... k ) -> 1 e. RR )
159 148 zred 
 |-  ( i e. ( 1 ... k ) -> i e. RR )
160 39 a1i 
 |-  ( i e. ( 1 ... k ) -> 2 e. RR )
161 0le2 
 |-  0 <_ 2
162 161 a1i 
 |-  ( i e. ( 1 ... k ) -> 0 <_ 2 )
163 elfzle1 
 |-  ( i e. ( 1 ... k ) -> 1 <_ i )
164 158 159 160 162 163 lemul2ad 
 |-  ( i e. ( 1 ... k ) -> ( 2 x. 1 ) <_ ( 2 x. i ) )
165 156 157 158 164 lesub1dd 
 |-  ( i e. ( 1 ... k ) -> ( ( 2 x. 1 ) - 1 ) <_ ( ( 2 x. i ) - 1 ) )
166 153 165 eqbrtrid 
 |-  ( i e. ( 1 ... k ) -> 1 <_ ( ( 2 x. i ) - 1 ) )
167 166 adantl 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> 1 <_ ( ( 2 x. i ) - 1 ) )
168 157 adantl 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( 2 x. i ) e. RR )
169 42 adantr 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( 2 x. k ) e. RR )
170 1red 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> 1 e. RR )
171 159 adantl 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> i e. RR )
172 41 adantr 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> k e. RR )
173 39 a1i 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> 2 e. RR )
174 161 a1i 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> 0 <_ 2 )
175 elfzle2 
 |-  ( i e. ( 1 ... k ) -> i <_ k )
176 175 adantl 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> i <_ k )
177 171 172 173 174 176 lemul2ad 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( 2 x. i ) <_ ( 2 x. k ) )
178 168 169 170 177 lesub1dd 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( ( 2 x. i ) - 1 ) <_ ( ( 2 x. k ) - 1 ) )
179 145 146 152 167 178 elfzd 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> ( ( 2 x. i ) - 1 ) e. ( 1 ... ( ( 2 x. k ) - 1 ) ) )
180 149 zcnd 
 |-  ( i e. ( 1 ... k ) -> ( 2 x. i ) e. CC )
181 1cnd 
 |-  ( i e. ( 1 ... k ) -> 1 e. CC )
182 2cnd 
 |-  ( i e. ( 1 ... k ) -> 2 e. CC )
183 2ne0 
 |-  2 =/= 0
184 183 a1i 
 |-  ( i e. ( 1 ... k ) -> 2 =/= 0 )
185 180 181 182 184 divsubdird 
 |-  ( i e. ( 1 ... k ) -> ( ( ( 2 x. i ) - 1 ) / 2 ) = ( ( ( 2 x. i ) / 2 ) - ( 1 / 2 ) ) )
186 148 zcnd 
 |-  ( i e. ( 1 ... k ) -> i e. CC )
187 186 182 184 divcan3d 
 |-  ( i e. ( 1 ... k ) -> ( ( 2 x. i ) / 2 ) = i )
188 187 oveq1d 
 |-  ( i e. ( 1 ... k ) -> ( ( ( 2 x. i ) / 2 ) - ( 1 / 2 ) ) = ( i - ( 1 / 2 ) ) )
189 185 188 eqtrd 
 |-  ( i e. ( 1 ... k ) -> ( ( ( 2 x. i ) - 1 ) / 2 ) = ( i - ( 1 / 2 ) ) )
190 148 150 zsubcld 
 |-  ( i e. ( 1 ... k ) -> ( i - 1 ) e. ZZ )
191 160 184 rereccld 
 |-  ( i e. ( 1 ... k ) -> ( 1 / 2 ) e. RR )
192 halflt1 
 |-  ( 1 / 2 ) < 1
193 192 a1i 
 |-  ( i e. ( 1 ... k ) -> ( 1 / 2 ) < 1 )
194 191 158 159 193 ltsub2dd 
 |-  ( i e. ( 1 ... k ) -> ( i - 1 ) < ( i - ( 1 / 2 ) ) )
195 2rp 
 |-  2 e. RR+
196 rpreccl 
 |-  ( 2 e. RR+ -> ( 1 / 2 ) e. RR+ )
197 195 196 mp1i 
 |-  ( i e. ( 1 ... k ) -> ( 1 / 2 ) e. RR+ )
198 159 197 ltsubrpd 
 |-  ( i e. ( 1 ... k ) -> ( i - ( 1 / 2 ) ) < i )
199 186 181 npcand 
 |-  ( i e. ( 1 ... k ) -> ( ( i - 1 ) + 1 ) = i )
200 198 199 breqtrrd 
 |-  ( i e. ( 1 ... k ) -> ( i - ( 1 / 2 ) ) < ( ( i - 1 ) + 1 ) )
201 btwnnz 
 |-  ( ( ( i - 1 ) e. ZZ /\ ( i - 1 ) < ( i - ( 1 / 2 ) ) /\ ( i - ( 1 / 2 ) ) < ( ( i - 1 ) + 1 ) ) -> -. ( i - ( 1 / 2 ) ) e. ZZ )
202 190 194 200 201 syl3anc 
 |-  ( i e. ( 1 ... k ) -> -. ( i - ( 1 / 2 ) ) e. ZZ )
203 nnz 
 |-  ( ( i - ( 1 / 2 ) ) e. NN -> ( i - ( 1 / 2 ) ) e. ZZ )
204 202 203 nsyl 
 |-  ( i e. ( 1 ... k ) -> -. ( i - ( 1 / 2 ) ) e. NN )
205 189 204 eqneltrd 
 |-  ( i e. ( 1 ... k ) -> -. ( ( ( 2 x. i ) - 1 ) / 2 ) e. NN )
206 205 intnand 
 |-  ( i e. ( 1 ... k ) -> -. ( ( ( 2 x. i ) - 1 ) e. NN /\ ( ( ( 2 x. i ) - 1 ) / 2 ) e. NN ) )
207 oveq1 
 |-  ( n = ( ( 2 x. i ) - 1 ) -> ( n / 2 ) = ( ( ( 2 x. i ) - 1 ) / 2 ) )
208 207 eleq1d 
 |-  ( n = ( ( 2 x. i ) - 1 ) -> ( ( n / 2 ) e. NN <-> ( ( ( 2 x. i ) - 1 ) / 2 ) e. NN ) )
209 208 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 ) )
210 206 209 sylnibr 
 |-  ( i e. ( 1 ... k ) -> -. ( ( 2 x. i ) - 1 ) e. { n e. NN | ( n / 2 ) e. NN } )
211 210 adantl 
 |-  ( ( k e. NN /\ i e. ( 1 ... k ) ) -> -. ( ( 2 x. i ) - 1 ) e. { n e. NN | ( n / 2 ) e. NN } )
212 179 211 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 } ) )
213 212 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 } ) )
214 eqidd 
 |-  ( x e. ( 1 ... k ) -> ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) = ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) )
215 oveq2 
 |-  ( i = x -> ( 2 x. i ) = ( 2 x. x ) )
216 215 oveq1d 
 |-  ( i = x -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. x ) - 1 ) )
217 216 adantl 
 |-  ( ( x e. ( 1 ... k ) /\ i = x ) -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. x ) - 1 ) )
218 id 
 |-  ( x e. ( 1 ... k ) -> x e. ( 1 ... k ) )
219 ovexd 
 |-  ( x e. ( 1 ... k ) -> ( ( 2 x. x ) - 1 ) e. _V )
220 214 217 218 219 fvmptd 
 |-  ( x e. ( 1 ... k ) -> ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` x ) = ( ( 2 x. x ) - 1 ) )
221 220 eqcomd 
 |-  ( x e. ( 1 ... k ) -> ( ( 2 x. x ) - 1 ) = ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` x ) )
222 221 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 ) )
223 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 ) )
224 eqidd 
 |-  ( y e. ( 1 ... k ) -> ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) = ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) )
225 oveq2 
 |-  ( i = y -> ( 2 x. i ) = ( 2 x. y ) )
226 225 oveq1d 
 |-  ( i = y -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. y ) - 1 ) )
227 226 adantl 
 |-  ( ( y e. ( 1 ... k ) /\ i = y ) -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. y ) - 1 ) )
228 id 
 |-  ( y e. ( 1 ... k ) -> y e. ( 1 ... k ) )
229 ovexd 
 |-  ( y e. ( 1 ... k ) -> ( ( 2 x. y ) - 1 ) e. _V )
230 224 227 228 229 fvmptd 
 |-  ( y e. ( 1 ... k ) -> ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` y ) = ( ( 2 x. y ) - 1 ) )
231 230 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 ) )
232 222 223 231 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 ) )
233 2cnd 
 |-  ( x e. ( 1 ... k ) -> 2 e. CC )
234 elfzelz 
 |-  ( x e. ( 1 ... k ) -> x e. ZZ )
235 234 zcnd 
 |-  ( x e. ( 1 ... k ) -> x e. CC )
236 233 235 mulcld 
 |-  ( x e. ( 1 ... k ) -> ( 2 x. x ) e. CC )
237 236 ad2antrr 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) ) -> ( 2 x. x ) e. CC )
238 2cnd 
 |-  ( y e. ( 1 ... k ) -> 2 e. CC )
239 elfzelz 
 |-  ( y e. ( 1 ... k ) -> y e. ZZ )
240 239 zcnd 
 |-  ( y e. ( 1 ... k ) -> y e. CC )
241 238 240 mulcld 
 |-  ( y e. ( 1 ... k ) -> ( 2 x. y ) e. CC )
242 241 ad2antlr 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) ) -> ( 2 x. y ) e. CC )
243 1cnd 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) ) -> 1 e. CC )
244 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 ) )
245 237 242 243 244 subcan2d 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) ) -> ( 2 x. x ) = ( 2 x. y ) )
246 235 ad2antrr 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> x e. CC )
247 240 ad2antlr 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> y e. CC )
248 2cnd 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> 2 e. CC )
249 183 a1i 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> 2 =/= 0 )
250 simpr 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> ( 2 x. x ) = ( 2 x. y ) )
251 246 247 248 249 250 mulcanad 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( 2 x. x ) = ( 2 x. y ) ) -> x = y )
252 245 251 syldan 
 |-  ( ( ( x e. ( 1 ... k ) /\ y e. ( 1 ... k ) ) /\ ( ( 2 x. x ) - 1 ) = ( ( 2 x. y ) - 1 ) ) -> x = y )
253 232 252 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 )
254 253 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 )
255 254 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 ) )
256 255 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 ) )
257 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 ) ) )
258 213 256 257 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 } ) )
259 1zzd 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> 1 e. ZZ )
260 33 adantr 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> k e. ZZ )
261 134 elfzelzd 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> j e. ZZ )
262 zeo 
 |-  ( j e. ZZ -> ( ( j / 2 ) e. ZZ \/ ( ( j + 1 ) / 2 ) e. ZZ ) )
263 261 262 syl 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> ( ( j / 2 ) e. ZZ \/ ( ( j + 1 ) / 2 ) e. ZZ ) )
264 263 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 ) )
265 eldifn 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> -. j e. { n e. NN | ( n / 2 ) e. NN } )
266 134 92 syl 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> j e. NN )
267 266 adantr 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> j e. NN )
268 simpr 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> ( j / 2 ) e. ZZ )
269 267 nnred 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> j e. RR )
270 39 a1i 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> 2 e. RR )
271 267 nngt0d 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> 0 < j )
272 2pos 
 |-  0 < 2
273 272 a1i 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> 0 < 2 )
274 269 270 271 273 divgt0d 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> 0 < ( j / 2 ) )
275 elnnz 
 |-  ( ( j / 2 ) e. NN <-> ( ( j / 2 ) e. ZZ /\ 0 < ( j / 2 ) ) )
276 268 274 275 sylanbrc 
 |-  ( ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) /\ ( j / 2 ) e. ZZ ) -> ( j / 2 ) e. NN )
277 oveq1 
 |-  ( n = j -> ( n / 2 ) = ( j / 2 ) )
278 277 eleq1d 
 |-  ( n = j -> ( ( n / 2 ) e. NN <-> ( j / 2 ) e. NN ) )
279 278 elrab 
 |-  ( j e. { n e. NN | ( n / 2 ) e. NN } <-> ( j e. NN /\ ( j / 2 ) e. NN ) )
280 267 276 279 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 } )
281 265 280 mtand 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> -. ( j / 2 ) e. ZZ )
282 281 adantl 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> -. ( j / 2 ) e. ZZ )
283 pm2.53 
 |-  ( ( ( j / 2 ) e. ZZ \/ ( ( j + 1 ) / 2 ) e. ZZ ) -> ( -. ( j / 2 ) e. ZZ -> ( ( j + 1 ) / 2 ) e. ZZ ) )
284 264 282 283 sylc 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> ( ( j + 1 ) / 2 ) e. ZZ )
285 1p1e2 
 |-  ( 1 + 1 ) = 2
286 285 oveq1i 
 |-  ( ( 1 + 1 ) / 2 ) = ( 2 / 2 )
287 2div2e1 
 |-  ( 2 / 2 ) = 1
288 286 287 eqtr2i 
 |-  1 = ( ( 1 + 1 ) / 2 )
289 1red 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> 1 e. RR )
290 289 289 readdcld 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( 1 + 1 ) e. RR )
291 92 nnred 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> j e. RR )
292 291 289 readdcld 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( j + 1 ) e. RR )
293 195 a1i 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> 2 e. RR+ )
294 elfzle1 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> 1 <_ j )
295 289 291 289 294 leadd1dd 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( 1 + 1 ) <_ ( j + 1 ) )
296 290 292 293 295 lediv1dd 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( ( 1 + 1 ) / 2 ) <_ ( ( j + 1 ) / 2 ) )
297 288 296 eqbrtrid 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> 1 <_ ( ( j + 1 ) / 2 ) )
298 134 297 syl 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> 1 <_ ( ( j + 1 ) / 2 ) )
299 298 adantl 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> 1 <_ ( ( j + 1 ) / 2 ) )
300 elfzel2 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( ( 2 x. k ) - 1 ) e. ZZ )
301 300 zred 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( ( 2 x. k ) - 1 ) e. RR )
302 301 289 readdcld 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( ( ( 2 x. k ) - 1 ) + 1 ) e. RR )
303 elfzle2 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> j <_ ( ( 2 x. k ) - 1 ) )
304 291 301 289 303 leadd1dd 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( j + 1 ) <_ ( ( ( 2 x. k ) - 1 ) + 1 ) )
305 292 302 293 304 lediv1dd 
 |-  ( j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) -> ( ( j + 1 ) / 2 ) <_ ( ( ( ( 2 x. k ) - 1 ) + 1 ) / 2 ) )
306 305 adantl 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( j + 1 ) / 2 ) <_ ( ( ( ( 2 x. k ) - 1 ) + 1 ) / 2 ) )
307 51 adantr 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( 2 x. k ) e. CC )
308 1cnd 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> 1 e. CC )
309 307 308 npcand 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( ( 2 x. k ) - 1 ) + 1 ) = ( 2 x. k ) )
310 309 oveq1d 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( ( ( 2 x. k ) - 1 ) + 1 ) / 2 ) = ( ( 2 x. k ) / 2 ) )
311 183 a1i 
 |-  ( k e. NN -> 2 =/= 0 )
312 45 44 311 divcan3d 
 |-  ( k e. NN -> ( ( 2 x. k ) / 2 ) = k )
313 312 adantr 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( 2 x. k ) / 2 ) = k )
314 310 313 eqtrd 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( ( ( 2 x. k ) - 1 ) + 1 ) / 2 ) = k )
315 306 314 breqtrd 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) ) -> ( ( j + 1 ) / 2 ) <_ k )
316 134 315 sylan2 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> ( ( j + 1 ) / 2 ) <_ k )
317 259 260 284 299 316 elfzd 
 |-  ( ( k e. NN /\ j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> ( ( j + 1 ) / 2 ) e. ( 1 ... k ) )
318 266 nncnd 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> j e. CC )
319 peano2cn 
 |-  ( j e. CC -> ( j + 1 ) e. CC )
320 2cnd 
 |-  ( j e. CC -> 2 e. CC )
321 183 a1i 
 |-  ( j e. CC -> 2 =/= 0 )
322 319 320 321 divcan2d 
 |-  ( j e. CC -> ( 2 x. ( ( j + 1 ) / 2 ) ) = ( j + 1 ) )
323 322 oveq1d 
 |-  ( j e. CC -> ( ( 2 x. ( ( j + 1 ) / 2 ) ) - 1 ) = ( ( j + 1 ) - 1 ) )
324 pncan1 
 |-  ( j e. CC -> ( ( j + 1 ) - 1 ) = j )
325 323 324 eqtr2d 
 |-  ( j e. CC -> j = ( ( 2 x. ( ( j + 1 ) / 2 ) ) - 1 ) )
326 318 325 syl 
 |-  ( j e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) -> j = ( ( 2 x. ( ( j + 1 ) / 2 ) ) - 1 ) )
327 326 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 ) )
328 oveq2 
 |-  ( m = ( ( j + 1 ) / 2 ) -> ( 2 x. m ) = ( 2 x. ( ( j + 1 ) / 2 ) ) )
329 328 oveq1d 
 |-  ( m = ( ( j + 1 ) / 2 ) -> ( ( 2 x. m ) - 1 ) = ( ( 2 x. ( ( j + 1 ) / 2 ) ) - 1 ) )
330 329 rspceeqv 
 |-  ( ( ( ( j + 1 ) / 2 ) e. ( 1 ... k ) /\ j = ( ( 2 x. ( ( j + 1 ) / 2 ) ) - 1 ) ) -> E. m e. ( 1 ... k ) j = ( ( 2 x. m ) - 1 ) )
331 317 327 330 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 ) )
332 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 ) ) )
333 oveq2 
 |-  ( i = m -> ( 2 x. i ) = ( 2 x. m ) )
334 333 oveq1d 
 |-  ( i = m -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. m ) - 1 ) )
335 334 adantl 
 |-  ( ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) /\ i = m ) -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. m ) - 1 ) )
336 simpl 
 |-  ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) -> m e. ( 1 ... k ) )
337 ovexd 
 |-  ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) -> ( ( 2 x. m ) - 1 ) e. _V )
338 332 335 336 337 fvmptd 
 |-  ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) -> ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` m ) = ( ( 2 x. m ) - 1 ) )
339 id 
 |-  ( j = ( ( 2 x. m ) - 1 ) -> j = ( ( 2 x. m ) - 1 ) )
340 339 eqcomd 
 |-  ( j = ( ( 2 x. m ) - 1 ) -> ( ( 2 x. m ) - 1 ) = j )
341 340 adantl 
 |-  ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) -> ( ( 2 x. m ) - 1 ) = j )
342 338 341 eqtr2d 
 |-  ( ( m e. ( 1 ... k ) /\ j = ( ( 2 x. m ) - 1 ) ) -> j = ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` m ) )
343 342 ex 
 |-  ( m e. ( 1 ... k ) -> ( j = ( ( 2 x. m ) - 1 ) -> j = ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` m ) ) )
344 343 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 ) ) )
345 344 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 ) ) )
346 331 345 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 ) )
347 346 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 ) )
348 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 ) ) )
349 213 347 348 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 } ) )
350 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 } ) ) )
351 258 349 350 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 } ) )
352 351 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 } ) )
353 eqidd 
 |-  ( j e. ( 1 ... k ) -> ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) = ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) )
354 oveq2 
 |-  ( i = j -> ( 2 x. i ) = ( 2 x. j ) )
355 354 oveq1d 
 |-  ( i = j -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. j ) - 1 ) )
356 355 adantl 
 |-  ( ( j e. ( 1 ... k ) /\ i = j ) -> ( ( 2 x. i ) - 1 ) = ( ( 2 x. j ) - 1 ) )
357 id 
 |-  ( j e. ( 1 ... k ) -> j e. ( 1 ... k ) )
358 ovexd 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. j ) - 1 ) e. _V )
359 353 356 357 358 fvmptd 
 |-  ( j e. ( 1 ... k ) -> ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` j ) = ( ( 2 x. j ) - 1 ) )
360 359 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( i e. ( 1 ... k ) |-> ( ( 2 x. i ) - 1 ) ) ` j ) = ( ( 2 x. j ) - 1 ) )
361 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 } ) ) )
362 361 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 } ) ) ) )
363 139 eleq1d 
 |-  ( j = i -> ( ( F ` j ) e. CC <-> ( F ` i ) e. CC ) )
364 362 363 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 ) ) )
365 364 136 chvarvv 
 |-  ( ( ( ph /\ k e. NN ) /\ i e. ( ( 1 ... ( ( 2 x. k ) - 1 ) ) \ { n e. NN | ( n / 2 ) e. NN } ) ) -> ( F ` i ) e. CC )
366 143 144 352 360 365 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 ) ) )
367 96 142 366 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 ) )
368 ovex 
 |-  ( ( 2 x. k ) - 1 ) e. _V
369 21 fvmpt2 
 |-  ( ( k e. NN /\ ( ( 2 x. k ) - 1 ) e. _V ) -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) = ( ( 2 x. k ) - 1 ) )
370 368 369 mpan2 
 |-  ( k e. NN -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) = ( ( 2 x. k ) - 1 ) )
371 370 oveq2d 
 |-  ( k e. NN -> ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) = ( 1 ... ( ( 2 x. k ) - 1 ) ) )
372 371 eqcomd 
 |-  ( k e. NN -> ( 1 ... ( ( 2 x. k ) - 1 ) ) = ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) )
373 372 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 ) )
374 373 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 ) )
375 367 374 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 ) )
376 elfznn 
 |-  ( j e. ( 1 ... k ) -> j e. NN )
377 376 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> j e. NN )
378 1 adantr 
 |-  ( ( ph /\ j e. ( 1 ... k ) ) -> F : NN --> CC )
379 31 a1i 
 |-  ( j e. ( 1 ... k ) -> 2 e. ZZ )
380 elfzelz 
 |-  ( j e. ( 1 ... k ) -> j e. ZZ )
381 379 380 zmulcld 
 |-  ( j e. ( 1 ... k ) -> ( 2 x. j ) e. ZZ )
382 1zzd 
 |-  ( j e. ( 1 ... k ) -> 1 e. ZZ )
383 381 382 zsubcld 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. j ) - 1 ) e. ZZ )
384 0red 
 |-  ( j e. ( 1 ... k ) -> 0 e. RR )
385 39 a1i 
 |-  ( j e. ( 1 ... k ) -> 2 e. RR )
386 25 385 eqeltrid 
 |-  ( j e. ( 1 ... k ) -> ( 2 x. 1 ) e. RR )
387 1red 
 |-  ( j e. ( 1 ... k ) -> 1 e. RR )
388 386 387 resubcld 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. 1 ) - 1 ) e. RR )
389 383 zred 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. j ) - 1 ) e. RR )
390 0lt1 
 |-  0 < 1
391 153 a1i 
 |-  ( j e. ( 1 ... k ) -> 1 = ( ( 2 x. 1 ) - 1 ) )
392 390 391 breqtrid 
 |-  ( j e. ( 1 ... k ) -> 0 < ( ( 2 x. 1 ) - 1 ) )
393 381 zred 
 |-  ( j e. ( 1 ... k ) -> ( 2 x. j ) e. RR )
394 376 nnred 
 |-  ( j e. ( 1 ... k ) -> j e. RR )
395 161 a1i 
 |-  ( j e. ( 1 ... k ) -> 0 <_ 2 )
396 elfzle1 
 |-  ( j e. ( 1 ... k ) -> 1 <_ j )
397 387 394 385 395 396 lemul2ad 
 |-  ( j e. ( 1 ... k ) -> ( 2 x. 1 ) <_ ( 2 x. j ) )
398 386 393 387 397 lesub1dd 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. 1 ) - 1 ) <_ ( ( 2 x. j ) - 1 ) )
399 384 388 389 392 398 ltletrd 
 |-  ( j e. ( 1 ... k ) -> 0 < ( ( 2 x. j ) - 1 ) )
400 elnnz 
 |-  ( ( ( 2 x. j ) - 1 ) e. NN <-> ( ( ( 2 x. j ) - 1 ) e. ZZ /\ 0 < ( ( 2 x. j ) - 1 ) ) )
401 383 399 400 sylanbrc 
 |-  ( j e. ( 1 ... k ) -> ( ( 2 x. j ) - 1 ) e. NN )
402 401 adantl 
 |-  ( ( ph /\ j e. ( 1 ... k ) ) -> ( ( 2 x. j ) - 1 ) e. NN )
403 378 402 ffvelrnd 
 |-  ( ( ph /\ j e. ( 1 ... k ) ) -> ( F ` ( ( 2 x. j ) - 1 ) ) e. CC )
404 403 adantlr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( F ` ( ( 2 x. j ) - 1 ) ) e. CC )
405 60 fveq2d 
 |-  ( k = j -> ( F ` ( ( 2 x. k ) - 1 ) ) = ( F ` ( ( 2 x. j ) - 1 ) ) )
406 405 cbvmptv 
 |-  ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) = ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) )
407 406 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 ) ) )
408 377 404 407 syl2anc 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ` j ) = ( F ` ( ( 2 x. j ) - 1 ) ) )
409 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
410 409 11 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
411 408 410 404 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 ) )
412 eqidd 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> ( F ` j ) = ( F ` j ) )
413 155 a1i 
 |-  ( k e. NN -> ( 2 x. 1 ) e. RR )
414 1red 
 |-  ( k e. NN -> 1 e. RR )
415 161 a1i 
 |-  ( k e. NN -> 0 <_ 2 )
416 nnge1 
 |-  ( k e. NN -> 1 <_ k )
417 414 41 40 415 416 lemul2ad 
 |-  ( k e. NN -> ( 2 x. 1 ) <_ ( 2 x. k ) )
418 413 42 414 417 lesub1dd 
 |-  ( k e. NN -> ( ( 2 x. 1 ) - 1 ) <_ ( ( 2 x. k ) - 1 ) )
419 153 418 eqbrtrid 
 |-  ( k e. NN -> 1 <_ ( ( 2 x. k ) - 1 ) )
420 eluz2 
 |-  ( ( ( 2 x. k ) - 1 ) e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ ( ( 2 x. k ) - 1 ) e. ZZ /\ 1 <_ ( ( 2 x. k ) - 1 ) ) )
421 37 66 419 420 syl3anbrc 
 |-  ( k e. NN -> ( ( 2 x. k ) - 1 ) e. ( ZZ>= ` 1 ) )
422 68 421 eqeltrd 
 |-  ( k e. NN -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) e. ( ZZ>= ` 1 ) )
423 422 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) e. ( ZZ>= ` 1 ) )
424 simpll 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> ph )
425 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 ) ) )
426 371 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 ) ) )
427 425 426 eleqtrd 
 |-  ( ( k e. NN /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) )
428 427 adantll 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> j e. ( 1 ... ( ( 2 x. k ) - 1 ) ) )
429 424 428 94 syl2anc 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... ( ( k e. NN |-> ( ( 2 x. k ) - 1 ) ) ` k ) ) ) -> ( F ` j ) e. CC )
430 412 423 429 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 ) ) )
431 375 411 430 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 ) ) )
432 4 5 9 10 11 12 14 17 3 30 74 76 431 climsuse 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> B )
433 eqidd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
434 11 12 433 15 isum 
 |-  ( ph -> sum_ k e. NN ( F ` k ) = ( ~~> ` seq 1 ( + , F ) ) )
435 climrel 
 |-  Rel ~~>
436 435 releldmi 
 |-  ( seq 1 ( + , F ) ~~> B -> seq 1 ( + , F ) e. dom ~~> )
437 3 436 syl 
 |-  ( ph -> seq 1 ( + , F ) e. dom ~~> )
438 climdm 
 |-  ( seq 1 ( + , F ) e. dom ~~> <-> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
439 437 438 sylib 
 |-  ( ph -> seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) )
440 climuni 
 |-  ( ( seq 1 ( + , F ) ~~> ( ~~> ` seq 1 ( + , F ) ) /\ seq 1 ( + , F ) ~~> B ) -> ( ~~> ` seq 1 ( + , F ) ) = B )
441 439 3 440 syl2anc 
 |-  ( ph -> ( ~~> ` seq 1 ( + , F ) ) = B )
442 435 a1i 
 |-  ( ph -> Rel ~~> )
443 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 ~~> )
444 442 432 443 syl2anc 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) e. dom ~~> )
445 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 ) ) ) ) ) )
446 444 445 sylib 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> ( ~~> ` seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ) )
447 406 a1i 
 |-  ( ph -> ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) = ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) )
448 447 seqeq3d 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) = seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) )
449 448 fveq2d 
 |-  ( ph -> ( ~~> ` seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ) = ( ~~> ` seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) ) )
450 446 449 breqtrd 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> ( ~~> ` seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) ) )
451 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 ) ) ) ) ) )
452 432 450 451 syl2anc 
 |-  ( ph -> B = ( ~~> ` seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) ) )
453 eqidd 
 |-  ( ( ph /\ k e. NN ) -> ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) = ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) )
454 eqcom 
 |-  ( k = j <-> j = k )
455 eqcom 
 |-  ( ( F ` ( ( 2 x. k ) - 1 ) ) = ( F ` ( ( 2 x. j ) - 1 ) ) <-> ( F ` ( ( 2 x. j ) - 1 ) ) = ( F ` ( ( 2 x. k ) - 1 ) ) )
456 405 454 455 3imtr3i 
 |-  ( j = k -> ( F ` ( ( 2 x. j ) - 1 ) ) = ( F ` ( ( 2 x. k ) - 1 ) ) )
457 456 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ j = k ) -> ( F ` ( ( 2 x. j ) - 1 ) ) = ( F ` ( ( 2 x. k ) - 1 ) ) )
458 1 adantr 
 |-  ( ( ph /\ k e. NN ) -> F : NN --> CC )
459 421 11 eleqtrrdi 
 |-  ( k e. NN -> ( ( 2 x. k ) - 1 ) e. NN )
460 459 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2 x. k ) - 1 ) e. NN )
461 458 460 ffvelrnd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( ( 2 x. k ) - 1 ) ) e. CC )
462 453 457 409 461 fvmptd 
 |-  ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ` k ) = ( F ` ( ( 2 x. k ) - 1 ) ) )
463 11 12 462 461 isum 
 |-  ( ph -> sum_ k e. NN ( F ` ( ( 2 x. k ) - 1 ) ) = ( ~~> ` seq 1 ( + , ( j e. NN |-> ( F ` ( ( 2 x. j ) - 1 ) ) ) ) ) )
464 452 463 eqtr4d 
 |-  ( ph -> B = sum_ k e. NN ( F ` ( ( 2 x. k ) - 1 ) ) )
465 434 441 464 3eqtrd 
 |-  ( ph -> sum_ k e. NN ( F ` k ) = sum_ k e. NN ( F ` ( ( 2 x. k ) - 1 ) ) )
466 432 465 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 ) ) ) )