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	$⊢ (φ \land k \in ℕ_{0}) \to C \in ℂ$
	iserodd.h	$⊢ n = 2 k + 1 \to B = C$
Assertion	iserodd	$⊢ φ \to (seq 0 (+ (k \in ℕ_{0} ⟼ C)) ⇝ A \leftrightarrow seq 1 (+ (n \in ℕ ⟼ if (2 ∥ n, 0, B))) ⇝ A)$

Proof

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

Metamath Proof Explorer

Theorem iserodd

Proof