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	Could not format assertion : No typesetting found for |- ( ( I e. NN0 /\ C e. NN0 ) -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ I ) ) - C ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		itcovalt2.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼2n+C\right)$$
2		fveq2	Could not format ( x = 0 -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` 0 ) ) : No typesetting found for |- ( x = 0 -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` 0 ) ) with typecode |-
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	Could not format ( x = 0 -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) <-> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) ) ) : No typesetting found for |- ( x = 0 -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) <-> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) ) ) with typecode |-
8	7	imbi2d	Could not format ( x = 0 -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) ) <-> ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) ) ) ) : No typesetting found for |- ( x = 0 -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) ) <-> ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) ) ) ) with typecode |-
9		fveq2	Could not format ( x = y -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` y ) ) : No typesetting found for |- ( x = y -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` y ) ) with typecode |-
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	Could not format ( x = y -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) <-> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) : No typesetting found for |- ( x = y -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) <-> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) with typecode |-
15	14	imbi2d	Could not format ( x = y -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) ) <-> ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) ) : No typesetting found for |- ( x = y -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) ) <-> ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) ) with typecode |-
16		fveq2	Could not format ( x = ( y + 1 ) -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` ( y + 1 ) ) ) : No typesetting found for |- ( x = ( y + 1 ) -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` ( y + 1 ) ) ) with typecode |-
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	Could not format ( x = ( y + 1 ) -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) <-> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) : No typesetting found for |- ( x = ( y + 1 ) -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) <-> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) with typecode |-
22	21	imbi2d	Could not format ( x = ( y + 1 ) -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) ) <-> ( C e. NN0 -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) ) : No typesetting found for |- ( x = ( y + 1 ) -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) ) <-> ( C e. NN0 -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) ) with typecode |-
23		fveq2	Could not format ( x = I -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` I ) ) : No typesetting found for |- ( x = I -> ( ( IterComp ` F ) ` x ) = ( ( IterComp ` F ) ` I ) ) with typecode |-
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	Could not format ( x = I -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) <-> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ I ) ) - C ) ) ) ) : No typesetting found for |- ( x = I -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) <-> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ I ) ) - C ) ) ) ) with typecode |-
29	28	imbi2d	Could not format ( x = I -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) ) <-> ( C e. NN0 -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ I ) ) - C ) ) ) ) ) : No typesetting found for |- ( x = I -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ x ) ) - C ) ) ) <-> ( C e. NN0 -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ I ) ) - C ) ) ) ) ) with typecode |-
30	1	itcovalt2lem1	Could not format ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) ) : No typesetting found for |- ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) ) with typecode |-
31		pm2.27	Could not format ( C e. NN0 -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) : No typesetting found for |- ( C e. NN0 -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) with typecode |-
32	31	adantl	Could not format ( ( y e. NN0 /\ C e. NN0 ) -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) : No typesetting found for |- ( ( y e. NN0 /\ C e. NN0 ) -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) with typecode |-
33	1	itcovalt2lem2	Could not format ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) : No typesetting found for |- ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) with typecode |-
34	32 33	syld	Could not format ( ( y e. NN0 /\ C e. NN0 ) -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) : No typesetting found for |- ( ( y e. NN0 /\ C e. NN0 ) -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) with typecode |-
35	34	ex	Could not format ( y e. NN0 -> ( C e. NN0 -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) ) : No typesetting found for |- ( y e. NN0 -> ( C e. NN0 -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) ) with typecode |-
36	35	com23	Could not format ( y e. NN0 -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( C e. NN0 -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) ) : No typesetting found for |- ( y e. NN0 -> ( ( C e. NN0 -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( C e. NN0 -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) ) with typecode |-
37	8 15 22 29 30 36	nn0ind	Could not format ( I e. NN0 -> ( C e. NN0 -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ I ) ) - C ) ) ) ) : No typesetting found for |- ( I e. NN0 -> ( C e. NN0 -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ I ) ) - C ) ) ) ) with typecode |-
38	37	imp	Could not format ( ( I e. NN0 /\ C e. NN0 ) -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ I ) ) - C ) ) ) : No typesetting found for |- ( ( I e. NN0 /\ C e. NN0 ) -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ I ) ) - C ) ) ) with typecode |-