Metamath Proof Explorer


Theorem itcovalpclem1

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

Ref Expression
Hypothesis itcovalpc.f F = n 0 n + C
Assertion itcovalpclem1 Could not format assertion : No typesetting found for |- ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 itcovalpc.f F = n 0 n + C
2 nn0ex 0 V
3 ovexd n 0 n + C V
4 3 rgen n 0 n + C V
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 C 0 C
8 7 mul01d C 0 C 0 = 0
9 8 adantr C 0 n 0 C 0 = 0
10 9 oveq2d C 0 n 0 n + C 0 = n + 0
11 nn0cn n 0 n
12 11 addid1d n 0 n + 0 = n
13 12 adantl C 0 n 0 n + 0 = n
14 10 13 eqtr2d C 0 n 0 n = n + C 0
15 14 mpteq2dva C 0 n 0 n = n 0 n + C 0
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 |-