This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mulridd ⊢ ( ( 𝐶 ∈ ℕ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 ) ) − 𝐶 ) ) )