# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {C}\in ℂ$
iserodd.h ${⊢}{n}=2{k}+1\to {B}={C}$
Assertion iserodd ${⊢}{\phi }\to \left(seq0\left(+,\left({k}\in {ℕ}_{0}⟼{C}\right)\right)⇝{A}↔seq1\left(+,\left({n}\in ℕ⟼if\left(2\parallel {n},0,{B}\right)\right)\right)⇝{A}\right)$

### Proof

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