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