Metamath Proof Explorer


Theorem clwlkclwwlklem2a1

Description: Lemma 1 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Assertion clwlkclwwlklem2a1 P Word V 2 P lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E i 0 ..^ P 1 P i P i + 1 ran E

Proof

Step Hyp Ref Expression
1 lencl P Word V P 0
2 nn0cn P 0 P
3 peano2cnm P P 1
4 3 subid1d P P - 1 - 0 = P 1
5 4 oveq1d P P 1 - 0 - 1 = P - 1 - 1
6 sub1m1 P P - 1 - 1 = P 2
7 5 6 eqtrd P P 1 - 0 - 1 = P 2
8 1 2 7 3syl P Word V P 1 - 0 - 1 = P 2
9 8 adantr P Word V 2 P P 1 - 0 - 1 = P 2
10 9 oveq2d P Word V 2 P 0 ..^ P 1 - 0 - 1 = 0 ..^ P 2
11 10 raleqdv P Word V 2 P i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E i 0 ..^ P 2 P i P i + 1 ran E
12 11 biimpcd i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P Word V 2 P i 0 ..^ P 2 P i P i + 1 ran E
13 12 adantr i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E P Word V 2 P i 0 ..^ P 2 P i P i + 1 ran E
14 13 adantl lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E P Word V 2 P i 0 ..^ P 2 P i P i + 1 ran E
15 14 impcom P Word V 2 P lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E i 0 ..^ P 2 P i P i + 1 ran E
16 lsw P Word V lastS P = P P 1
17 2m1e1 2 1 = 1
18 17 a1i P Word V 2 1 = 1
19 18 eqcomd P Word V 1 = 2 1
20 19 oveq2d P Word V P 1 = P 2 1
21 1 2 syl P Word V P
22 2cnd P Word V 2
23 1cnd P Word V 1
24 21 22 23 subsubd P Word V P 2 1 = P - 2 + 1
25 20 24 eqtrd P Word V P 1 = P - 2 + 1
26 25 fveq2d P Word V P P 1 = P P - 2 + 1
27 16 26 eqtrd P Word V lastS P = P P - 2 + 1
28 27 adantr P Word V 2 P lastS P = P P - 2 + 1
29 28 adantr P Word V 2 P lastS P = P 0 lastS P = P P - 2 + 1
30 eqeq1 lastS P = P 0 lastS P = P P - 2 + 1 P 0 = P P - 2 + 1
31 30 adantl P Word V 2 P lastS P = P 0 lastS P = P P - 2 + 1 P 0 = P P - 2 + 1
32 29 31 mpbid P Word V 2 P lastS P = P 0 P 0 = P P - 2 + 1
33 32 preq2d P Word V 2 P lastS P = P 0 P P 2 P 0 = P P 2 P P - 2 + 1
34 33 eleq1d P Word V 2 P lastS P = P 0 P P 2 P 0 ran E P P 2 P P - 2 + 1 ran E
35 34 biimpd P Word V 2 P lastS P = P 0 P P 2 P 0 ran E P P 2 P P - 2 + 1 ran E
36 35 ex P Word V 2 P lastS P = P 0 P P 2 P 0 ran E P P 2 P P - 2 + 1 ran E
37 36 com13 P P 2 P 0 ran E lastS P = P 0 P Word V 2 P P P 2 P P - 2 + 1 ran E
38 37 adantl i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E lastS P = P 0 P Word V 2 P P P 2 P P - 2 + 1 ran E
39 38 impcom lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E P Word V 2 P P P 2 P P - 2 + 1 ran E
40 39 impcom P Word V 2 P lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E P P 2 P P - 2 + 1 ran E
41 ovexd P Word V 2 P lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E P 2 V
42 fveq2 i = P 2 P i = P P 2
43 fvoveq1 i = P 2 P i + 1 = P P - 2 + 1
44 42 43 preq12d i = P 2 P i P i + 1 = P P 2 P P - 2 + 1
45 44 eleq1d i = P 2 P i P i + 1 ran E P P 2 P P - 2 + 1 ran E
46 45 ralunsn P 2 V i 0 ..^ P 2 P 2 P i P i + 1 ran E i 0 ..^ P 2 P i P i + 1 ran E P P 2 P P - 2 + 1 ran E
47 41 46 syl P Word V 2 P lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E i 0 ..^ P 2 P 2 P i P i + 1 ran E i 0 ..^ P 2 P i P i + 1 ran E P P 2 P P - 2 + 1 ran E
48 15 40 47 mpbir2and P Word V 2 P lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E i 0 ..^ P 2 P 2 P i P i + 1 ran E
49 1e2m1 1 = 2 1
50 49 a1i P Word V 1 = 2 1
51 50 oveq2d P Word V P 1 = P 2 1
52 51 24 eqtrd P Word V P 1 = P - 2 + 1
53 52 oveq2d P Word V 0 ..^ P 1 = 0 ..^ P - 2 + 1
54 53 adantr P Word V 2 P 0 ..^ P 1 = 0 ..^ P - 2 + 1
55 nn0re P 0 P
56 2re 2
57 56 a1i P 0 2
58 55 57 subge0d P 0 0 P 2 2 P
59 58 biimprd P 0 2 P 0 P 2
60 nn0z P 0 P
61 2z 2
62 61 a1i P 0 2
63 60 62 zsubcld P 0 P 2
64 59 63 jctild P 0 2 P P 2 0 P 2
65 1 64 syl P Word V 2 P P 2 0 P 2
66 65 imp P Word V 2 P P 2 0 P 2
67 elnn0z P 2 0 P 2 0 P 2
68 66 67 sylibr P Word V 2 P P 2 0
69 elnn0uz P 2 0 P 2 0
70 68 69 sylib P Word V 2 P P 2 0
71 fzosplitsn P 2 0 0 ..^ P - 2 + 1 = 0 ..^ P 2 P 2
72 70 71 syl P Word V 2 P 0 ..^ P - 2 + 1 = 0 ..^ P 2 P 2
73 54 72 eqtrd P Word V 2 P 0 ..^ P 1 = 0 ..^ P 2 P 2
74 73 adantr P Word V 2 P lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E 0 ..^ P 1 = 0 ..^ P 2 P 2
75 74 raleqdv P Word V 2 P lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E i 0 ..^ P 1 P i P i + 1 ran E i 0 ..^ P 2 P 2 P i P i + 1 ran E
76 48 75 mpbird P Word V 2 P lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E i 0 ..^ P 1 P i P i + 1 ran E
77 76 ex P Word V 2 P lastS P = P 0 i 0 ..^ P 1 - 0 - 1 P i P i + 1 ran E P P 2 P 0 ran E i 0 ..^ P 1 P i P i + 1 ran E