Step |
Hyp |
Ref |
Expression |
1 |
|
itcovalpc.f |
|
2 |
|
nn0ex |
|
3 |
|
ovexd |
|
4 |
3
|
rgen |
|
5 |
1
|
itcoval0mpt |
Could not format ( ( NN0 e. _V /\ A. n e. NN0 ( n + C ) e. _V ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) ) : No typesetting found for |- ( ( NN0 e. _V /\ A. n e. NN0 ( n + C ) e. _V ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) ) with typecode |- |
6 |
2 4 5
|
mp2an |
Could not format ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) : No typesetting found for |- ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) with typecode |- |
7 |
|
nn0cn |
|
8 |
7
|
mul01d |
|
9 |
8
|
adantr |
|
10 |
9
|
oveq2d |
|
11 |
|
nn0cn |
|
12 |
11
|
addid1d |
|
13 |
12
|
adantl |
|
14 |
10 13
|
eqtr2d |
|
15 |
14
|
mpteq2dva |
|
16 |
6 15
|
syl5eq |
Could not format ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) ) : No typesetting found for |- ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) ) with typecode |- |