Metamath Proof Explorer

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 = ( n e. NN0 |-> ( ( 2 x. n ) + C ) )
Assertion itcovalt2 
|- ( ( I e. NN0 /\ C e. NN0 ) -> ( ( IterComp ` F ) ` I ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ I ) ) - C ) ) )

Proof

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