Description: Lemma 1 for itcovalpc : induction basis. (Contributed by AV, 4-May-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | itcovalpc.f | |
|
Assertion | itcovalpclem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | itcovalpc.f | |
|
2 | nn0ex | |
|
3 | ovexd | |
|
4 | 3 | rgen | |
5 | 1 | itcoval0mpt | |
6 | 2 4 5 | mp2an | |
7 | nn0cn | |
|
8 | 7 | mul01d | |
9 | 8 | adantr | |
10 | 9 | oveq2d | |
11 | nn0cn | |
|
12 | 11 | addridd | |
13 | 12 | adantl | |
14 | 10 13 | eqtr2d | |
15 | 14 | mpteq2dva | |
16 | 6 15 | eqtrid | |