Theorem itcovalt2lem1

Description: Lemma 1 for itcovalt2 : induction basis. (Contributed by AV, 5-May-2024)

	Ref	Expression
Hypothesis	itcovalt2.f	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 𝐶 ) )
Assertion	itcovalt2lem1	⊢ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) − 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		itcovalt2.f	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 𝐶 ) )
2		nn0ex	⊢ ℕ0 ∈ V
3		ovexd	⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 · 𝑛 ) + 𝐶 ) ∈ V )
4	3	rgen	⊢ ∀ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 𝐶 ) ∈ V
5	2 4	pm3.2i	⊢ ( ℕ0 ∈ V ∧ ∀ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 𝐶 ) ∈ V )
6	1	itcoval0mpt	⊢ ( ( ℕ0 ∈ V ∧ ∀ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 𝐶 ) ∈ V ) → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ 𝑛 ) )
7	5 6	mp1i	⊢ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ 𝑛 ) )
8		simpr	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
9	8	nn0cnd	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℂ )
10		simpl	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 )
11	10	nn0cnd	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
12		2nn0	⊢ 2 ∈ ℕ0
13	12	numexp0	⊢ ( 2 ↑ 0 ) = 1
14	13	a1i	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 0 ) = 1 )
15	14	oveq2d	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) = ( ( 𝑛 + 𝐶 ) · 1 ) )
16	8 10	nn0addcld	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + 𝐶 ) ∈ ℕ0 )
17	16	nn0cnd	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + 𝐶 ) ∈ ℂ )
18	17	mulid1d	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + 𝐶 ) · 1 ) = ( 𝑛 + 𝐶 ) )
19	15 18	eqtrd	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) = ( 𝑛 + 𝐶 ) )
20	9 11 19	mvrraddd	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) − 𝐶 ) = 𝑛 )
21	20	eqcomd	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 = ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) − 𝐶 ) )
22	21	mpteq2dva	⊢ ( 𝐶 ∈ ℕ0 → ( 𝑛 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) − 𝐶 ) ) )
23	7 22	eqtrd	⊢ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) − 𝐶 ) ) )