Metamath Proof Explorer

Theorem itcovalpclem2

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

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

Proof

Step Hyp Ref Expression
1 itcovalpc.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) )
2 nn0ex ⊢ ℕ0 ∈ V
3 2 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) ) ∈ V
4 1 3 eqeltri ⊢ 𝐹 ∈ V
5 simpl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝑦 ∈ ℕ0 )
6 simpr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) )
7 itcovalsucov ⊢ ( ( 𝐹 ∈ V ∧ 𝑦 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) )
8 4 5 6 7 mp3an2ani ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) )
9 simpr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
10 simplr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 )
11 5 adantr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑦 ∈ ℕ0 )
12 10 11 nn0mulcld ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐶 · 𝑦 ) ∈ ℕ0 )
13 9 12 nn0addcld ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + ( 𝐶 · 𝑦 ) ) ∈ ℕ0 )
14 eqidd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) )
15 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 + 𝐶 ) = ( 𝑚 + 𝐶 ) )
16 15 cbvmptv ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 + 𝐶 ) )
17 1 16 eqtri ⊢ 𝐹 = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 + 𝐶 ) )
18 17 a1i ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝐹 = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 + 𝐶 ) ) )
19 oveq1 ⊢ ( 𝑚 = ( 𝑛 + ( 𝐶 · 𝑦 ) ) → ( 𝑚 + 𝐶 ) = ( ( 𝑛 + ( 𝐶 · 𝑦 ) ) + 𝐶 ) )
20 13 14 18 19 fmptco ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 + ( 𝐶 · 𝑦 ) ) + 𝐶 ) ) )
21 9 nn0cnd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℂ )
22 12 nn0cnd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐶 · 𝑦 ) ∈ ℂ )
23 10 nn0cnd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
24 21 22 23 addassd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + ( 𝐶 · 𝑦 ) ) + 𝐶 ) = ( 𝑛 + ( ( 𝐶 · 𝑦 ) + 𝐶 ) ) )
25 nn0cn ⊢ ( 𝐶 ∈ ℕ0 → 𝐶 ∈ ℂ )
26 25 mulid1d ⊢ ( 𝐶 ∈ ℕ0 → ( 𝐶 · 1 ) = 𝐶 )
27 26 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 · 1 ) = 𝐶 )
28 27 eqcomd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝐶 = ( 𝐶 · 1 ) )
29 28 oveq2d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 · 𝑦 ) + 𝐶 ) = ( ( 𝐶 · 𝑦 ) + ( 𝐶 · 1 ) ) )
30 simpr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 )
31 30 nn0cnd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
32 5 nn0cnd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝑦 ∈ ℂ )
33 1cnd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 1 ∈ ℂ )
34 31 32 33 adddid ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 · ( 𝑦 + 1 ) ) = ( ( 𝐶 · 𝑦 ) + ( 𝐶 · 1 ) ) )
35 29 34 eqtr4d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 · 𝑦 ) + 𝐶 ) = ( 𝐶 · ( 𝑦 + 1 ) ) )
36 35 oveq2d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝑛 + ( ( 𝐶 · 𝑦 ) + 𝐶 ) ) = ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) )
37 36 adantr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + ( ( 𝐶 · 𝑦 ) + 𝐶 ) ) = ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) )
38 24 37 eqtrd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + ( 𝐶 · 𝑦 ) ) + 𝐶 ) = ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) )
39 38 mpteq2dva ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 + ( 𝐶 · 𝑦 ) ) + 𝐶 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
40 20 39 eqtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
41 40 adantr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
42 8 41 eqtrd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
43 42 ex ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) ) )