iserodd

Description: Collect the odd terms in a sequence. (Contributed by Mario Carneiro, 7-Apr-2015) (Proof shortened by AV, 10-Jul-2022)

	Ref	Expression
Hypotheses	iserodd.f	\|- ( ( ph /\ k e. NN0 ) -> C e. CC )
	iserodd.h	\|- ( n = ( ( 2 x. k ) + 1 ) -> B = C )
Assertion	iserodd	\|- ( ph -> ( seq 0 ( + , ( k e. NN0 \|-> C ) ) ~~> A <-> seq 1 ( + , ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ) ~~> A ) )

Proof

Step	Hyp	Ref	Expression
1		iserodd.f	\|- ( ( ph /\ k e. NN0 ) -> C e. CC )
2		iserodd.h	\|- ( n = ( ( 2 x. k ) + 1 ) -> B = C )
3		nn0uz	\|- NN0 = ( ZZ>= ` 0 )
4		nnuz	\|- NN = ( ZZ>= ` 1 )
5		0zd	\|- ( ph -> 0 e. ZZ )
6		1zzd	\|- ( ph -> 1 e. ZZ )
7		2nn0	\|- 2 e. NN0
8	7	a1i	\|- ( ph -> 2 e. NN0 )
9		nn0mulcl	\|- ( ( 2 e. NN0 /\ m e. NN0 ) -> ( 2 x. m ) e. NN0 )
10	8 9	sylan	\|- ( ( ph /\ m e. NN0 ) -> ( 2 x. m ) e. NN0 )
11		nn0p1nn	\|- ( ( 2 x. m ) e. NN0 -> ( ( 2 x. m ) + 1 ) e. NN )
12	10 11	syl	\|- ( ( ph /\ m e. NN0 ) -> ( ( 2 x. m ) + 1 ) e. NN )
13	12	fmpttd	\|- ( ph -> ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) : NN0 --> NN )
14		nn0mulcl	\|- ( ( 2 e. NN0 /\ i e. NN0 ) -> ( 2 x. i ) e. NN0 )
15	8 14	sylan	\|- ( ( ph /\ i e. NN0 ) -> ( 2 x. i ) e. NN0 )
16	15	nn0red	\|- ( ( ph /\ i e. NN0 ) -> ( 2 x. i ) e. RR )
17		peano2nn0	\|- ( i e. NN0 -> ( i + 1 ) e. NN0 )
18		nn0mulcl	\|- ( ( 2 e. NN0 /\ ( i + 1 ) e. NN0 ) -> ( 2 x. ( i + 1 ) ) e. NN0 )
19	8 17 18	syl2an	\|- ( ( ph /\ i e. NN0 ) -> ( 2 x. ( i + 1 ) ) e. NN0 )
20	19	nn0red	\|- ( ( ph /\ i e. NN0 ) -> ( 2 x. ( i + 1 ) ) e. RR )
21		1red	\|- ( ( ph /\ i e. NN0 ) -> 1 e. RR )
22		nn0re	\|- ( i e. NN0 -> i e. RR )
23	22	adantl	\|- ( ( ph /\ i e. NN0 ) -> i e. RR )
24	23	ltp1d	\|- ( ( ph /\ i e. NN0 ) -> i < ( i + 1 ) )
25		1red	\|- ( i e. NN0 -> 1 e. RR )
26	22 25	readdcld	\|- ( i e. NN0 -> ( i + 1 ) e. RR )
27		2rp	\|- 2 e. RR+
28	27	a1i	\|- ( i e. NN0 -> 2 e. RR+ )
29	22 26 28	ltmul2d	\|- ( i e. NN0 -> ( i < ( i + 1 ) <-> ( 2 x. i ) < ( 2 x. ( i + 1 ) ) ) )
30	29	adantl	\|- ( ( ph /\ i e. NN0 ) -> ( i < ( i + 1 ) <-> ( 2 x. i ) < ( 2 x. ( i + 1 ) ) ) )
31	24 30	mpbid	\|- ( ( ph /\ i e. NN0 ) -> ( 2 x. i ) < ( 2 x. ( i + 1 ) ) )
32	16 20 21 31	ltadd1dd	\|- ( ( ph /\ i e. NN0 ) -> ( ( 2 x. i ) + 1 ) < ( ( 2 x. ( i + 1 ) ) + 1 ) )
33		oveq2	\|- ( m = i -> ( 2 x. m ) = ( 2 x. i ) )
34	33	oveq1d	\|- ( m = i -> ( ( 2 x. m ) + 1 ) = ( ( 2 x. i ) + 1 ) )
35		eqid	\|- ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) = ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) )
36		ovex	\|- ( ( 2 x. i ) + 1 ) e. _V
37	34 35 36	fvmpt	\|- ( i e. NN0 -> ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` i ) = ( ( 2 x. i ) + 1 ) )
38	37	adantl	\|- ( ( ph /\ i e. NN0 ) -> ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` i ) = ( ( 2 x. i ) + 1 ) )
39	17	adantl	\|- ( ( ph /\ i e. NN0 ) -> ( i + 1 ) e. NN0 )
40		oveq2	\|- ( m = ( i + 1 ) -> ( 2 x. m ) = ( 2 x. ( i + 1 ) ) )
41	40	oveq1d	\|- ( m = ( i + 1 ) -> ( ( 2 x. m ) + 1 ) = ( ( 2 x. ( i + 1 ) ) + 1 ) )
42		ovex	\|- ( ( 2 x. ( i + 1 ) ) + 1 ) e. _V
43	41 35 42	fvmpt	\|- ( ( i + 1 ) e. NN0 -> ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` ( i + 1 ) ) = ( ( 2 x. ( i + 1 ) ) + 1 ) )
44	39 43	syl	\|- ( ( ph /\ i e. NN0 ) -> ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` ( i + 1 ) ) = ( ( 2 x. ( i + 1 ) ) + 1 ) )
45	32 38 44	3brtr4d	\|- ( ( ph /\ i e. NN0 ) -> ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` i ) < ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` ( i + 1 ) ) )
46		eldifi	\|- ( n e. ( NN \ ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) -> n e. NN )
47		simpr	\|- ( ( ph /\ n e. NN ) -> n e. NN )
48		0cnd	\|- ( ( ( ph /\ n e. NN ) /\ 2 \|\| n ) -> 0 e. CC )
49		nnz	\|- ( n e. NN -> n e. ZZ )
50	49	adantl	\|- ( ( ph /\ n e. NN ) -> n e. ZZ )
51		odd2np1	\|- ( n e. ZZ -> ( -. 2 \|\| n <-> E. k e. ZZ ( ( 2 x. k ) + 1 ) = n ) )
52	50 51	syl	\|- ( ( ph /\ n e. NN ) -> ( -. 2 \|\| n <-> E. k e. ZZ ( ( 2 x. k ) + 1 ) = n ) )
53		simprl	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> k e. ZZ )
54		nnm1nn0	\|- ( n e. NN -> ( n - 1 ) e. NN0 )
55	54	ad2antlr	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( n - 1 ) e. NN0 )
56	55	nn0red	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( n - 1 ) e. RR )
57	27	a1i	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 2 e. RR+ )
58	55	nn0ge0d	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 0 <_ ( n - 1 ) )
59	56 57 58	divge0d	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 0 <_ ( ( n - 1 ) / 2 ) )
60		simprr	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( 2 x. k ) + 1 ) = n )
61	60	oveq1d	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( ( 2 x. k ) + 1 ) - 1 ) = ( n - 1 ) )
62		2cn	\|- 2 e. CC
63		zcn	\|- ( k e. ZZ -> k e. CC )
64	63	ad2antrl	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> k e. CC )
65		mulcl	\|- ( ( 2 e. CC /\ k e. CC ) -> ( 2 x. k ) e. CC )
66	62 64 65	sylancr	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( 2 x. k ) e. CC )
67		ax-1cn	\|- 1 e. CC
68		pncan	\|- ( ( ( 2 x. k ) e. CC /\ 1 e. CC ) -> ( ( ( 2 x. k ) + 1 ) - 1 ) = ( 2 x. k ) )
69	66 67 68	sylancl	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( ( 2 x. k ) + 1 ) - 1 ) = ( 2 x. k ) )
70	61 69	eqtr3d	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( n - 1 ) = ( 2 x. k ) )
71	70	oveq1d	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( n - 1 ) / 2 ) = ( ( 2 x. k ) / 2 ) )
72		2cnd	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 2 e. CC )
73		2ne0	\|- 2 =/= 0
74	73	a1i	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 2 =/= 0 )
75	64 72 74	divcan3d	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( 2 x. k ) / 2 ) = k )
76	71 75	eqtrd	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> ( ( n - 1 ) / 2 ) = k )
77	59 76	breqtrd	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> 0 <_ k )
78		elnn0z	\|- ( k e. NN0 <-> ( k e. ZZ /\ 0 <_ k ) )
79	53 77 78	sylanbrc	\|- ( ( ( ph /\ n e. NN ) /\ ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) ) -> k e. NN0 )
80	79	ex	\|- ( ( ph /\ n e. NN ) -> ( ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) -> k e. NN0 ) )
81		simpr	\|- ( ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) -> ( ( 2 x. k ) + 1 ) = n )
82	81	eqcomd	\|- ( ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) -> n = ( ( 2 x. k ) + 1 ) )
83	80 82	jca2	\|- ( ( ph /\ n e. NN ) -> ( ( k e. ZZ /\ ( ( 2 x. k ) + 1 ) = n ) -> ( k e. NN0 /\ n = ( ( 2 x. k ) + 1 ) ) ) )
84	83	reximdv2	\|- ( ( ph /\ n e. NN ) -> ( E. k e. ZZ ( ( 2 x. k ) + 1 ) = n -> E. k e. NN0 n = ( ( 2 x. k ) + 1 ) ) )
85	52 84	sylbid	\|- ( ( ph /\ n e. NN ) -> ( -. 2 \|\| n -> E. k e. NN0 n = ( ( 2 x. k ) + 1 ) ) )
86	2	eleq1d	\|- ( n = ( ( 2 x. k ) + 1 ) -> ( B e. CC <-> C e. CC ) )
87	1 86	syl5ibrcom	\|- ( ( ph /\ k e. NN0 ) -> ( n = ( ( 2 x. k ) + 1 ) -> B e. CC ) )
88	87	rexlimdva	\|- ( ph -> ( E. k e. NN0 n = ( ( 2 x. k ) + 1 ) -> B e. CC ) )
89	88	adantr	\|- ( ( ph /\ n e. NN ) -> ( E. k e. NN0 n = ( ( 2 x. k ) + 1 ) -> B e. CC ) )
90	85 89	syld	\|- ( ( ph /\ n e. NN ) -> ( -. 2 \|\| n -> B e. CC ) )
91	90	imp	\|- ( ( ( ph /\ n e. NN ) /\ -. 2 \|\| n ) -> B e. CC )
92	48 91	ifclda	\|- ( ( ph /\ n e. NN ) -> if ( 2 \|\| n , 0 , B ) e. CC )
93		eqid	\|- ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) = ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) )
94	93	fvmpt2	\|- ( ( n e. NN /\ if ( 2 \|\| n , 0 , B ) e. CC ) -> ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` n ) = if ( 2 \|\| n , 0 , B ) )
95	47 92 94	syl2anc	\|- ( ( ph /\ n e. NN ) -> ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` n ) = if ( 2 \|\| n , 0 , B ) )
96	46 95	sylan2	\|- ( ( ph /\ n e. ( NN \ ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) ) -> ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` n ) = if ( 2 \|\| n , 0 , B ) )
97		eldif	\|- ( n e. ( NN \ ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) <-> ( n e. NN /\ -. n e. ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) )
98		oveq2	\|- ( m = k -> ( 2 x. m ) = ( 2 x. k ) )
99	98	oveq1d	\|- ( m = k -> ( ( 2 x. m ) + 1 ) = ( ( 2 x. k ) + 1 ) )
100	99	cbvmptv	\|- ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) = ( k e. NN0 \|-> ( ( 2 x. k ) + 1 ) )
101	100	elrnmpt	\|- ( n e. _V -> ( n e. ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) <-> E. k e. NN0 n = ( ( 2 x. k ) + 1 ) ) )
102	101	elv	\|- ( n e. ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) <-> E. k e. NN0 n = ( ( 2 x. k ) + 1 ) )
103	85 102	imbitrrdi	\|- ( ( ph /\ n e. NN ) -> ( -. 2 \|\| n -> n e. ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) )
104	103	con1d	\|- ( ( ph /\ n e. NN ) -> ( -. n e. ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) -> 2 \|\| n ) )
105	104	impr	\|- ( ( ph /\ ( n e. NN /\ -. n e. ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) ) -> 2 \|\| n )
106	97 105	sylan2b	\|- ( ( ph /\ n e. ( NN \ ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) ) -> 2 \|\| n )
107	106	iftrued	\|- ( ( ph /\ n e. ( NN \ ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) ) -> if ( 2 \|\| n , 0 , B ) = 0 )
108	96 107	eqtrd	\|- ( ( ph /\ n e. ( NN \ ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) ) -> ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` n ) = 0 )
109	108	ralrimiva	\|- ( ph -> A. n e. ( NN \ ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` n ) = 0 )
110		nfv	\|- F/ j ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` n ) = 0
111		nffvmpt1	\|- F/_ n ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` j )
112	111	nfeq1	\|- F/ n ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` j ) = 0
113		fveqeq2	\|- ( n = j -> ( ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` n ) = 0 <-> ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` j ) = 0 ) )
114	110 112 113	cbvralw	\|- ( A. n e. ( NN \ ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` n ) = 0 <-> A. j e. ( NN \ ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` j ) = 0 )
115	109 114	sylib	\|- ( ph -> A. j e. ( NN \ ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` j ) = 0 )
116	115	r19.21bi	\|- ( ( ph /\ j e. ( NN \ ran ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ) ) -> ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` j ) = 0 )
117	92	fmpttd	\|- ( ph -> ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) : NN --> CC )
118	117	ffvelcdmda	\|- ( ( ph /\ j e. NN ) -> ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` j ) e. CC )
119		simpr	\|- ( ( ph /\ k e. NN0 ) -> k e. NN0 )
120		eqid	\|- ( k e. NN0 \|-> C ) = ( k e. NN0 \|-> C )
121	120	fvmpt2	\|- ( ( k e. NN0 /\ C e. CC ) -> ( ( k e. NN0 \|-> C ) ` k ) = C )
122	119 1 121	syl2anc	\|- ( ( ph /\ k e. NN0 ) -> ( ( k e. NN0 \|-> C ) ` k ) = C )
123		ovex	\|- ( ( 2 x. k ) + 1 ) e. _V
124	99 35 123	fvmpt	\|- ( k e. NN0 -> ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` k ) = ( ( 2 x. k ) + 1 ) )
125	124	adantl	\|- ( ( ph /\ k e. NN0 ) -> ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` k ) = ( ( 2 x. k ) + 1 ) )
126	125	fveq2d	\|- ( ( ph /\ k e. NN0 ) -> ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` k ) ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( 2 x. k ) + 1 ) ) )
127		breq2	\|- ( n = ( ( 2 x. k ) + 1 ) -> ( 2 \|\| n <-> 2 \|\| ( ( 2 x. k ) + 1 ) ) )
128	127 2	ifbieq2d	\|- ( n = ( ( 2 x. k ) + 1 ) -> if ( 2 \|\| n , 0 , B ) = if ( 2 \|\| ( ( 2 x. k ) + 1 ) , 0 , C ) )
129		nn0mulcl	\|- ( ( 2 e. NN0 /\ k e. NN0 ) -> ( 2 x. k ) e. NN0 )
130	8 129	sylan	\|- ( ( ph /\ k e. NN0 ) -> ( 2 x. k ) e. NN0 )
131		nn0p1nn	\|- ( ( 2 x. k ) e. NN0 -> ( ( 2 x. k ) + 1 ) e. NN )
132	130 131	syl	\|- ( ( ph /\ k e. NN0 ) -> ( ( 2 x. k ) + 1 ) e. NN )
133		2z	\|- 2 e. ZZ
134		nn0z	\|- ( k e. NN0 -> k e. ZZ )
135	134	adantl	\|- ( ( ph /\ k e. NN0 ) -> k e. ZZ )
136		dvdsmul1	\|- ( ( 2 e. ZZ /\ k e. ZZ ) -> 2 \|\| ( 2 x. k ) )
137	133 135 136	sylancr	\|- ( ( ph /\ k e. NN0 ) -> 2 \|\| ( 2 x. k ) )
138	130	nn0zd	\|- ( ( ph /\ k e. NN0 ) -> ( 2 x. k ) e. ZZ )
139		2nn	\|- 2 e. NN
140	139	a1i	\|- ( ( ph /\ k e. NN0 ) -> 2 e. NN )
141		1lt2	\|- 1 < 2
142	141	a1i	\|- ( ( ph /\ k e. NN0 ) -> 1 < 2 )
143		ndvdsp1	\|- ( ( ( 2 x. k ) e. ZZ /\ 2 e. NN /\ 1 < 2 ) -> ( 2 \|\| ( 2 x. k ) -> -. 2 \|\| ( ( 2 x. k ) + 1 ) ) )
144	138 140 142 143	syl3anc	\|- ( ( ph /\ k e. NN0 ) -> ( 2 \|\| ( 2 x. k ) -> -. 2 \|\| ( ( 2 x. k ) + 1 ) ) )
145	137 144	mpd	\|- ( ( ph /\ k e. NN0 ) -> -. 2 \|\| ( ( 2 x. k ) + 1 ) )
146	145	iffalsed	\|- ( ( ph /\ k e. NN0 ) -> if ( 2 \|\| ( ( 2 x. k ) + 1 ) , 0 , C ) = C )
147	146 1	eqeltrd	\|- ( ( ph /\ k e. NN0 ) -> if ( 2 \|\| ( ( 2 x. k ) + 1 ) , 0 , C ) e. CC )
148	93 128 132 147	fvmptd3	\|- ( ( ph /\ k e. NN0 ) -> ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( 2 x. k ) + 1 ) ) = if ( 2 \|\| ( ( 2 x. k ) + 1 ) , 0 , C ) )
149	126 148 146	3eqtrd	\|- ( ( ph /\ k e. NN0 ) -> ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` k ) ) = C )
150	122 149	eqtr4d	\|- ( ( ph /\ k e. NN0 ) -> ( ( k e. NN0 \|-> C ) ` k ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` k ) ) )
151	150	ralrimiva	\|- ( ph -> A. k e. NN0 ( ( k e. NN0 \|-> C ) ` k ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` k ) ) )
152		nfv	\|- F/ i ( ( k e. NN0 \|-> C ) ` k ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` k ) )
153		nffvmpt1	\|- F/_ k ( ( k e. NN0 \|-> C ) ` i )
154	153	nfeq1	\|- F/ k ( ( k e. NN0 \|-> C ) ` i ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` i ) )
155		fveq2	\|- ( k = i -> ( ( k e. NN0 \|-> C ) ` k ) = ( ( k e. NN0 \|-> C ) ` i ) )
156		2fveq3	\|- ( k = i -> ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` k ) ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` i ) ) )
157	155 156	eqeq12d	\|- ( k = i -> ( ( ( k e. NN0 \|-> C ) ` k ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` k ) ) <-> ( ( k e. NN0 \|-> C ) ` i ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` i ) ) ) )
158	152 154 157	cbvralw	\|- ( A. k e. NN0 ( ( k e. NN0 \|-> C ) ` k ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` k ) ) <-> A. i e. NN0 ( ( k e. NN0 \|-> C ) ` i ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` i ) ) )
159	151 158	sylib	\|- ( ph -> A. i e. NN0 ( ( k e. NN0 \|-> C ) ` i ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` i ) ) )
160	159	r19.21bi	\|- ( ( ph /\ i e. NN0 ) -> ( ( k e. NN0 \|-> C ) ` i ) = ( ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ` ( ( m e. NN0 \|-> ( ( 2 x. m ) + 1 ) ) ` i ) ) )
161	3 4 5 6 13 45 116 118 160	isercoll2	\|- ( ph -> ( seq 0 ( + , ( k e. NN0 \|-> C ) ) ~~> A <-> seq 1 ( + , ( n e. NN \|-> if ( 2 \|\| n , 0 , B ) ) ) ~~> A ) )

Metamath Proof Explorer

Theorem iserodd

Proof