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	$$⊢F=\left(n\in {\mathbb{N}}_0⟼2n+C\right)$$
Assertion	itcovalt2	$$⊢\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⟼\left(n+C\right)2^I-C\right)$$

Proof

Step	Hyp	Ref	Expression
1		itcovalt2.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼2n+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 2^x=2^0$$
4	3	oveq2d	$$⊢x=0\to \left(n+C\right)2^x=\left(n+C\right)2^0$$
5	4	oveq1d	$$⊢x=0\to \left(n+C\right)2^x-C=\left(n+C\right)2^0-C$$
6	5	mpteq2dv	$$⊢x=0\to \left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^0-C\right)$$
7	2 6	eqeq12d	$$⊢x=0\to \left(\mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)\leftrightarrow \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^0-C\right)\right)$$
8	7	imbi2d	$$⊢x=0\to \left(\left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)\right)\leftrightarrow \left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^0-C\right)\right)\right)$$
9		fveq2	$$⊢x=y\to \mathrm{IterComp}\left(F\right)\left(x\right)=\mathrm{IterComp}\left(F\right)\left(y\right)$$
10		oveq2	$$⊢x=y\to 2^x=2^y$$
11	10	oveq2d	$$⊢x=y\to \left(n+C\right)2^x=\left(n+C\right)2^y$$
12	11	oveq1d	$$⊢x=y\to \left(n+C\right)2^x-C=\left(n+C\right)2^y-C$$
13	12	mpteq2dv	$$⊢x=y\to \left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)$$
14	9 13	eqeq12d	$$⊢x=y\to \left(\mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)\leftrightarrow \mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)\right)$$
15	14	imbi2d	$$⊢x=y\to \left(\left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)\right)\leftrightarrow \left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)\right)\right)$$
16		fveq2	$$⊢x=y+1\to \mathrm{IterComp}\left(F\right)\left(x\right)=\mathrm{IterComp}\left(F\right)\left(y+1\right)$$
17		oveq2	$$⊢x=y+1\to 2^x=2^{y+1}$$
18	17	oveq2d	$$⊢x=y+1\to \left(n+C\right)2^x=\left(n+C\right)2^{y+1}$$
19	18	oveq1d	$$⊢x=y+1\to \left(n+C\right)2^x-C=\left(n+C\right)2^{y+1}-C$$
20	19	mpteq2dv	$$⊢x=y+1\to \left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^{y+1}-C\right)$$
21	16 20	eqeq12d	$$⊢x=y+1\to \left(\mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)\leftrightarrow \mathrm{IterComp}\left(F\right)\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^{y+1}-C\right)\right)$$
22	21	imbi2d	$$⊢x=y+1\to \left(\left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)\right)\leftrightarrow \left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^{y+1}-C\right)\right)\right)$$
23		fveq2	$$⊢x=I\to \mathrm{IterComp}\left(F\right)\left(x\right)=\mathrm{IterComp}\left(F\right)\left(I\right)$$
24		oveq2	$$⊢x=I\to 2^x=2^I$$
25	24	oveq2d	$$⊢x=I\to \left(n+C\right)2^x=\left(n+C\right)2^I$$
26	25	oveq1d	$$⊢x=I\to \left(n+C\right)2^x-C=\left(n+C\right)2^I-C$$
27	26	mpteq2dv	$$⊢x=I\to \left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^I-C\right)$$
28	23 27	eqeq12d	$$⊢x=I\to \left(\mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)\leftrightarrow \mathrm{IterComp}\left(F\right)\left(I\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^I-C\right)\right)$$
29	28	imbi2d	$$⊢x=I\to \left(\left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(x\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^x-C\right)\right)\leftrightarrow \left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(I\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^I-C\right)\right)\right)$$
30	1	itcovalt2lem1	$$⊢C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^0-C\right)$$
31		pm2.27	$$⊢C\in {\mathbb{N}}_0\to \left(\left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)\right)\to \mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)\right)$$
32	31	adantl	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(\left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)\right)\to \mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)\right)$$
33	1	itcovalt2lem2	$$⊢\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⟼\left(n+C\right)2^y-C\right)\to \mathrm{IterComp}\left(F\right)\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^{y+1}-C\right)\right)$$
34	32 33	syld	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(\left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)\right)\to \mathrm{IterComp}\left(F\right)\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^{y+1}-C\right)\right)$$
35	34	ex	$$⊢y\in {\mathbb{N}}_0\to \left(C\in {\mathbb{N}}_0\to \left(\left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)\right)\to \mathrm{IterComp}\left(F\right)\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^{y+1}-C\right)\right)\right)$$
36	35	com23	$$⊢y\in {\mathbb{N}}_0\to \left(\left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(y\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)\right)\to \left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(y+1\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^{y+1}-C\right)\right)\right)$$
37	8 15 22 29 30 36	nn0ind	$$⊢I\in {\mathbb{N}}_0\to \left(C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(I\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^I-C\right)\right)$$
38	37	imp	$$⊢\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⟼\left(n+C\right)2^I-C\right)$$