Metamath Proof Explorer

Theorem itcovalt2

Description: The value of the function that returns the n-th iterate of the "times 2 plus a constant" function with regard to composition. (Contributed by AV, 7-May-2024)

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

Proof

Step Hyp Ref Expression
1 itcovalt2.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 · 𝑛 ) + 𝐶 ) )
2 fveq2 ⊢ ( 𝑥 = 0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 0 ) )
3 oveq2 ⊢ ( 𝑥 = 0 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 0 ) )
4 3 oveq2d ⊢ ( 𝑥 = 0 → ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) = ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) )
5 4 oveq1d ⊢ ( 𝑥 = 0 → ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) = ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) − 𝐶 ) )
6 5 mpteq2dv ⊢ ( 𝑥 = 0 → ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) − 𝐶 ) ) )
7 2 6 eqeq12d ⊢ ( 𝑥 = 0 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) − 𝐶 ) ) ) )
8 7 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) ) ↔ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) − 𝐶 ) ) ) ) )
9 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) )
10 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 𝑦 ) )
11 10 oveq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) = ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) )
12 11 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) = ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) )
13 12 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) )
14 9 13 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) )
15 14 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) ) ↔ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) ) )
16 fveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) )
17 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 2 ↑ 𝑥 ) = ( 2 ↑ ( 𝑦 + 1 ) ) )
18 17 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) = ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) )
19 18 oveq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) = ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) )
20 19 mpteq2dv ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) )
21 16 20 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) ) )
22 21 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) ) ↔ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) ) ) )
23 fveq2 ⊢ ( 𝑥 = 𝐼 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) )
24 oveq2 ⊢ ( 𝑥 = 𝐼 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 𝐼 ) )
25 24 oveq2d ⊢ ( 𝑥 = 𝐼 → ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) = ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝐼 ) ) )
26 25 oveq1d ⊢ ( 𝑥 = 𝐼 → ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) = ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝐼 ) ) − 𝐶 ) )
27 26 mpteq2dv ⊢ ( 𝑥 = 𝐼 → ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝐼 ) ) − 𝐶 ) ) )
28 23 27 eqeq12d ⊢ ( 𝑥 = 𝐼 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝐼 ) ) − 𝐶 ) ) ) )
29 28 imbi2d ⊢ ( 𝑥 = 𝐼 → ( ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑥 ) ) − 𝐶 ) ) ) ↔ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝐼 ) ) − 𝐶 ) ) ) ) )
30 1 itcovalt2lem1 ⊢ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 0 ) ) − 𝐶 ) ) )
31 pm2.27 ⊢ ( 𝐶 ∈ ℕ0 → ( ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) )
32 31 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) )
33 1 itcovalt2lem2 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) ) )
34 32 33 syld ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) ) )
35 34 ex ⊢ ( 𝑦 ∈ ℕ0 → ( 𝐶 ∈ ℕ0 → ( ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) ) ) )
36 35 com23 ⊢ ( 𝑦 ∈ ℕ0 → ( ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝑦 ) ) − 𝐶 ) ) ) → ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ ( 𝑦 + 1 ) ) ) − 𝐶 ) ) ) ) )
37 8 15 22 29 30 36 nn0ind ⊢ ( 𝐼 ∈ ℕ0 → ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝐼 ) ) − 𝐶 ) ) ) )
38 37 imp ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 𝐶 ) · ( 2 ↑ 𝐼 ) ) − 𝐶 ) ) )