Metamath Proof Explorer


Theorem 2pthdlem1

Description: Lemma 1 for 2pthd . (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
Assertion 2pthdlem1 φ k 0 ..^ P j 1 ..^ F k j P k P j

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 1 2 3 2wlkdlem3 φ P 0 = A P 1 = B P 2 = C
6 simpl P 0 = A P 1 = B P 0 = A
7 simpr P 0 = A P 1 = B P 1 = B
8 6 7 neeq12d P 0 = A P 1 = B P 0 P 1 A B
9 8 bicomd P 0 = A P 1 = B A B P 0 P 1
10 9 3adant3 P 0 = A P 1 = B P 2 = C A B P 0 P 1
11 10 biimpcd A B P 0 = A P 1 = B P 2 = C P 0 P 1
12 11 adantr A B B C P 0 = A P 1 = B P 2 = C P 0 P 1
13 12 imp A B B C P 0 = A P 1 = B P 2 = C P 0 P 1
14 13 a1d A B B C P 0 = A P 1 = B P 2 = C 0 1 P 0 P 1
15 eqid 1 = 1
16 eqneqall 1 = 1 1 1 P 1 P 1
17 15 16 mp1i A B B C P 0 = A P 1 = B P 2 = C 1 1 P 1 P 1
18 simpr P 1 = B P 2 = C P 2 = C
19 simpl P 1 = B P 2 = C P 1 = B
20 18 19 neeq12d P 1 = B P 2 = C P 2 P 1 C B
21 necom C B B C
22 20 21 bitr2di P 1 = B P 2 = C B C P 2 P 1
23 22 3adant1 P 0 = A P 1 = B P 2 = C B C P 2 P 1
24 23 biimpcd B C P 0 = A P 1 = B P 2 = C P 2 P 1
25 24 adantl A B B C P 0 = A P 1 = B P 2 = C P 2 P 1
26 25 imp A B B C P 0 = A P 1 = B P 2 = C P 2 P 1
27 26 a1d A B B C P 0 = A P 1 = B P 2 = C 2 1 P 2 P 1
28 14 17 27 3jca A B B C P 0 = A P 1 = B P 2 = C 0 1 P 0 P 1 1 1 P 1 P 1 2 1 P 2 P 1
29 4 5 28 syl2anc φ 0 1 P 0 P 1 1 1 P 1 P 1 2 1 P 2 P 1
30 1 fveq2i P = ⟨“ ABC ”⟩
31 s3len ⟨“ ABC ”⟩ = 3
32 30 31 eqtri P = 3
33 32 oveq2i 0 ..^ P = 0 ..^ 3
34 fzo0to3tp 0 ..^ 3 = 0 1 2
35 33 34 eqtri 0 ..^ P = 0 1 2
36 35 raleqi k 0 ..^ P k 1 P k P 1 k 0 1 2 k 1 P k P 1
37 c0ex 0 V
38 1ex 1 V
39 2ex 2 V
40 neeq1 k = 0 k 1 0 1
41 fveq2 k = 0 P k = P 0
42 41 neeq1d k = 0 P k P 1 P 0 P 1
43 40 42 imbi12d k = 0 k 1 P k P 1 0 1 P 0 P 1
44 neeq1 k = 1 k 1 1 1
45 fveq2 k = 1 P k = P 1
46 45 neeq1d k = 1 P k P 1 P 1 P 1
47 44 46 imbi12d k = 1 k 1 P k P 1 1 1 P 1 P 1
48 neeq1 k = 2 k 1 2 1
49 fveq2 k = 2 P k = P 2
50 49 neeq1d k = 2 P k P 1 P 2 P 1
51 48 50 imbi12d k = 2 k 1 P k P 1 2 1 P 2 P 1
52 37 38 39 43 47 51 raltp k 0 1 2 k 1 P k P 1 0 1 P 0 P 1 1 1 P 1 P 1 2 1 P 2 P 1
53 36 52 bitri k 0 ..^ P k 1 P k P 1 0 1 P 0 P 1 1 1 P 1 P 1 2 1 P 2 P 1
54 29 53 sylibr φ k 0 ..^ P k 1 P k P 1
55 2 fveq2i F = ⟨“ JK ”⟩
56 s2len ⟨“ JK ”⟩ = 2
57 55 56 eqtri F = 2
58 57 oveq2i 1 ..^ F = 1 ..^ 2
59 fzo12sn 1 ..^ 2 = 1
60 58 59 eqtri 1 ..^ F = 1
61 60 raleqi j 1 ..^ F k j P k P j j 1 k j P k P j
62 neeq2 j = 1 k j k 1
63 fveq2 j = 1 P j = P 1
64 63 neeq2d j = 1 P k P j P k P 1
65 62 64 imbi12d j = 1 k j P k P j k 1 P k P 1
66 38 65 ralsn j 1 k j P k P j k 1 P k P 1
67 61 66 bitri j 1 ..^ F k j P k P j k 1 P k P 1
68 67 ralbii k 0 ..^ P j 1 ..^ F k j P k P j k 0 ..^ P k 1 P k P 1
69 54 68 sylibr φ k 0 ..^ P j 1 ..^ F k j P k P j