Theorem itcovalpc

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

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

Proof

Step	Hyp	Ref	Expression
1		itcovalpc.f	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 𝐶 ) )
2		fveq2	⊢ ( 𝑥 = 0 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 0 ) )
3		oveq2	⊢ ( 𝑥 = 0 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 0 ) )
4	3	oveq2d	⊢ ( 𝑥 = 0 → ( 𝑛 + ( 𝐶 · 𝑥 ) ) = ( 𝑛 + ( 𝐶 · 0 ) ) )
5	4	mpteq2dv	⊢ ( 𝑥 = 0 → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) )
6	2 5	eqeq12d	⊢ ( 𝑥 = 0 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) ) )
7		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) )
8		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) )
9	8	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑛 + ( 𝐶 · 𝑥 ) ) = ( 𝑛 + ( 𝐶 · 𝑦 ) ) )
10	9	mpteq2dv	⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) )
11	7 10	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) )
12		fveq2	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) )
13		oveq2	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐶 · 𝑥 ) = ( 𝐶 · ( 𝑦 + 1 ) ) )
14	13	oveq2d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑛 + ( 𝐶 · 𝑥 ) ) = ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) )
15	14	mpteq2dv	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
16	12 15	eqeq12d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) ) )
17		fveq2	⊢ ( 𝑥 = 𝐼 → ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) )
18		oveq2	⊢ ( 𝑥 = 𝐼 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝐼 ) )
19	18	oveq2d	⊢ ( 𝑥 = 𝐼 → ( 𝑛 + ( 𝐶 · 𝑥 ) ) = ( 𝑛 + ( 𝐶 · 𝐼 ) ) )
20	19	mpteq2dv	⊢ ( 𝑥 = 𝐼 → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝐼 ) ) ) )
21	17 20	eqeq12d	⊢ ( 𝑥 = 𝐼 → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑥 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑥 ) ) ) ↔ ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝐼 ) ) ) ) )
22	1	itcovalpclem1	⊢ ( 𝐶 ∈ ℕ0 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 0 ) ) ) )
23	1	itcovalpclem2	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) ) )
24	23	ancoms	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) ) )
25	24	imp	⊢ ( ( ( 𝐶 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( IterComp ‘ 𝐹 ) ‘ 𝑦 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝑦 ) ) ) ) → ( ( IterComp ‘ 𝐹 ) ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · ( 𝑦 + 1 ) ) ) ) )
26	6 11 16 21 22 25	nn0indd	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝐼 ) ) ) )
27	26	ancoms	⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( IterComp ‘ 𝐹 ) ‘ 𝐼 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + ( 𝐶 · 𝐼 ) ) ) )