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

Metamath Proof Explorer

Theorem itcovalpclem1

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

Ref Expression
Hypothesis itcovalpc.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) )
Assertion itcovalpclem1 ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 itcovalpc.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) )
2 nn0ex ⊢ ℕ0 ∈ V
3 ovexd ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 𝐶 ) ∈ V )
4 3 rgen ⊢ ∀ 𝑛 ∈ ℕ0 ( 𝑛 + 𝐶 ) ∈ V
5 1 itcoval0mpt ⊢ ( ( ℕ0 ∈ V ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑛 + 𝐶 ) ∈ V ) → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ 𝑛 ) )
6 2 4 5 mp2an ⊢ ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ 𝑛 )
7 nn0cn ⊢ ( 𝐶 ∈ ℕ0 → 𝐶 ∈ ℂ )
8 7 mul01d ⊢ ( 𝐶 ∈ ℕ0 → ( 𝐶 · 0 ) = 0 )
9 8 adantr ⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐶 · 0 ) = 0 )
10 9 oveq2d ⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + ( 𝐶 · 0 ) ) = ( 𝑛 + 0 ) )
11 nn0cn ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
12 11 addridd ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 0 ) = 𝑛 )
13 12 adantl ⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + 0 ) = 𝑛 )
14 10 13 eqtr2d ⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 = ( 𝑛 + ( 𝐶 · 0 ) ) )
15 14 mpteq2dva ⊢ ( 𝐶 ∈ ℕ0 → ( 𝑛 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) )
16 6 15 eqtrid ⊢ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) )