Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  extwwlkfablem2 Structured version   Unicode version

Theorem extwwlkfablem2 30811
 Description: Lemma 2 for extwwlkfab 30823. (Contributed by Alexander van der Vekens, 15-Sep-2018.)
Hypothesis
Ref Expression
numclwwlk.c ClWWalksN
Assertion
Ref Expression
extwwlkfablem2 USGrph ClWWalksN substr
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   (,)   ()   ()   ()   (,)

Proof of Theorem extwwlkfablem2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 usgrav 23407 . . . . . . . . . . 11 USGrph
2 uzuzle23 30333 . . . . . . . . . . . 12
3 eluzge2nn0 30332 . . . . . . . . . . . 12
42, 3syl 16 . . . . . . . . . . 11
51, 4anim12i 566 . . . . . . . . . 10 USGrph
6 df-3an 967 . . . . . . . . . 10
75, 6sylibr 212 . . . . . . . . 9 USGrph
8 isclwwlkn 30572 . . . . . . . . 9 ClWWalksN ClWWalks
97, 8syl 16 . . . . . . . 8 USGrph ClWWalksN ClWWalks
1093adant2 1007 . . . . . . 7 USGrph ClWWalksN ClWWalks
11 isclwwlk 30571 . . . . . . . . . 10 ClWWalks Word ..^ lastS
1211anbi1d 704 . . . . . . . . 9 ClWWalks Word ..^ lastS
131, 12syl 16 . . . . . . . 8 USGrph ClWWalks Word ..^ lastS
14133ad2ant1 1009 . . . . . . 7 USGrph ClWWalks Word ..^ lastS
1510, 14bitrd 253 . . . . . 6 USGrph ClWWalksN Word ..^ lastS
16 swrdcl 12419 . . . . . . . . . . . 12 Word substr Word
17163ad2ant1 1009 . . . . . . . . . . 11 Word ..^ lastS substr Word
1817adantr 465 . . . . . . . . . 10 Word ..^ lastS substr Word
1918ad2antlr 726 . . . . . . . . 9 Word ..^ lastS substr Word
20 oveq1 6199 . . . . . . . . . . . . . . . . . . . 20
2120adantr 465 . . . . . . . . . . . . . . . . . . 19
22 1le3 10641 . . . . . . . . . . . . . . . . . . . . . 22
23 1re 9488 . . . . . . . . . . . . . . . . . . . . . . . 24
2423a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
25 3re 10498 . . . . . . . . . . . . . . . . . . . . . . . 24
2625a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
27 eluzelre 10974 . . . . . . . . . . . . . . . . . . . . . . 23
2824, 26, 27lesub2d 10050 . . . . . . . . . . . . . . . . . . . . . 22
2922, 28mpbii 211 . . . . . . . . . . . . . . . . . . . . 21
30 eluzelz 10973 . . . . . . . . . . . . . . . . . . . . . . 23
31 eluzel2 10969 . . . . . . . . . . . . . . . . . . . . . . 23
3230, 31zsubcld 10855 . . . . . . . . . . . . . . . . . . . . . 22
33 peano2zm 10791 . . . . . . . . . . . . . . . . . . . . . . 23
3430, 33syl 16 . . . . . . . . . . . . . . . . . . . . . 22
35 eluz 10977 . . . . . . . . . . . . . . . . . . . . . 22
3632, 34, 35syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
3729, 36mpbird 232 . . . . . . . . . . . . . . . . . . . 20
3837adantl 466 . . . . . . . . . . . . . . . . . . 19
3921, 38eqeltrd 2539 . . . . . . . . . . . . . . . . . 18
40 fzoss2 11680 . . . . . . . . . . . . . . . . . 18 ..^ ..^
41 ssralv 3516 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
4239, 40, 413syl 20 . . . . . . . . . . . . . . . . 17 ..^ ..^
4342adantl 466 . . . . . . . . . . . . . . . 16 Word ..^ ..^
44 simpll 753 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ Word
45 1eluzge0 11002 . . . . . . . . . . . . . . . . . . . . . . . . . 26
46 fzss1 11600 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4745, 46mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . 25
48 ige3m2fz 30347 . . . . . . . . . . . . . . . . . . . . . . . . 25
4947, 48sseldd 3457 . . . . . . . . . . . . . . . . . . . . . . . 24
5049adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23
51 oveq2 6200 . . . . . . . . . . . . . . . . . . . . . . . . 25
5251eleq2d 2521 . . . . . . . . . . . . . . . . . . . . . . . 24
5352adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
5450, 53mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22
5554ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 Word ..^
56 2re 10494 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
57 2lt3 10592 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5856, 25, 57ltleii 9600 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5956a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6059, 26, 27lesub2d 10050 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6158, 60mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . . . 26
62 2z 10781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6362a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6430, 63zsubcld 10855 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
65 eluz 10977 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6632, 64, 65syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6761, 66mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . 25
68 fzoss2 11680 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
6967, 68syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
7069sseld 3455 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
7170ad2antll 728 . . . . . . . . . . . . . . . . . . . . . 22 Word ..^ ..^
7271imp 429 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ ..^
73 swrd0fv 12439 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ substr
7444, 55, 72, 73syl3anc 1219 . . . . . . . . . . . . . . . . . . . 20 Word ..^ substr
7574eqcomd 2459 . . . . . . . . . . . . . . . . . . 19 Word ..^ substr
76 elfzonn0 11694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
7776adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
78 peano2nn0 10723 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7977, 78syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
80 uz3m2nn 30335 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8180adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
82 elfzo0 11690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
83 nn0cn 10692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
84 ax-1cn 9443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
8583, 84jctir 538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
8685adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
87 pncan 9719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
8886, 87syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
8988eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
90 eluzelcn 10975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
9190adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
92 2cnd 10497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9491, 92, 93subsub4d 9853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
95 df-3 10484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9695oveq2i 6203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9794, 96syl6reqr 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9889, 97breq12d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9998biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
10099impancom 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1011003adant2 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
102101imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
103 nn0re 10691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
104 peano2re 9645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
105103, 104syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1061053ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
107106adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
10827, 59resubcld 9879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109108adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
11023a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
111107, 109, 110ltsub1d 10051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
112102, 111mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
113112ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
11482, 113sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
115114impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
116 elfzo0 11690 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
11779, 81, 115, 116syl3anbrc 1172 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
118117ex 434 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
119118ad2antll 728 . . . . . . . . . . . . . . . . . . . . . 22 Word ..^ ..^
120119imp 429 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ ..^
121 swrd0fv 12439 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ substr
12244, 55, 120, 121syl3anc 1219 . . . . . . . . . . . . . . . . . . . 20 Word ..^ substr
123122eqcomd 2459 . . . . . . . . . . . . . . . . . . 19 Word ..^ substr
12475, 123preq12d 4062 . . . . . . . . . . . . . . . . . 18 Word ..^ substr substr
125124eleq1d 2520 . . . . . . . . . . . . . . . . 17 Word ..^ substr substr
126125ralbidva 2836 . . . . . . . . . . . . . . . 16 Word ..^ ..^ substr substr
12743, 126sylibd 214 . . . . . . . . . . . . . . 15 Word ..^ ..^ substr substr
128127impancom 440 . . . . . . . . . . . . . 14 Word ..^ ..^ substr substr
1291283adant3 1008 . . . . . . . . . . . . 13 Word ..^ lastS ..^ substr substr
130129expdimp 437 . . . . . . . . . . . 12 Word ..^ lastS ..^ substr substr
131130impcom 430 . . . . . . . . . . 11 Word ..^ lastS ..^ substr substr
132131adantr 465 . . . . . . . . . 10 Word ..^ lastS ..^ substr substr
133 simprl1 1033 . . . . . . . . . . . . . . . . 17 Word ..^ lastS Word
134 simprr 756 . . . . . . . . . . . . . . . . 17 Word ..^ lastS
1352adantr 465 . . . . . . . . . . . . . . . . 17 Word ..^ lastS
136133, 134, 1353jca 1168 . . . . . . . . . . . . . . . 16 Word ..^ lastS Word
137136adantr 465 . . . . . . . . . . . . . . 15 Word ..^ lastS Word
138 extwwlkfablem2lem 30808 . . . . . . . . . . . . . . 15 Word substr
139137, 138syl 16 . . . . . . . . . . . . . 14 Word ..^ lastS substr
140139oveq1d 6207 . . . . . . . . . . . . 13 Word ..^ lastS substr
141140oveq2d 6208 . . . . . . . . . . . 12 Word ..^ lastS ..^ substr ..^
142 2cnd 10497 . . . . . . . . . . . . . . . 16
14384a1i 11 . . . . . . . . . . . . . . . 16
14490, 142, 143subsub4d 9853 . . . . . . . . . . . . . . 15
145 2p1e3 10548 . . . . . . . . . . . . . . . . 17
146145a1i 11 . . . . . . . . . . . . . . . 16
147146oveq2d 6208 . . . . . . . . . . . . . . 15
148144, 147eqtrd 2492 . . . . . . . . . . . . . 14
149148ad2antrr 725 . . . . . . . . . . . . 13 Word ..^ lastS
150149oveq2d 6208 . . . . . . . . . . . 12 Word ..^ lastS ..^ ..^
151141, 150eqtrd 2492 . . . . . . . . . . 11 Word ..^ lastS ..^ substr ..^
152151raleqdv 3021 . . . . . . . . . 10 Word ..^ lastS ..^ substr substr substr ..^ substr substr
153132, 152mpbird 232 . . . . . . . . 9 Word ..^ lastS ..^ substr substr substr
15420oveq2d 6208 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
155154raleqdv 3021 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
156 simplr 754 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word Word
157 oveq2 6200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
158157eleq2d 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
15948, 158syl5ibr 221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
160159ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ Word
161160com12 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ Word
162161adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ Word
163162impcom 430 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
164 swrd0fvlsw 12443 . . . . . . . . . . . . . . . . . . . . . . 23 Word lastS substr
165156, 163, 164syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Word lastS substr
16648adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
167157adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
168166, 167eleqtrrd 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
169168ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
170169ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ Word
171170com12 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ Word
172171adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ Word
173172impcom 430 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
174 swrd0fv0 12440 . . . . . . . . . . . . . . . . . . . . . . 23 Word substr
175156, 173, 174syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Word substr
176165, 175preq12d 4062 . . . . . . . . . . . . . . . . . . . . 21 ..^ Word lastS substr substr
177 cnm2m1cnm3 30319 . . . . . . . . . . . . . . . . . . . . . . . . . 26
17890, 177syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
179178fveq2d 5795 . . . . . . . . . . . . . . . . . . . . . . . 24
180179ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
181 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25
182181eqcoms 2463 . . . . . . . . . . . . . . . . . . . . . . . 24
183182ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
184180, 183preq12d 4062 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Word
185 eluzfz2b 11563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
186 fzval3 11708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
18730, 186syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
188187eleq2d 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
189 peano2z 10789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
190 zadd2cl 30328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
191 1le2 10638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
19223a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
19356a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
194 zre 10753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
195192, 193, 194leadd2d 10037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
196191, 195mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
197189, 190, 1963jca 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
19830, 197syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
199 eluz2 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
200198, 199sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
201 fzoss2 11680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^ ..^
202200, 201syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ ..^
203202sseld 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ ..^
204188, 203sylbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
205185, 204syl5bi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
206205pm2.43i 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
207 3cn 10499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
208207a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
209208, 90, 143addsub12d 9845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
210 3m1e2 10541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
211210oveq2i 6203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
212209, 211syl6eq 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
213212oveq2d 6208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^
214206, 213eleqtrrd 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
215214, 34jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
216 fzosubel3 11704 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
217 fveq2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
218 oveq1 6199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
219218fveq2d 5795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
220217, 219preq12d 4062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
221220eleq1d 2520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
222221rspcv 3167 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
223215, 216, 2223syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
22490, 208, 143subsubd 9850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
225210a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
226225oveq2d 6208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
227224, 226eqtr3d 2494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
228227fveq2d 5795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
229228preq2d 4061 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
230229eleq1d 2520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
231223, 230sylibd 214 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
232231adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
233232com12 31 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
234233ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
235234imp 429 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Word
236184, 235eqeltrd 2539 . . . . . . . . . . . . . . . . . . . . 21 ..^ Word
237176, 236eqeltrd 2539 . . . . . . . . . . . . . . . . . . . 20 ..^ Word lastS substr substr
238237exp41 610 . . . . . . . . . . . . . . . . . . 19 ..^ Word lastS substr substr
239155, 238sylbid 215 . . . . . . . . . . . . . . . . . 18 ..^ Word lastS substr substr
240239com13 80 . . . . . . . . . . . . . . . . 17 Word ..^ lastS substr substr
241240imp 429 . . . . . . . . . . . . . . . 16 Word ..^ lastS substr substr
2422413adant3 1008 . . . . . . . . . . . . . . 15 Word ..^ lastS lastS substr substr
243242imp 429 . . . . . . . . . . . . . 14 Word ..^ lastS lastS substr substr
244243expd 436 . . . . . . . . . . . . 13 Word ..^ lastS lastS substr substr
245244impcom 430 . . . . . . . . . . . 12 Word ..^ lastS lastS substr substr
246245com12 31 . . . . . . . . . . 11 Word ..^ lastS lastS substr substr
247246adantl 466 . . . . . . . . . 10 Word ..^ lastS lastS substr substr
248247impcom 430 . . . . . . . . 9 Word ..^ lastS lastS substr substr
24919, 153, 2483jca 1168 . . . . . . . 8 Word ..^ lastS substr Word ..^ substr substr substr lastS substr substr
250249exp31 604 . . . . . . 7 Word ..^ lastS substr Word ..^ substr substr substr lastS substr substr
2512503ad2ant3 1011 . . . . . 6 USGrph Word ..^ lastS substr Word ..^ substr substr substr lastS substr substr
25215, 251sylbid 215 . . . . 5 USGrph ClWWalksN substr Word ..^ substr substr substr lastS substr substr
253252imp31 432 . . . 4 USGrph ClWWalksN substr Word ..^ substr substr substr lastS substr substr
254 clwwlknprop 30575 . . . . . . . . . 10 ClWWalksN Word
255 simpl2 992 . . . . . . . . . . . 12 Word Word
256 simpl3r 1044 . . . . . . . . . . . 12 Word
2572adantl 466 . . . . . . . . . . . 12 Word
258255, 256, 2573jca 1168 . . . . . . . . . . 11 Word Word
259258ex 434 . . . . . . . . . 10 Word Word
260254, 259syl 16 . . . . . . . . 9 ClWWalksN Word
261260com12 31 . . . . . . . 8 ClWWalksN Word
2622613ad2ant3 1011 . . . . . . 7 USGrph ClWWalksN Word
263262imp 429 . . . . . 6 USGrph ClWWalksN Word
264263adantr 465 . . . . 5 USGrph ClWWalksN Word
265264, 138syl 16 . . . 4 USGrph ClWWalksN substr
266253, 265jca 532 . . 3 USGrph ClWWalksN substr Word ..^ substr substr substr lastS substr substr substr
267 uznn0sub 10995 . . . . . . . . . 10
2682, 267syl 16 . . . . . . . . 9
2691, 268anim12i 566 . . . . . . . 8 USGrph
270 df-3an 967 . . . . . . . 8
271269, 270sylibr 212 . . . . . . 7 USGrph
272 isclwwlkn 30572 . . . . . . 7 substr ClWWalksN substr ClWWalks substr
273271, 272syl 16 . . . . . 6 USGrph substr ClWWalksN substr ClWWalks substr
274 isclwwlk 30571 . . . . . . . . 9 substr ClWWalks substr Word ..^ substr substr substr lastS substr substr
2751, 274syl 16 . . . . . . . 8 USGrph substr ClWWalks substr Word ..^ substr substr substr lastS substr substr
276275adantr 465 . . . . . . 7 USGrph substr ClWWalks substr Word ..^ substr substr substr lastS substr substr
277276anbi1d 704 . . . . . 6 USGrph substr ClWWalks substr substr Word ..^ substr substr substr lastS substr substr substr
278273, 277bitrd 253 . . . . 5 USGrph substr ClWWalksN substr Word ..^ substr substr substr lastS substr substr substr
2792783adant2 1007 . . . 4 USGrph substr ClWWalksN substr Word ..^ substr substr substr