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 C 0 IterComp F 0 = n 0 n + C 0

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 0 V n 0 n + C V IterComp F 0 = n 0 n
6 2 4 5 mp2an IterComp F 0 = n 0 n
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 addridd 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 eqtrid C 0 IterComp F 0 = n 0 n + C 0