Metamath Proof Explorer


Theorem itcovalpclem1

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

Ref Expression
Hypothesis itcovalpc.f F=n0n+C
Assertion itcovalpclem1 C0IterCompF0=n0n+C0

Proof

Step Hyp Ref Expression
1 itcovalpc.f F=n0n+C
2 nn0ex 0V
3 ovexd n0n+CV
4 3 rgen n0n+CV
5 1 itcoval0mpt 0Vn0n+CVIterCompF0=n0n
6 2 4 5 mp2an IterCompF0=n0n
7 nn0cn C0C
8 7 mul01d C0C0=0
9 8 adantr C0n0C0=0
10 9 oveq2d C0n0n+C0=n+0
11 nn0cn n0n
12 11 addridd n0n+0=n
13 12 adantl C0n0n+0=n
14 10 13 eqtr2d C0n0n=n+C0
15 14 mpteq2dva C0n0n=n0n+C0
16 6 15 eqtrid C0IterCompF0=n0n+C0