Metamath Proof Explorer


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 = n 0 n + C
Assertion itcovalpc I 0 C 0 IterComp F I = n 0 n + C I

Proof

Step Hyp Ref Expression
1 itcovalpc.f F = n 0 n + C
2 fveq2 x = 0 IterComp F x = IterComp F 0
3 oveq2 x = 0 C x = C 0
4 3 oveq2d x = 0 n + C x = n + C 0
5 4 mpteq2dv x = 0 n 0 n + C x = n 0 n + C 0
6 2 5 eqeq12d x = 0 IterComp F x = n 0 n + C x IterComp F 0 = n 0 n + C 0
7 fveq2 x = y IterComp F x = IterComp F y
8 oveq2 x = y C x = C y
9 8 oveq2d x = y n + C x = n + C y
10 9 mpteq2dv x = y n 0 n + C x = n 0 n + C y
11 7 10 eqeq12d x = y IterComp F x = n 0 n + C x IterComp F y = n 0 n + C y
12 fveq2 x = y + 1 IterComp F x = IterComp F y + 1
13 oveq2 x = y + 1 C x = C y + 1
14 13 oveq2d x = y + 1 n + C x = n + C y + 1
15 14 mpteq2dv x = y + 1 n 0 n + C x = n 0 n + C y + 1
16 12 15 eqeq12d x = y + 1 IterComp F x = n 0 n + C x IterComp F y + 1 = n 0 n + C y + 1
17 fveq2 x = I IterComp F x = IterComp F I
18 oveq2 x = I C x = C I
19 18 oveq2d x = I n + C x = n + C I
20 19 mpteq2dv x = I n 0 n + C x = n 0 n + C I
21 17 20 eqeq12d x = I IterComp F x = n 0 n + C x IterComp F I = n 0 n + C I
22 1 itcovalpclem1 C 0 IterComp F 0 = n 0 n + C 0
23 1 itcovalpclem2 y 0 C 0 IterComp F y = n 0 n + C y IterComp F y + 1 = n 0 n + C y + 1
24 23 ancoms C 0 y 0 IterComp F y = n 0 n + C y IterComp F y + 1 = n 0 n + C y + 1
25 24 imp C 0 y 0 IterComp F y = n 0 n + C y IterComp F y + 1 = n 0 n + C y + 1
26 6 11 16 21 22 25 nn0indd C 0 I 0 IterComp F I = n 0 n + C I
27 26 ancoms I 0 C 0 IterComp F I = n 0 n + C I