Metamath Proof Explorer


Theorem clwlkclwwlklem2a4

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

Ref Expression
Hypothesis clwlkclwwlklem2.f F = x 0 ..^ P 1 if x < P 2 E -1 P x P x + 1 E -1 P x P 0
Assertion clwlkclwwlklem2a4 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E E F I = P I P I + 1

Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f F = x 0 ..^ P 1 if x < P 2 E -1 P x P x + 1 E -1 P x P 0
2 fveq2 I = P 2 F I = F P 2
3 lencl P Word V P 0
4 1 clwlkclwwlklem2fv2 P 0 2 P F P 2 = E -1 P P 2 P 0
5 3 4 sylan P Word V 2 P F P 2 = E -1 P P 2 P 0
6 2 5 sylan9eqr P Word V 2 P I = P 2 F I = E -1 P P 2 P 0
7 6 ex P Word V 2 P I = P 2 F I = E -1 P P 2 P 0
8 7 3adant1 E : dom E 1-1 R P Word V 2 P I = P 2 F I = E -1 P P 2 P 0
9 8 ad2antrr E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E I = P 2 F I = E -1 P P 2 P 0
10 9 impcom I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E F I = E -1 P P 2 P 0
11 10 fveq2d I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E E F I = E E -1 P P 2 P 0
12 f1f1orn E : dom E 1-1 R E : dom E 1-1 onto ran E
13 12 3ad2ant1 E : dom E 1-1 R P Word V 2 P E : dom E 1-1 onto ran E
14 13 ad2antrr E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E E : dom E 1-1 onto ran E
15 lsw P Word V lastS P = P P 1
16 15 eqeq1d P Word V lastS P = P 0 P P 1 = P 0
17 nn0cn P 0 P
18 id P P
19 2cnd P 2
20 1cnd P 1
21 18 19 20 subsubd P P 2 1 = P - 2 + 1
22 2m1e1 2 1 = 1
23 22 a1i P 2 1 = 1
24 23 oveq2d P P 2 1 = P 1
25 21 24 eqtr3d P P - 2 + 1 = P 1
26 3 17 25 3syl P Word V P - 2 + 1 = P 1
27 26 adantr P Word V P P 1 = P 0 P - 2 + 1 = P 1
28 27 fveq2d P Word V P P 1 = P 0 P P - 2 + 1 = P P 1
29 eqeq2 P 0 = P P 1 P P - 2 + 1 = P 0 P P - 2 + 1 = P P 1
30 29 eqcoms P P 1 = P 0 P P - 2 + 1 = P 0 P P - 2 + 1 = P P 1
31 30 adantl P Word V P P 1 = P 0 P P - 2 + 1 = P 0 P P - 2 + 1 = P P 1
32 28 31 mpbird P Word V P P 1 = P 0 P P - 2 + 1 = P 0
33 32 ex P Word V P P 1 = P 0 P P - 2 + 1 = P 0
34 16 33 sylbid P Word V lastS P = P 0 P P - 2 + 1 = P 0
35 34 3ad2ant2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 P P - 2 + 1 = P 0
36 35 com12 lastS P = P 0 E : dom E 1-1 R P Word V 2 P P P - 2 + 1 = P 0
37 36 adantr lastS P = P 0 I 0 ..^ P 1 E : dom E 1-1 R P Word V 2 P P P - 2 + 1 = P 0
38 37 impcom E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P P - 2 + 1 = P 0
39 38 adantr E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 I = P 2 P P - 2 + 1 = P 0
40 39 preq2d E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 I = P 2 P P 2 P P - 2 + 1 = P P 2 P 0
41 fveq2 I = P 2 P I = P P 2
42 fvoveq1 I = P 2 P I + 1 = P P - 2 + 1
43 41 42 preq12d I = P 2 P I P I + 1 = P P 2 P P - 2 + 1
44 43 eqeq1d I = P 2 P I P I + 1 = P P 2 P 0 P P 2 P P - 2 + 1 = P P 2 P 0
45 44 adantl E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 I = P 2 P I P I + 1 = P P 2 P 0 P P 2 P P - 2 + 1 = P P 2 P 0
46 40 45 mpbird E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 I = P 2 P I P I + 1 = P P 2 P 0
47 46 eleq1d E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 I = P 2 P I P I + 1 ran E P P 2 P 0 ran E
48 47 biimpd E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 I = P 2 P I P I + 1 ran E P P 2 P 0 ran E
49 48 impancom E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E I = P 2 P P 2 P 0 ran E
50 49 impcom I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E P P 2 P 0 ran E
51 f1ocnvfv2 E : dom E 1-1 onto ran E P P 2 P 0 ran E E E -1 P P 2 P 0 = P P 2 P 0
52 14 50 51 syl2an2 I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E E E -1 P P 2 P 0 = P P 2 P 0
53 eqcom P P 1 = P 0 P 0 = P P 1
54 53 biimpi P P 1 = P 0 P 0 = P P 1
55 1e2m1 1 = 2 1
56 55 a1i P Word V 1 = 2 1
57 56 oveq2d P Word V P 1 = P 2 1
58 3 17 syl P Word V P
59 2cnd P Word V 2
60 1cnd P Word V 1
61 58 59 60 subsubd P Word V P 2 1 = P - 2 + 1
62 57 61 eqtrd P Word V P 1 = P - 2 + 1
63 62 fveq2d P Word V P P 1 = P P - 2 + 1
64 54 63 sylan9eqr P Word V P P 1 = P 0 P 0 = P P - 2 + 1
65 64 ex P Word V P P 1 = P 0 P 0 = P P - 2 + 1
66 16 65 sylbid P Word V lastS P = P 0 P 0 = P P - 2 + 1
67 66 imp P Word V lastS P = P 0 P 0 = P P - 2 + 1
68 67 preq2d P Word V lastS P = P 0 P P 2 P 0 = P P 2 P P - 2 + 1
69 68 adantr P Word V lastS P = P 0 I = P 2 P P 2 P 0 = P P 2 P P - 2 + 1
70 43 adantl P Word V lastS P = P 0 I = P 2 P I P I + 1 = P P 2 P P - 2 + 1
71 69 70 eqtr4d P Word V lastS P = P 0 I = P 2 P P 2 P 0 = P I P I + 1
72 71 exp31 P Word V lastS P = P 0 I = P 2 P P 2 P 0 = P I P I + 1
73 72 3ad2ant2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I = P 2 P P 2 P 0 = P I P I + 1
74 73 com12 lastS P = P 0 E : dom E 1-1 R P Word V 2 P I = P 2 P P 2 P 0 = P I P I + 1
75 74 adantr lastS P = P 0 I 0 ..^ P 1 E : dom E 1-1 R P Word V 2 P I = P 2 P P 2 P 0 = P I P I + 1
76 75 impcom E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 I = P 2 P P 2 P 0 = P I P I + 1
77 76 adantr E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E I = P 2 P P 2 P 0 = P I P I + 1
78 77 impcom I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E P P 2 P 0 = P I P I + 1
79 11 52 78 3eqtrd I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E E F I = P I P I + 1
80 simpll P 0 2 P I 0 ..^ P 1 ¬ I = P 2 P 0
81 oveq1 P = 2 P 1 = 2 1
82 81 22 syl6eq P = 2 P 1 = 1
83 82 oveq2d P = 2 0 ..^ P 1 = 0 ..^ 1
84 83 eleq2d P = 2 I 0 ..^ P 1 I 0 ..^ 1
85 oveq1 P = 2 P 2 = 2 2
86 2cn 2
87 86 subidi 2 2 = 0
88 85 87 syl6eq P = 2 P 2 = 0
89 88 eqeq2d P = 2 I = P 2 I = 0
90 89 notbid P = 2 ¬ I = P 2 ¬ I = 0
91 84 90 anbi12d P = 2 I 0 ..^ P 1 ¬ I = P 2 I 0 ..^ 1 ¬ I = 0
92 elsni I 0 I = 0
93 92 pm2.24d I 0 ¬ I = 0 I 0 P 2 I < P 2
94 fzo01 0 ..^ 1 = 0
95 93 94 eleq2s I 0 ..^ 1 ¬ I = 0 I 0 P 2 I < P 2
96 95 imp I 0 ..^ 1 ¬ I = 0 I 0 P 2 I < P 2
97 91 96 syl6bi P = 2 I 0 ..^ P 1 ¬ I = P 2 I 0 P 2 I < P 2
98 97 adantld P = 2 P 0 2 P I 0 ..^ P 1 ¬ I = P 2 I 0 P 2 I < P 2
99 df-ne P 2 ¬ P = 2
100 2re 2
101 100 a1i P 0 2 P 2
102 nn0re P 0 P
103 102 adantr P 0 2 P P
104 simpr P 0 2 P 2 P
105 101 103 104 leltned P 0 2 P 2 < P P 2
106 elfzo0 I 0 ..^ P 1 I 0 P 1 I < P 1
107 simp-4l I 0 P 0 ¬ I = P 2 2 < P I < P 1 I 0
108 nn0z P 0 P
109 2z 2
110 109 a1i P 0 2
111 108 110 zsubcld P 0 P 2
112 111 adantr P 0 2 < P P 2
113 100 a1i P 0 2
114 113 102 posdifd P 0 2 < P 0 < P 2
115 114 biimpa P 0 2 < P 0 < P 2
116 elnnz P 2 P 2 0 < P 2
117 112 115 116 sylanbrc P 0 2 < P P 2
118 117 ad5ant24 I 0 P 0 ¬ I = P 2 2 < P I < P 1 P 2
119 nn0z I 0 I
120 peano2zm P P 1
121 108 120 syl P 0 P 1
122 zltlem1 I P 1 I < P 1 I P - 1 - 1
123 119 121 122 syl2an I 0 P 0 I < P 1 I P - 1 - 1
124 17 adantl I 0 P 0 P
125 1cnd I 0 P 0 1
126 124 125 125 subsub4d I 0 P 0 P - 1 - 1 = P 1 + 1
127 1p1e2 1 + 1 = 2
128 127 a1i I 0 P 0 1 + 1 = 2
129 128 oveq2d I 0 P 0 P 1 + 1 = P 2
130 126 129 eqtrd I 0 P 0 P - 1 - 1 = P 2
131 130 breq2d I 0 P 0 I P - 1 - 1 I P 2
132 123 131 bitrd I 0 P 0 I < P 1 I P 2
133 necom P 2 I I P 2
134 df-ne I P 2 ¬ I = P 2
135 133 134 bitr2i ¬ I = P 2 P 2 I
136 nn0re I 0 I
137 136 ad2antrr I 0 P 0 I P 2 I
138 102 113 resubcld P 0 P 2
139 138 ad2antlr I 0 P 0 I P 2 P 2
140 simpr I 0 P 0 I P 2 I P 2
141 leltne I P 2 I P 2 I < P 2 P 2 I
142 141 bicomd I P 2 I P 2 P 2 I I < P 2
143 137 139 140 142 syl3anc I 0 P 0 I P 2 P 2 I I < P 2
144 143 biimpd I 0 P 0 I P 2 P 2 I I < P 2
145 135 144 syl5bi I 0 P 0 I P 2 ¬ I = P 2 I < P 2
146 145 ex I 0 P 0 I P 2 ¬ I = P 2 I < P 2
147 132 146 sylbid I 0 P 0 I < P 1 ¬ I = P 2 I < P 2
148 147 com23 I 0 P 0 ¬ I = P 2 I < P 1 I < P 2
149 148 imp I 0 P 0 ¬ I = P 2 I < P 1 I < P 2
150 149 adantr I 0 P 0 ¬ I = P 2 2 < P I < P 1 I < P 2
151 150 imp I 0 P 0 ¬ I = P 2 2 < P I < P 1 I < P 2
152 107 118 151 3jca I 0 P 0 ¬ I = P 2 2 < P I < P 1 I 0 P 2 I < P 2
153 152 ex I 0 P 0 ¬ I = P 2 2 < P I < P 1 I 0 P 2 I < P 2
154 153 exp41 I 0 P 0 ¬ I = P 2 2 < P I < P 1 I 0 P 2 I < P 2
155 154 com25 I 0 I < P 1 ¬ I = P 2 2 < P P 0 I 0 P 2 I < P 2
156 155 imp I 0 I < P 1 ¬ I = P 2 2 < P P 0 I 0 P 2 I < P 2
157 156 3adant2 I 0 P 1 I < P 1 ¬ I = P 2 2 < P P 0 I 0 P 2 I < P 2
158 106 157 sylbi I 0 ..^ P 1 ¬ I = P 2 2 < P P 0 I 0 P 2 I < P 2
159 158 imp I 0 ..^ P 1 ¬ I = P 2 2 < P P 0 I 0 P 2 I < P 2
160 159 com13 P 0 2 < P I 0 ..^ P 1 ¬ I = P 2 I 0 P 2 I < P 2
161 160 adantr P 0 2 P 2 < P I 0 ..^ P 1 ¬ I = P 2 I 0 P 2 I < P 2
162 105 161 sylbird P 0 2 P P 2 I 0 ..^ P 1 ¬ I = P 2 I 0 P 2 I < P 2
163 99 162 syl5bir P 0 2 P ¬ P = 2 I 0 ..^ P 1 ¬ I = P 2 I 0 P 2 I < P 2
164 163 com23 P 0 2 P I 0 ..^ P 1 ¬ I = P 2 ¬ P = 2 I 0 P 2 I < P 2
165 164 imp P 0 2 P I 0 ..^ P 1 ¬ I = P 2 ¬ P = 2 I 0 P 2 I < P 2
166 165 com12 ¬ P = 2 P 0 2 P I 0 ..^ P 1 ¬ I = P 2 I 0 P 2 I < P 2
167 98 166 pm2.61i P 0 2 P I 0 ..^ P 1 ¬ I = P 2 I 0 P 2 I < P 2
168 elfzo0 I 0 ..^ P 2 I 0 P 2 I < P 2
169 167 168 sylibr P 0 2 P I 0 ..^ P 1 ¬ I = P 2 I 0 ..^ P 2
170 80 169 jca P 0 2 P I 0 ..^ P 1 ¬ I = P 2 P 0 I 0 ..^ P 2
171 170 exp31 P 0 2 P I 0 ..^ P 1 ¬ I = P 2 P 0 I 0 ..^ P 2
172 3 171 syl P Word V 2 P I 0 ..^ P 1 ¬ I = P 2 P 0 I 0 ..^ P 2
173 172 imp P Word V 2 P I 0 ..^ P 1 ¬ I = P 2 P 0 I 0 ..^ P 2
174 173 3adant1 E : dom E 1-1 R P Word V 2 P I 0 ..^ P 1 ¬ I = P 2 P 0 I 0 ..^ P 2
175 174 expd E : dom E 1-1 R P Word V 2 P I 0 ..^ P 1 ¬ I = P 2 P 0 I 0 ..^ P 2
176 175 com12 I 0 ..^ P 1 E : dom E 1-1 R P Word V 2 P ¬ I = P 2 P 0 I 0 ..^ P 2
177 176 adantl lastS P = P 0 I 0 ..^ P 1 E : dom E 1-1 R P Word V 2 P ¬ I = P 2 P 0 I 0 ..^ P 2
178 177 impcom E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 ¬ I = P 2 P 0 I 0 ..^ P 2
179 178 adantr E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E ¬ I = P 2 P 0 I 0 ..^ P 2
180 179 impcom ¬ I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E P 0 I 0 ..^ P 2
181 1 clwlkclwwlklem2fv1 P 0 I 0 ..^ P 2 F I = E -1 P I P I + 1
182 180 181 syl ¬ I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E F I = E -1 P I P I + 1
183 182 fveq2d ¬ I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E E F I = E E -1 P I P I + 1
184 simprr ¬ I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E P I P I + 1 ran E
185 f1ocnvfv2 E : dom E 1-1 onto ran E P I P I + 1 ran E E E -1 P I P I + 1 = P I P I + 1
186 14 184 185 syl2an2 ¬ I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E E E -1 P I P I + 1 = P I P I + 1
187 183 186 eqtrd ¬ I = P 2 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E E F I = P I P I + 1
188 79 187 pm2.61ian E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E E F I = P I P I + 1
189 188 exp31 E : dom E 1-1 R P Word V 2 P lastS P = P 0 I 0 ..^ P 1 P I P I + 1 ran E E F I = P I P I + 1