Metamath Proof Explorer

Theorem itcovalt2lem2

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

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

Proof

Step Hyp Ref Expression
1 itcovalt2.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 𝐶 ) )
2 nn0ex ⊢ ℕ0 ∈ V
3 2 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 𝐶 ) ) ∈ V
4 1 3 eqeltri ⊢ 𝐹 ∈ V
5 simpl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝑦 ∈ ℕ0 )
6 simpr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) )
7 itcovalsucov ⊢ ( ( 𝐹 ∈ V ∧ 𝑦 ∈ ℕ0 ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) )
8 4 5 6 7 mp3an2ani ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) )
9 2nn ⊢ 2 ∈ ℕ
10 9 a1i ⊢ ( 𝑦 ∈ ℕ0 → 2 ∈ ℕ )
11 id ⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℕ0 )
12 10 11 nnexpcld ⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ 𝑦 ) ∈ ℕ )
13 itcovalt2lem2lem1 ⊢ ( ( ( ( 2 ↑ 𝑦 ) ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ∈ ℕ0 )
14 12 13 sylanl1 ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ∈ ℕ0 )
15 eqidd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) )
16 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 2 · 𝑛 ) = ( 2 · 𝑚 ) )
17 16 oveq1d ⊢ ( 𝑛 = 𝑚 → ( ( 2 · 𝑛 ) + 𝐶 ) = ( ( 2 · 𝑚 ) + 𝐶 ) )
18 17 cbvmptv ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 𝐶 ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 2 · 𝑚 ) + 𝐶 ) )
19 1 18 eqtri ⊢ 𝐹 = ( 𝑚 ∈ ℕ0 ↦ ( ( 2 · 𝑚 ) + 𝐶 ) )
20 19 a1i ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝐹 = ( 𝑚 ∈ ℕ0 ↦ ( ( 2 · 𝑚 ) + 𝐶 ) ) )
21 oveq2 ⊢ ( 𝑚 = ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) → ( 2 · 𝑚 ) = ( 2 · ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) )
22 21 oveq1d ⊢ ( 𝑚 = ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) → ( ( 2 · 𝑚 ) + 𝐶 ) = ( ( 2 · ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) + 𝐶 ) )
23 14 15 20 22 fmptco ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) + 𝐶 ) ) )
24 itcovalt2lem2lem2 ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 · ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) + 𝐶 ) = ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) )
25 24 mpteq2dva ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) + 𝐶 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) )
26 23 25 eqtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) )
27 26 adantr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) → ( 𝐹 ∘ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) )
28 8 27 eqtrd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) )
29 28 ex ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) ) )