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

Proof

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