Metamath Proof Explorer

Theorem itcovalt2lem1

Description: Lemma 1 for itcovalt2 : induction basis. (Contributed by AV, 5-May-2024)

Ref Expression
Hypothesis itcovalt2.f 
|- F = ( n e. NN0 |-> ( ( 2 x. n ) + C ) )
Assertion itcovalt2lem1 
|- ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) )

Proof

Step Hyp Ref Expression
1 itcovalt2.f 
 |-  F = ( n e. NN0 |-> ( ( 2 x. n ) + C ) )
2 nn0ex 
 |-  NN0 e. _V
3 ovexd 
 |-  ( n e. NN0 -> ( ( 2 x. n ) + C ) e. _V )
4 3 rgen 
 |-  A. n e. NN0 ( ( 2 x. n ) + C ) e. _V
5 2 4 pm3.2i 
 |-  ( NN0 e. _V /\ A. n e. NN0 ( ( 2 x. n ) + C ) e. _V )
6 1 itcoval0mpt 
 |-  ( ( NN0 e. _V /\ A. n e. NN0 ( ( 2 x. n ) + C ) e. _V ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) )
7 5 6 mp1i 
 |-  ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) )
8 simpr 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> n e. NN0 )
9 8 nn0cnd 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> n e. CC )
10 simpl 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> C e. NN0 )
11 10 nn0cnd 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> C e. CC )
12 2nn0 
 |-  2 e. NN0
13 12 numexp0 
 |-  ( 2 ^ 0 ) = 1
14 13 a1i 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> ( 2 ^ 0 ) = 1 )
15 14 oveq2d 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> ( ( n + C ) x. ( 2 ^ 0 ) ) = ( ( n + C ) x. 1 ) )
16 8 10 nn0addcld 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> ( n + C ) e. NN0 )
17 16 nn0cnd 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> ( n + C ) e. CC )
18 17 mulid1d 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> ( ( n + C ) x. 1 ) = ( n + C ) )
19 15 18 eqtrd 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> ( ( n + C ) x. ( 2 ^ 0 ) ) = ( n + C ) )
20 9 11 19 mvrraddd 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) = n )
21 20 eqcomd 
 |-  ( ( C e. NN0 /\ n e. NN0 ) -> n = ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) )
22 21 mpteq2dva 
 |-  ( C e. NN0 -> ( n e. NN0 |-> n ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) )
23 7 22 eqtrd 
 |-  ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) )