Metamath Proof Explorer


Theorem 2wlkdlem10

Description: Lemma 10 for 3wlkd . (Contributed by AV, 14-Feb-2021)

Ref Expression
Hypotheses 2wlkd.p P = ⟨“ ABC ”⟩
2wlkd.f F = ⟨“ JK ”⟩
2wlkd.s φ A V B V C V
2wlkd.n φ A B B C
2wlkd.e φ A B I J B C I K
Assertion 2wlkdlem10 φ k 0 ..^ F P k P k + 1 I F k

Proof

Step Hyp Ref Expression
1 2wlkd.p P = ⟨“ ABC ”⟩
2 2wlkd.f F = ⟨“ JK ”⟩
3 2wlkd.s φ A V B V C V
4 2wlkd.n φ A B B C
5 2wlkd.e φ A B I J B C I K
6 1 2 3 4 5 2wlkdlem9 φ A B I F 0 B C I F 1
7 1 2 3 2wlkdlem3 φ P 0 = A P 1 = B P 2 = C
8 preq12 P 0 = A P 1 = B P 0 P 1 = A B
9 8 3adant3 P 0 = A P 1 = B P 2 = C P 0 P 1 = A B
10 9 sseq1d P 0 = A P 1 = B P 2 = C P 0 P 1 I F 0 A B I F 0
11 preq12 P 1 = B P 2 = C P 1 P 2 = B C
12 11 3adant1 P 0 = A P 1 = B P 2 = C P 1 P 2 = B C
13 12 sseq1d P 0 = A P 1 = B P 2 = C P 1 P 2 I F 1 B C I F 1
14 10 13 anbi12d P 0 = A P 1 = B P 2 = C P 0 P 1 I F 0 P 1 P 2 I F 1 A B I F 0 B C I F 1
15 7 14 syl φ P 0 P 1 I F 0 P 1 P 2 I F 1 A B I F 0 B C I F 1
16 6 15 mpbird φ P 0 P 1 I F 0 P 1 P 2 I F 1
17 1 2 2wlkdlem2 0 ..^ F = 0 1
18 17 raleqi k 0 ..^ F P k P k + 1 I F k k 0 1 P k P k + 1 I F k
19 c0ex 0 V
20 1ex 1 V
21 fveq2 k = 0 P k = P 0
22 fv0p1e1 k = 0 P k + 1 = P 1
23 21 22 preq12d k = 0 P k P k + 1 = P 0 P 1
24 2fveq3 k = 0 I F k = I F 0
25 23 24 sseq12d k = 0 P k P k + 1 I F k P 0 P 1 I F 0
26 fveq2 k = 1 P k = P 1
27 oveq1 k = 1 k + 1 = 1 + 1
28 1p1e2 1 + 1 = 2
29 27 28 eqtrdi k = 1 k + 1 = 2
30 29 fveq2d k = 1 P k + 1 = P 2
31 26 30 preq12d k = 1 P k P k + 1 = P 1 P 2
32 2fveq3 k = 1 I F k = I F 1
33 31 32 sseq12d k = 1 P k P k + 1 I F k P 1 P 2 I F 1
34 19 20 25 33 ralpr k 0 1 P k P k + 1 I F k P 0 P 1 I F 0 P 1 P 2 I F 1
35 18 34 bitri k 0 ..^ F P k P k + 1 I F k P 0 P 1 I F 0 P 1 P 2 I F 1
36 16 35 sylibr φ k 0 ..^ F P k P k + 1 I F k