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

Proof

Step	Hyp	Ref	Expression
1		itcovalpc.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼n+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 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	Could not format ( x = 0 -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) ) ) : No typesetting found for |- ( x = 0 -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) ) ) with typecode |-
7		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 |-
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	Could not format ( x = y -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) ) : No typesetting found for |- ( x = y -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) ) with typecode |-
12		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 |-
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	Could not format ( x = ( y + 1 ) -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) : No typesetting found for |- ( x = ( y + 1 ) -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) with typecode |-
17		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 |-
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	Could not format ( x = I -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( n + ( C x. I ) ) ) ) ) : No typesetting found for |- ( x = I -> ( ( ( IterComp ` F ) ` x ) = ( n e. NN0 |-> ( n + ( C x. x ) ) ) <-> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( n + ( C x. I ) ) ) ) ) with typecode |-
22	1	itcovalpclem1	Could not format ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) ) : No typesetting found for |- ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) ) with typecode |-
23	1	itcovalpclem2	Could not format ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) : No typesetting found for |- ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) with typecode |-
24	23	ancoms	Could not format ( ( C e. NN0 /\ y e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) : No typesetting found for |- ( ( C e. NN0 /\ y e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) with typecode |-
25	24	imp	Could not format ( ( ( C e. NN0 /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) : No typesetting found for |- ( ( ( C e. NN0 /\ y e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) with typecode |-
26	6 11 16 21 22 25	nn0indd	Could not format ( ( C e. NN0 /\ I e. NN0 ) -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( n + ( C x. I ) ) ) ) : No typesetting found for |- ( ( C e. NN0 /\ I e. NN0 ) -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( n + ( C x. I ) ) ) ) with typecode |-
27	26	ancoms	Could not format ( ( I e. NN0 /\ C e. NN0 ) -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( n + ( C x. I ) ) ) ) : No typesetting found for |- ( ( I e. NN0 /\ C e. NN0 ) -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( n + ( C x. I ) ) ) ) with typecode |-