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	$$⊢F=\left(n\in {\mathbb{N}}_0⟼n+C\right)$$
Assertion	itcovalpc	$$⊢\left(I\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \mathrm{IterComp}\left(F\right)\left(I\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot \mathrm{<mi\; mathcolor="\#808">I</mi>}\right)$$

Proof

Step	Hyp	Ref	Expression
1		itcovalpc.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼n+C\right)$$
2		fveq2	$$⊢x=0\to \mathrm{IterComp}\left(F\right)\left(x\right)=\mathrm{IterComp}\left(F\right)\left(0\right)$$
3		oveq2	$$⊢x=0\to Cx=C\cdot 0$$
4	3	oveq2d	$$⊢x=0\to n+Cx=n+C\cdot 0$$
5	4	mpteq2dv	$$⊢x=0\to \left(n\in {\mathbb{N}}_0⟼n+Cx\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot 0\right)$$
6	2 5	eqeq12d	$$⊢x=0\to \left(\mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼n+Cx\right)\leftrightarrow \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot 0\right)\right)$$
7		fveq2	$$⊢x=y\to \mathrm{IterComp}\left(F\right)\left(x\right)=\mathrm{IterComp}\left(F\right)\left(y\right)$$
8		oveq2	$$⊢x=y\to Cx=Cy$$
9	8	oveq2d	$$⊢x=y\to n+Cx=n+Cy$$
10	9	mpteq2dv	$$⊢x=y\to \left(n\in {\mathbb{N}}_0⟼n+Cx\right)=\left(n\in {\mathbb{N}}_0⟼n+Cy\right)$$
11	7 10	eqeq12d	$$⊢x=y\to \left(\mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼n+Cx\right)\leftrightarrow \mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼n+Cy\right)\right)$$
12		fveq2	$$⊢x=y+1\to \mathrm{IterComp}\left(F\right)\left(x\right)=\mathrm{IterComp}\left(F\right)\left(y+1\right)$$
13		oveq2	$$⊢x=y+1\to Cx=C\left(y+1\right)$$
14	13	oveq2d	$$⊢x=y+1\to n+Cx=n+C\left(y+1\right)$$
15	14	mpteq2dv	$$⊢x=y+1\to \left(n\in {\mathbb{N}}_0⟼n+Cx\right)=\left(n\in {\mathbb{N}}_0⟼n+C\left(y+1\right)\right)$$
16	12 15	eqeq12d	$$⊢x=y+1\to \left(\mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼n+Cx\right)\leftrightarrow \mathrm{IterComp}\left(F\right)\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼n+C\left(y+1\right)\right)\right)$$
17		fveq2	$$⊢x=I\to \mathrm{IterComp}\left(F\right)\left(x\right)=\mathrm{IterComp}\left(F\right)\left(I\right)$$
18		oveq2	$$⊢x=I\to Cx=C\cdot \mathrm{<mi\; mathcolor="\#808">I</mi>}$$
19	18	oveq2d	$$⊢x=I\to n+Cx=n+C\cdot \mathrm{<mi\; mathcolor="\#808">I</mi>}$$
20	19	mpteq2dv	$$⊢x=I\to \left(n\in {\mathbb{N}}_0⟼n+Cx\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot \mathrm{<mi\; mathcolor="\#808">I</mi>}\right)$$
21	17 20	eqeq12d	$$⊢x=I\to \left(\mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼n+Cx\right)\leftrightarrow \mathrm{IterComp}\left(F\right)\left(I\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot \mathrm{<mi\; mathcolor="\#808">I</mi>}\right)\right)$$
22	1	itcovalpclem1	$$⊢C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot 0\right)$$
23	1	itcovalpclem2	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(\mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼n+Cy\right)\to \mathrm{IterComp}\left(F\right)\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼n+C\left(y+1\right)\right)\right)$$
24	23	ancoms	$$⊢\left(C\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to \left(\mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼n+Cy\right)\to \mathrm{IterComp}\left(F\right)\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼n+C\left(y+1\right)\right)\right)$$
25	24	imp	$$⊢\left(\left(C\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\wedge \mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼n+Cy\right)\right)\to \mathrm{IterComp}\left(F\right)\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼n+C\left(y+1\right)\right)$$
26	6 11 16 21 22 25	nn0indd	$$⊢\left(C\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to \mathrm{IterComp}\left(F\right)\left(I\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot \mathrm{<mi\; mathcolor="\#808">I</mi>}\right)$$
27	26	ancoms	$$⊢\left(I\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \mathrm{IterComp}\left(F\right)\left(I\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot \mathrm{<mi\; mathcolor="\#808">I</mi>}\right)$$