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 , 𝐵 ) ) ) ⇝ 𝐴 ) )