Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  extwwlkfablem2 Structured version   Visualization version   Unicode version

Theorem extwwlkfablem2 25885
 Description: Lemma 2 for extwwlkfab 25897. (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 25144 . . . . . . . . . . 11 USGrph
2 uzuzle23 11223 . . . . . . . . . . . 12
3 eluzge2nn0 11222 . . . . . . . . . . . 12
42, 3syl 17 . . . . . . . . . . 11
51, 4anim12i 576 . . . . . . . . . 10 USGrph
6 df-3an 1009 . . . . . . . . . 10
75, 6sylibr 217 . . . . . . . . 9 USGrph
8 isclwwlkn 25576 . . . . . . . . 9 ClWWalksN ClWWalks
97, 8syl 17 . . . . . . . 8 USGrph ClWWalksN ClWWalks
1093adant2 1049 . . . . . . 7 USGrph ClWWalksN ClWWalks
11 isclwwlk 25575 . . . . . . . . . 10 ClWWalks Word ..^ lastS
1211anbi1d 719 . . . . . . . . 9 ClWWalks Word ..^ lastS
131, 12syl 17 . . . . . . . 8 USGrph ClWWalks Word ..^ lastS
14133ad2ant1 1051 . . . . . . 7 USGrph ClWWalks Word ..^ lastS
1510, 14bitrd 261 . . . . . 6 USGrph ClWWalksN Word ..^ lastS
16 swrdcl 12829 . . . . . . . . . . . 12 Word substr Word
17163ad2ant1 1051 . . . . . . . . . . 11 Word ..^ lastS substr Word
1817adantr 472 . . . . . . . . . 10 Word ..^ lastS substr Word
1918ad2antlr 741 . . . . . . . . 9 Word ..^ lastS substr Word
20 oveq1 6315 . . . . . . . . . . . . . . . . . . . 20
2120adantr 472 . . . . . . . . . . . . . . . . . . 19
22 1le3 10849 . . . . . . . . . . . . . . . . . . . . . 22
23 1red 9676 . . . . . . . . . . . . . . . . . . . . . . 23
24 3re 10705 . . . . . . . . . . . . . . . . . . . . . . . 24
2524a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
26 eluzelre 11193 . . . . . . . . . . . . . . . . . . . . . . 23
2723, 25, 26lesub2d 10242 . . . . . . . . . . . . . . . . . . . . . 22
2822, 27mpbii 216 . . . . . . . . . . . . . . . . . . . . 21
29 eluzelz 11192 . . . . . . . . . . . . . . . . . . . . . . 23
30 eluzel2 11187 . . . . . . . . . . . . . . . . . . . . . . 23
3129, 30zsubcld 11068 . . . . . . . . . . . . . . . . . . . . . 22
32 peano2zm 11004 . . . . . . . . . . . . . . . . . . . . . . 23
3329, 32syl 17 . . . . . . . . . . . . . . . . . . . . . 22
34 eluz 11196 . . . . . . . . . . . . . . . . . . . . . 22
3531, 33, 34syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21
3628, 35mpbird 240 . . . . . . . . . . . . . . . . . . . 20
3736adantl 473 . . . . . . . . . . . . . . . . . . 19
3821, 37eqeltrd 2549 . . . . . . . . . . . . . . . . . 18
39 fzoss2 11973 . . . . . . . . . . . . . . . . . 18 ..^ ..^
40 ssralv 3479 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
4138, 39, 403syl 18 . . . . . . . . . . . . . . . . 17 ..^ ..^
4241adantl 473 . . . . . . . . . . . . . . . 16 Word ..^ ..^
43 simpll 768 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ Word
44 1eluzge0 11226 . . . . . . . . . . . . . . . . . . . . . . . . . 26
45 fzss1 11863 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4644, 45mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . 25
47 ige3m2fz 11849 . . . . . . . . . . . . . . . . . . . . . . . . 25
4846, 47sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . . 24
4948adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23
50 oveq2 6316 . . . . . . . . . . . . . . . . . . . . . . . . 25
5150eleq2d 2534 . . . . . . . . . . . . . . . . . . . . . . . 24
5251adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
5349, 52mpbird 240 . . . . . . . . . . . . . . . . . . . . . 22
5453ad2antlr 741 . . . . . . . . . . . . . . . . . . . . 21 Word ..^
55 2re 10701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
56 2lt3 10800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5755, 24, 56ltleii 9775 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5855a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5958, 25, 26lesub2d 10242 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6057, 59mpbii 216 . . . . . . . . . . . . . . . . . . . . . . . . . 26
61 2z 10993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6261a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6329, 62zsubcld 11068 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
64 eluz 11196 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6531, 63, 64syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6660, 65mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . 25
67 fzoss2 11973 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
6866, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
6968sseld 3417 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
7069ad2antll 743 . . . . . . . . . . . . . . . . . . . . . 22 Word ..^ ..^
7170imp 436 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ ..^
72 swrd0fv 12849 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ substr
7343, 54, 71, 72syl3anc 1292 . . . . . . . . . . . . . . . . . . . 20 Word ..^ substr
7473eqcomd 2477 . . . . . . . . . . . . . . . . . . 19 Word ..^ substr
75 elfzonn0 11988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
7675adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
77 peano2nn0 10934 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7876, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
79 uz3m2nn 11225 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8079adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
81 elfzo0 11984 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
82 nn0cn 10903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
83 ax-1cn 9615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
8482, 83jctir 547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
8584adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
86 pncan 9901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
8785, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
8887eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
89 eluzelcn 11194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
9089adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
91 2cnd 10704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
92 1cnd 9677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9390, 91, 92subsub4d 10036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
94 df-3 10691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9594oveq2i 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9693, 95syl6reqr 2524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9788, 96breq12d 4408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9897biimpd 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9998impancom 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
100993adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
101100imp 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102 nn0re 10902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
103 peano2re 9824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1051043ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106105adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
10726, 58resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
108107adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
109 1red 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
110106, 108, 109ltsub1d 10243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
111101, 110mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
112111ex 441 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
11381, 112sylbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
114113impcom 437 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
115 elfzo0 11984 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
11678, 80, 114, 115syl3anbrc 1214 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
117116ex 441 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
118117ad2antll 743 . . . . . . . . . . . . . . . . . . . . . 22 Word ..^ ..^
119118imp 436 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ ..^
120 swrd0fv 12849 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ substr
12143, 54, 119, 120syl3anc 1292 . . . . . . . . . . . . . . . . . . . 20 Word ..^ substr
122121eqcomd 2477 . . . . . . . . . . . . . . . . . . 19 Word ..^ substr
12374, 122preq12d 4050 . . . . . . . . . . . . . . . . . 18 Word ..^ substr substr
124123eleq1d 2533 . . . . . . . . . . . . . . . . 17 Word ..^ substr substr
125124ralbidva 2828 . . . . . . . . . . . . . . . 16 Word ..^ ..^ substr substr
12642, 125sylibd 222 . . . . . . . . . . . . . . 15 Word ..^ ..^ substr substr
127126impancom 447 . . . . . . . . . . . . . 14 Word ..^ ..^ substr substr
1281273adant3 1050 . . . . . . . . . . . . 13 Word ..^ lastS ..^ substr substr
129128expdimp 444 . . . . . . . . . . . 12 Word ..^ lastS ..^ substr substr
130129impcom 437 . . . . . . . . . . 11 Word ..^ lastS ..^ substr substr
131130adantr 472 . . . . . . . . . 10 Word ..^ lastS ..^ substr substr
132 simprl1 1075 . . . . . . . . . . . . . . . . 17 Word ..^ lastS Word
133 simprr 774 . . . . . . . . . . . . . . . . 17 Word ..^ lastS
1342adantr 472 . . . . . . . . . . . . . . . . 17 Word ..^ lastS
135132, 133, 1343jca 1210 . . . . . . . . . . . . . . . 16 Word ..^ lastS Word
136135adantr 472 . . . . . . . . . . . . . . 15 Word ..^ lastS Word
137 extwwlkfablem2lem 25882 . . . . . . . . . . . . . . 15 Word substr
138136, 137syl 17 . . . . . . . . . . . . . 14 Word ..^ lastS substr
139138oveq1d 6323 . . . . . . . . . . . . 13 Word ..^ lastS substr
140139oveq2d 6324 . . . . . . . . . . . 12 Word ..^ lastS ..^ substr ..^
141 2cnd 10704 . . . . . . . . . . . . . . . 16
142 1cnd 9677 . . . . . . . . . . . . . . . 16
14389, 141, 142subsub4d 10036 . . . . . . . . . . . . . . 15
144 2p1e3 10756 . . . . . . . . . . . . . . . . 17
145144a1i 11 . . . . . . . . . . . . . . . 16
146145oveq2d 6324 . . . . . . . . . . . . . . 15
147143, 146eqtrd 2505 . . . . . . . . . . . . . 14
148147ad2antrr 740 . . . . . . . . . . . . 13 Word ..^ lastS
149148oveq2d 6324 . . . . . . . . . . . 12 Word ..^ lastS ..^ ..^
150140, 149eqtrd 2505 . . . . . . . . . . 11 Word ..^ lastS ..^ substr ..^
151150raleqdv 2979 . . . . . . . . . 10 Word ..^ lastS ..^ substr substr substr ..^ substr substr
152131, 151mpbird 240 . . . . . . . . 9 Word ..^ lastS ..^ substr substr substr
15320oveq2d 6324 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
154153raleqdv 2979 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
155 simplr 770 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word Word
156 oveq2 6316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
157156eleq2d 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
15847, 157syl5ibr 229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
159158ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ Word
160159com12 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ Word
161160adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ Word
162161impcom 437 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
163 swrd0fvlsw 12853 . . . . . . . . . . . . . . . . . . . . . . 23 Word lastS substr
164155, 162, 163syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Word lastS substr
16547adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
166156adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
167165, 166eleqtrrd 2552 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
168167ex 441 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
169168ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ Word
170169com12 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ Word
171170adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ Word
172171impcom 437 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
173 swrd0fv0 12850 . . . . . . . . . . . . . . . . . . . . . . 23 Word substr
174155, 172, 173syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Word substr
175164, 174preq12d 4050 . . . . . . . . . . . . . . . . . . . . 21 ..^ Word lastS substr substr
176 cnm2m1cnm3 10888 . . . . . . . . . . . . . . . . . . . . . . . . . 26
17789, 176syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25
178177fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . 24
179178ad2antrl 742 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
180 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25
181180eqcoms 2479 . . . . . . . . . . . . . . . . . . . . . . . 24
182181ad2antll 743 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
183179, 182preq12d 4050 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Word
184 eluzfz2b 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
185 fzval3 12012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
18629, 185syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
187186eleq2d 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
188 peano2z 11002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
189 zadd2cl 11071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
190 1le2 10846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
191 1red 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
19255a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
193 zre 10965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
194191, 192, 193leadd2d 10229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
195190, 194mpbii 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
196188, 189, 1953jca 1210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
19729, 196syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
198 eluz2 11188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
199197, 198sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
200 fzoss2 11973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^ ..^
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ ..^
202201sseld 3417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ ..^
203187, 202sylbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
204184, 203syl5bi 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
205204pm2.43i 48 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
206 3cn 10706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
207206a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
208207, 89, 142addsub12d 10028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
209 3m1e2 10748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
210209oveq2i 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211208, 210syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212211oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^
213205, 212eleqtrrd 2552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
214213, 33jca 541 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
215 fzosubel3 12004 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
216 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
217 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
218217fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
219216, 218preq12d 4050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
220219eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
221220rspcv 3132 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
222214, 215, 2213syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
22389, 207, 142subsubd 10033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
224209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
225224oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
226223, 225eqtr3d 2507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
227226fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
228227preq2d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
229228eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
230222, 229sylibd 222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
231230adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
232231com12 31 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
233232ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
234233imp 436 . . . . . . . . . . . . . . . . . . . . . 22 ..^ Word
235183, 234eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . 21 ..^ Word
236175, 235eqeltrd 2549 . . . . . . . . . . . . . . . . . . . 20 ..^ Word lastS substr substr
237236exp41 621 . . . . . . . . . . . . . . . . . . 19 ..^ Word lastS substr substr
238154, 237sylbid 223 . . . . . . . . . . . . . . . . . 18 ..^ Word lastS substr substr
239238com13 82 . . . . . . . . . . . . . . . . 17 Word ..^ lastS substr substr
240239imp 436 . . . . . . . . . . . . . . . 16 Word ..^ lastS substr substr
2412403adant3 1050 . . . . . . . . . . . . . . 15 Word ..^ lastS lastS substr substr
242241imp 436 . . . . . . . . . . . . . 14 Word ..^ lastS lastS substr substr
243242expd 443 . . . . . . . . . . . . 13 Word ..^ lastS lastS substr substr
244243impcom 437 . . . . . . . . . . . 12 Word ..^ lastS lastS substr substr
245244com12 31 . . . . . . . . . . 11 Word ..^ lastS lastS substr substr
246245adantl 473 . . . . . . . . . 10 Word ..^ lastS lastS substr substr
247246impcom 437 . . . . . . . . 9 Word ..^ lastS lastS substr substr
24819, 152, 2473jca 1210 . . . . . . . 8 Word ..^ lastS substr Word ..^ substr substr substr lastS substr substr
249248exp31 615 . . . . . . 7 Word ..^ lastS substr Word ..^ substr substr substr lastS substr substr
2502493ad2ant3 1053 . . . . . 6 USGrph Word ..^ lastS substr Word ..^ substr substr substr lastS substr substr
25115, 250sylbid 223 . . . . 5 USGrph ClWWalksN substr Word ..^ substr substr substr lastS substr substr
252251imp31 439 . . . 4 USGrph ClWWalksN substr Word ..^ substr substr substr lastS substr substr
253 clwwlknprop 25579 . . . . . . . . . 10 ClWWalksN Word
254 simpl2 1034 . . . . . . . . . . . 12 Word Word
255 simpl3r 1086 . . . . . . . . . . . 12 Word
2562adantl 473 . . . . . . . . . . . 12 Word
257254, 255, 2563jca 1210 . . . . . . . . . . 11 Word Word
258257ex 441 . . . . . . . . . 10 Word Word
259253, 258syl 17 . . . . . . . . 9 ClWWalksN Word
260259com12 31 . . . . . . . 8 ClWWalksN Word
2612603ad2ant3 1053 . . . . . . 7 USGrph ClWWalksN Word
262261imp 436 . . . . . 6 USGrph ClWWalksN Word
263262adantr 472 . . . . 5 USGrph ClWWalksN Word
264263, 137syl 17 . . . 4 USGrph ClWWalksN substr
265252, 264jca 541 . . 3 USGrph ClWWalksN substr Word ..^ substr substr substr lastS substr substr substr
266 uznn0sub 11214 . . . . . . . . . 10
2672, 266syl 17 . . . . . . . . 9
2681, 267anim12i 576 . . . . . . . 8 USGrph
269 df-3an 1009 . . . . . . . 8
270268, 269sylibr 217 . . . . . . 7 USGrph
271 isclwwlkn 25576 . . . . . . 7 substr ClWWalksN substr ClWWalks substr
272270, 271syl 17 . . . . . 6 USGrph substr ClWWalksN substr ClWWalks substr
273 isclwwlk 25575 . . . . . . . . 9 substr ClWWalks substr Word ..^ substr substr substr lastS substr substr
2741, 273syl 17 . . . . . . . 8 USGrph substr ClWWalks substr Word ..^ substr substr substr lastS substr substr
275274adantr 472 . . . . . . 7 USGrph substr ClWWalks substr Word ..^ substr substr substr lastS substr substr
276275anbi1d 719 . . . . . 6 USGrph substr ClWWalks substr substr Word ..^ substr substr substr lastS substr substr substr
277272, 276bitrd 261 . . . . 5 USGrph substr ClWWalksN substr Word ..^ substr substr substr lastS substr substr substr
2782773adant2 1049 . . . 4 USGrph substr ClWWalksN substr Word ..^ substr substr substr