Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
Vtx Vtx |
2 | | wwlksnextprop.e |
. . . . 5
Edg |
3 | 1, 2 | wwlknp 26734 |
. . . 4
WWalksN
Word Vtx ..^ |
4 | | fzonn0p1 12544 |
. . . . . . . . . . 11
..^ |
5 | 4 | adantl 482 |
. . . . . . . . . 10
Word Vtx ..^ |
6 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
7 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
8 | 7 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
9 | 6, 8 | preq12d 4276 |
. . . . . . . . . . . 12
|
10 | 9 | eleq1d 2686 |
. . . . . . . . . . 11
|
11 | 10 | rspcv 3305 |
. . . . . . . . . 10
..^
..^
|
12 | 5, 11 | syl 17 |
. . . . . . . . 9
Word Vtx
..^
|
13 | 12 | imp 445 |
. . . . . . . 8
Word Vtx ..^
|
14 | | simpll 790 |
. . . . . . . . . . . . . 14
Word Vtx Word Vtx |
15 | | 1zzd 11408 |
. . . . . . . . . . . . . . . 16
Word Vtx |
16 | | lencl 13324 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
|
17 | 16 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
Word Vtx
|
18 | 17 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
Word Vtx |
19 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . 18
|
20 | 19 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
|
21 | 20 | adantl 482 |
. . . . . . . . . . . . . . . 16
Word Vtx
|
22 | 15, 18, 21 | 3jca 1242 |
. . . . . . . . . . . . . . 15
Word Vtx
|
23 | | nn0ge0 11318 |
. . . . . . . . . . . . . . . . . 18
|
24 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . 19
|
25 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . 19
|
26 | 24, 25 | addge02d 10616 |
. . . . . . . . . . . . . . . . . 18
|
27 | 23, 26 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
28 | 27 | adantl 482 |
. . . . . . . . . . . . . . . 16
Word Vtx |
29 | 19 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . 22
|
30 | 29 | lep1d 10955 |
. . . . . . . . . . . . . . . . . . . . 21
|
31 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | 30, 31 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
34 | 33 | com23 86 |
. . . . . . . . . . . . . . . . . 18
|
35 | 16, 34 | syl 17 |
. . . . . . . . . . . . . . . . 17
Word Vtx
|
36 | 35 | imp31 448 |
. . . . . . . . . . . . . . . 16
Word Vtx
|
37 | 28, 36 | jca 554 |
. . . . . . . . . . . . . . 15
Word Vtx
|
38 | | elfz2 12333 |
. . . . . . . . . . . . . . 15
|
39 | 22, 37, 38 | sylanbrc 698 |
. . . . . . . . . . . . . 14
Word Vtx
|
40 | 14, 39 | jca 554 |
. . . . . . . . . . . . 13
Word Vtx
Word Vtx
|
41 | | swrd0fvlsw 13443 |
. . . . . . . . . . . . 13
Word Vtx
lastS substr |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . 12
Word Vtx lastS substr |
43 | | nn0cn 11302 |
. . . . . . . . . . . . . . 15
|
44 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
|
45 | 43, 44 | pncand 10393 |
. . . . . . . . . . . . . 14
|
46 | 45 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
47 | 46 | adantl 482 |
. . . . . . . . . . . 12
Word Vtx
|
48 | 42, 47 | eqtrd 2656 |
. . . . . . . . . . 11
Word Vtx lastS substr |
49 | | lsw 13351 |
. . . . . . . . . . . . 13
Word Vtx
lastS |
50 | 49 | ad2antrr 762 |
. . . . . . . . . . . 12
Word Vtx lastS |
51 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
52 | 51 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
53 | 52 | adantl 482 |
. . . . . . . . . . . . 13
Word Vtx |
54 | 19 | nn0cnd 11353 |
. . . . . . . . . . . . . . 15
|
55 | 54, 44 | pncand 10393 |
. . . . . . . . . . . . . 14
|
56 | 55 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
57 | 53, 56 | sylan9eq 2676 |
. . . . . . . . . . . 12
Word Vtx
|
58 | 50, 57 | eqtrd 2656 |
. . . . . . . . . . 11
Word Vtx lastS |
59 | 48, 58 | preq12d 4276 |
. . . . . . . . . 10
Word Vtx lastS substr lastS |
60 | 59 | eleq1d 2686 |
. . . . . . . . 9
Word Vtx
lastS substr lastS |
61 | 60 | adantr 481 |
. . . . . . . 8
Word Vtx ..^ lastS substr lastS |
62 | 13, 61 | mpbird 247 |
. . . . . . 7
Word Vtx ..^ lastS substr lastS |
63 | 62 | exp31 630 |
. . . . . 6
Word Vtx
..^ lastS substr lastS |
64 | 63 | com23 86 |
. . . . 5
Word Vtx
..^
lastS substr lastS |
65 | 64 | 3impia 1261 |
. . . 4
Word Vtx ..^ lastS substr lastS |
66 | 3, 65 | syl 17 |
. . 3
WWalksN
lastS substr lastS |
67 | | wwlksnextprop.x |
. . 3
WWalksN
|
68 | 66, 67 | eleq2s 2719 |
. 2
lastS substr lastS |
69 | 68 | imp 445 |
1
lastS substr lastS |