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 PWordV2PlastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranEi0..^P1PiPi+1ranE

Proof

Step Hyp Ref Expression
1 lencl PWordVP0
2 nn0cn P0P
3 peano2cnm PP1
4 3 subid1d PP-1-0=P1
5 4 oveq1d PP1-0-1=P-1-1
6 sub1m1 PP-1-1=P2
7 5 6 eqtrd PP1-0-1=P2
8 1 2 7 3syl PWordVP1-0-1=P2
9 8 adantr PWordV2PP1-0-1=P2
10 9 oveq2d PWordV2P0..^P1-0-1=0..^P2
11 10 raleqdv PWordV2Pi0..^P1-0-1PiPi+1ranEi0..^P2PiPi+1ranE
12 11 biimpcd i0..^P1-0-1PiPi+1ranEPWordV2Pi0..^P2PiPi+1ranE
13 12 adantr i0..^P1-0-1PiPi+1ranEPP2P0ranEPWordV2Pi0..^P2PiPi+1ranE
14 13 adantl lastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranEPWordV2Pi0..^P2PiPi+1ranE
15 14 impcom PWordV2PlastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranEi0..^P2PiPi+1ranE
16 lsw PWordVlastSP=PP1
17 2m1e1 21=1
18 17 a1i PWordV21=1
19 18 eqcomd PWordV1=21
20 19 oveq2d PWordVP1=P21
21 1 2 syl PWordVP
22 2cnd PWordV2
23 1cnd PWordV1
24 21 22 23 subsubd PWordVP21=P-2+1
25 20 24 eqtrd PWordVP1=P-2+1
26 25 fveq2d PWordVPP1=PP-2+1
27 16 26 eqtrd PWordVlastSP=PP-2+1
28 27 adantr PWordV2PlastSP=PP-2+1
29 28 adantr PWordV2PlastSP=P0lastSP=PP-2+1
30 eqeq1 lastSP=P0lastSP=PP-2+1P0=PP-2+1
31 30 adantl PWordV2PlastSP=P0lastSP=PP-2+1P0=PP-2+1
32 29 31 mpbid PWordV2PlastSP=P0P0=PP-2+1
33 32 preq2d PWordV2PlastSP=P0PP2P0=PP2PP-2+1
34 33 eleq1d PWordV2PlastSP=P0PP2P0ranEPP2PP-2+1ranE
35 34 biimpd PWordV2PlastSP=P0PP2P0ranEPP2PP-2+1ranE
36 35 ex PWordV2PlastSP=P0PP2P0ranEPP2PP-2+1ranE
37 36 com13 PP2P0ranElastSP=P0PWordV2PPP2PP-2+1ranE
38 37 adantl i0..^P1-0-1PiPi+1ranEPP2P0ranElastSP=P0PWordV2PPP2PP-2+1ranE
39 38 impcom lastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranEPWordV2PPP2PP-2+1ranE
40 39 impcom PWordV2PlastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranEPP2PP-2+1ranE
41 ovexd PWordV2PlastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranEP2V
42 fveq2 i=P2Pi=PP2
43 fvoveq1 i=P2Pi+1=PP-2+1
44 42 43 preq12d i=P2PiPi+1=PP2PP-2+1
45 44 eleq1d i=P2PiPi+1ranEPP2PP-2+1ranE
46 45 ralunsn P2Vi0..^P2P2PiPi+1ranEi0..^P2PiPi+1ranEPP2PP-2+1ranE
47 41 46 syl PWordV2PlastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranEi0..^P2P2PiPi+1ranEi0..^P2PiPi+1ranEPP2PP-2+1ranE
48 15 40 47 mpbir2and PWordV2PlastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranEi0..^P2P2PiPi+1ranE
49 1e2m1 1=21
50 49 a1i PWordV1=21
51 50 oveq2d PWordVP1=P21
52 51 24 eqtrd PWordVP1=P-2+1
53 52 oveq2d PWordV0..^P1=0..^P-2+1
54 53 adantr PWordV2P0..^P1=0..^P-2+1
55 nn0re P0P
56 2re 2
57 56 a1i P02
58 55 57 subge0d P00P22P
59 58 biimprd P02P0P2
60 nn0z P0P
61 2z 2
62 61 a1i P02
63 60 62 zsubcld P0P2
64 59 63 jctild P02PP20P2
65 1 64 syl PWordV2PP20P2
66 65 imp PWordV2PP20P2
67 elnn0z P20P20P2
68 66 67 sylibr PWordV2PP20
69 elnn0uz P20P20
70 68 69 sylib PWordV2PP20
71 fzosplitsn P200..^P-2+1=0..^P2P2
72 70 71 syl PWordV2P0..^P-2+1=0..^P2P2
73 54 72 eqtrd PWordV2P0..^P1=0..^P2P2
74 73 adantr PWordV2PlastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranE0..^P1=0..^P2P2
75 74 raleqdv PWordV2PlastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranEi0..^P1PiPi+1ranEi0..^P2P2PiPi+1ranE
76 48 75 mpbird PWordV2PlastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranEi0..^P1PiPi+1ranE
77 76 ex PWordV2PlastSP=P0i0..^P1-0-1PiPi+1ranEPP2P0ranEi0..^P1PiPi+1ranE