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

Metamath Proof Explorer

Theorem sumnnodd

Proof