Metamath Proof Explorer

Theorem itcovalt2lem2

Description: Lemma 2 for itcovalt2 : induction step. (Contributed by AV, 7-May-2024)

Ref Expression
Hypothesis itcovalt2.f 
|- F = ( n e. NN0 |-> ( ( 2 x. n ) + C ) )
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 itcovalt2.f 
 |-  F = ( n e. NN0 |-> ( ( 2 x. n ) + C ) )
2 nn0ex 
 |-  NN0 e. _V
3 2 mptex 
 |-  ( n e. NN0 |-> ( ( 2 x. n ) + C ) ) e. _V
4 1 3 eqeltri 
 |-  F e. _V
5 simpl 
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> y e. NN0 )
6 simpr 
 |-  ( ( ( y 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 ) ) )
7 itcovalsucov 
 |-  ( ( F e. _V /\ y e. NN0 /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) )
8 4 5 6 7 mp3an2ani 
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) )
9 2nn 
 |-  2 e. NN
10 9 a1i 
 |-  ( y e. NN0 -> 2 e. NN )
11 id 
 |-  ( y e. NN0 -> y e. NN0 )
12 10 11 nnexpcld 
 |-  ( y e. NN0 -> ( 2 ^ y ) e. NN )
13 itcovalt2lem2lem1 
 |-  ( ( ( ( 2 ^ y ) e. NN /\ C e. NN0 ) /\ n e. NN0 ) -> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) e. NN0 )
14 12 13 sylanl1 
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) e. NN0 )
15 eqidd 
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) )
16 oveq2 
 |-  ( n = m -> ( 2 x. n ) = ( 2 x. m ) )
17 16 oveq1d 
 |-  ( n = m -> ( ( 2 x. n ) + C ) = ( ( 2 x. m ) + C ) )
18 17 cbvmptv 
 |-  ( n e. NN0 |-> ( ( 2 x. n ) + C ) ) = ( m e. NN0 |-> ( ( 2 x. m ) + C ) )
19 1 18 eqtri 
 |-  F = ( m e. NN0 |-> ( ( 2 x. m ) + C ) )
20 19 a1i 
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> F = ( m e. NN0 |-> ( ( 2 x. m ) + C ) ) )
21 oveq2 
 |-  ( m = ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) -> ( 2 x. m ) = ( 2 x. ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) )
22 21 oveq1d 
 |-  ( m = ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) -> ( ( 2 x. m ) + C ) = ( ( 2 x. ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) + C ) )
23 14 15 20 22 fmptco 
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( F o. ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) = ( n e. NN0 |-> ( ( 2 x. ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) + C ) ) )
24 itcovalt2lem2lem2 
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ n e. NN0 ) -> ( ( 2 x. ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) + C ) = ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) )
25 24 mpteq2dva 
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( n e. NN0 |-> ( ( 2 x. ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) + C ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) )
26 23 25 eqtrd 
 |-  ( ( y e. NN0 /\ C e. NN0 ) -> ( F o. ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) )
27 26 adantr 
 |-  ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( F o. ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) )
28 8 27 eqtrd 
 |-  ( ( ( 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 ) ) )
29 28 ex 
 |-  ( ( 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 ) ) ) )