Metamath Proof Explorer


Theorem itcovalt2lem2

Description: Lemma 2 for itcovalt2 : induction step. (Contributed by AV, 7-May-2024)

Ref Expression
Hypothesis itcovalt2.f F = n 0 2 n + C
Assertion itcovalt2lem2 y 0 C 0 IterComp F y = n 0 n + C 2 y C IterComp F y + 1 = n 0 n + C 2 y + 1 C

Proof

Step Hyp Ref Expression
1 itcovalt2.f F = n 0 2 n + C
2 nn0ex 0 V
3 2 mptex n 0 2 n + C V
4 1 3 eqeltri F V
5 simpl y 0 C 0 y 0
6 simpr y 0 C 0 IterComp F y = n 0 n + C 2 y C IterComp F y = n 0 n + C 2 y C
7 itcovalsucov F V y 0 IterComp F y = n 0 n + C 2 y C IterComp F y + 1 = F n 0 n + C 2 y C
8 4 5 6 7 mp3an2ani y 0 C 0 IterComp F y = n 0 n + C 2 y C IterComp F y + 1 = F n 0 n + C 2 y C
9 2nn 2
10 9 a1i y 0 2
11 id y 0 y 0
12 10 11 nnexpcld y 0 2 y
13 itcovalt2lem2lem1 2 y C 0 n 0 n + C 2 y C 0
14 12 13 sylanl1 y 0 C 0 n 0 n + C 2 y C 0
15 eqidd y 0 C 0 n 0 n + C 2 y C = n 0 n + C 2 y C
16 oveq2 n = m 2 n = 2 m
17 16 oveq1d n = m 2 n + C = 2 m + C
18 17 cbvmptv n 0 2 n + C = m 0 2 m + C
19 1 18 eqtri F = m 0 2 m + C
20 19 a1i y 0 C 0 F = m 0 2 m + C
21 oveq2 m = n + C 2 y C 2 m = 2 n + C 2 y C
22 21 oveq1d m = n + C 2 y C 2 m + C = 2 n + C 2 y C + C
23 14 15 20 22 fmptco y 0 C 0 F n 0 n + C 2 y C = n 0 2 n + C 2 y C + C
24 itcovalt2lem2lem2 y 0 C 0 n 0 2 n + C 2 y C + C = n + C 2 y + 1 C
25 24 mpteq2dva y 0 C 0 n 0 2 n + C 2 y C + C = n 0 n + C 2 y + 1 C
26 23 25 eqtrd y 0 C 0 F n 0 n + C 2 y C = n 0 n + C 2 y + 1 C
27 26 adantr y 0 C 0 IterComp F y = n 0 n + C 2 y C F n 0 n + C 2 y C = n 0 n + C 2 y + 1 C
28 8 27 eqtrd y 0 C 0 IterComp F y = n 0 n + C 2 y C IterComp F y + 1 = n 0 n + C 2 y + 1 C
29 28 ex y 0 C 0 IterComp F y = n 0 n + C 2 y C IterComp F y + 1 = n 0 n + C 2 y + 1 C