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 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
iserodd.h ⊢ ( 𝑛 = ( ( 2 · 𝑘 ) + 1 ) → 𝐵 = 𝐶 )
Assertion iserodd ( 𝜑 → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) ⇝ 𝐴 ↔ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ if ( 2 ∥ 𝑛 , 0 , 𝐵 ) ) ) ⇝ 𝐴 ) )

Proof

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