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