Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . 6
Vtx Vtx |
2 | | eqid 2622 |
. . . . . 6
Edg Edg |
3 | 1, 2 | clwwlknp 26887 |
. . . . 5
ClWWalksN Word Vtx
..^ Edg lastS Edg |
4 | | swrdcl 13419 |
. . . . . . . . . 10
Word Vtx
substr Word Vtx |
5 | 4 | adantr 481 |
. . . . . . . . 9
Word Vtx substr Word Vtx |
6 | 5 | ad2antrr 762 |
. . . . . . . 8
Word Vtx ..^ Edg
substr Word Vtx |
7 | | nnz 11399 |
. . . . . . . . . . . . . . . . . 18
|
8 | | eluzp1m1 11711 |
. . . . . . . . . . . . . . . . . . 19
|
9 | 8 | ex 450 |
. . . . . . . . . . . . . . . . . 18
|
10 | 7, 9 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
11 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . . 19
|
12 | 7, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
13 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . 19
|
14 | 13 | lem1d 10957 |
. . . . . . . . . . . . . . . . . 18
|
15 | | eluzuzle 11696 |
. . . . . . . . . . . . . . . . . 18
|
16 | 12, 14, 15 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
17 | 10, 16 | syld 47 |
. . . . . . . . . . . . . . . 16
|
18 | 17 | imp 445 |
. . . . . . . . . . . . . . 15
|
19 | | fzoss2 12496 |
. . . . . . . . . . . . . . 15
..^ ..^ |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
..^ ..^ |
21 | 20 | adantl 482 |
. . . . . . . . . . . . 13
Word Vtx
..^ ..^ |
22 | | ssralv 3666 |
. . . . . . . . . . . . 13
..^ ..^ ..^ Edg ..^ Edg |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
Word Vtx
..^ Edg
..^ Edg |
24 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
Word Vtx |
25 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word Vtx ..^
Word Vtx |
26 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
27 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
28 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
29 | 13, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
31 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
32 | 31 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
33 | 13 | lep1d 10955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
35 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
36 | 35 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
37 | 27, 30, 32, 34, 36 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
38 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
39 | 38 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
40 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
42 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
43 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
44 | 31 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
45 | 42, 43, 44 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
46 | 45 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
47 | 38 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
48 | 47 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
49 | 48 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
50 | | letr 10131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
51 | 46, 49, 50 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
52 | 41, 51 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
53 | | elnn0z 11390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
54 | 52, 53 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
55 | 54 | adantlrr 757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
56 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
57 | 39, 55, 56 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
58 | 37, 57 | mpdan 702 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
59 | 58 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
60 | 59 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
61 | 26, 60 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . 22
|
62 | 61 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . 21
|
63 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . . . . 21
|
64 | 62, 63 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . 20
|
65 | 64 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx
|
66 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . 22
|
67 | 66 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . 21
|
68 | 67 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Word Vtx
|
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx
|
70 | 65, 69 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
|
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word Vtx ..^
|
72 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
73 | 12, 7, 14, 72 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . . . . 21
|
74 | | fzoss2 12496 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
76 | 75 | sseld 3602 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
77 | 76 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
..^ ..^ |
78 | 77 | imp 445 |
. . . . . . . . . . . . . . . . 17
Word Vtx ..^
..^ |
79 | | swrd0fv 13439 |
. . . . . . . . . . . . . . . . 17
Word Vtx ..^ substr |
80 | 25, 71, 78, 79 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
Word Vtx ..^
substr |
81 | 80 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
Word Vtx ..^
substr |
82 | | fzonn0p1p1 12546 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
83 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
84 | | npcan1 10455 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
86 | 85 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
87 | 86 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
88 | 82, 87 | syl5ib 234 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
89 | 88 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
..^ ..^ |
90 | 89 | imp 445 |
. . . . . . . . . . . . . . . . 17
Word Vtx ..^
..^ |
91 | | swrd0fv 13439 |
. . . . . . . . . . . . . . . . 17
Word Vtx ..^ substr |
92 | 25, 71, 90, 91 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
Word Vtx ..^
substr |
93 | 92 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
Word Vtx ..^
substr |
94 | 81, 93 | preq12d 4276 |
. . . . . . . . . . . . . 14
Word Vtx ..^
substr substr |
95 | 94 | eleq1d 2686 |
. . . . . . . . . . . . 13
Word Vtx ..^
Edg substr substr Edg |
96 | 95 | ralbidva 2985 |
. . . . . . . . . . . 12
Word Vtx
..^ Edg ..^ substr substr Edg |
97 | 23, 96 | sylibd 229 |
. . . . . . . . . . 11
Word Vtx
..^ Edg
..^ substr substr Edg |
98 | 97 | impancom 456 |
. . . . . . . . . 10
Word Vtx
..^ Edg
..^ substr substr Edg |
99 | 98 | imp 445 |
. . . . . . . . 9
Word Vtx ..^ Edg
..^ substr substr Edg |
100 | 24, 70 | jca 554 |
. . . . . . . . . . . . . 14
Word Vtx
Word Vtx
|
101 | 100 | adantlr 751 |
. . . . . . . . . . . . 13
Word Vtx ..^ Edg
Word Vtx
|
102 | | swrd0len 13422 |
. . . . . . . . . . . . 13
Word Vtx
substr |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . 12
Word Vtx ..^ Edg
substr |
104 | 103 | oveq1d 6665 |
. . . . . . . . . . 11
Word Vtx ..^ Edg
substr |
105 | 104 | oveq2d 6666 |
. . . . . . . . . 10
Word Vtx ..^ Edg
..^ substr ..^ |
106 | 105 | raleqdv 3144 |
. . . . . . . . 9
Word Vtx ..^ Edg
..^ substr substr substr Edg ..^ substr substr Edg |
107 | 99, 106 | mpbird 247 |
. . . . . . . 8
Word Vtx ..^ Edg
..^ substr substr substr Edg |
108 | 24, 70, 102 | syl2anc 693 |
. . . . . . . . . 10
Word Vtx
substr |
109 | 85 | eqcomd 2628 |
. . . . . . . . . . 11
|
110 | 109 | ad2antrl 764 |
. . . . . . . . . 10
Word Vtx
|
111 | 108, 110 | eqtrd 2656 |
. . . . . . . . 9
Word Vtx
substr |
112 | 111 | adantlr 751 |
. . . . . . . 8
Word Vtx ..^ Edg
substr |
113 | 6, 107, 112 | 3jca 1242 |
. . . . . . 7
Word Vtx ..^ Edg
substr Word Vtx
..^ substr substr substr Edg
substr |
114 | 113 | ex 450 |
. . . . . 6
Word Vtx
..^ Edg
substr Word Vtx
..^ substr substr substr Edg substr |
115 | 114 | 3adant3 1081 |
. . . . 5
Word Vtx
..^ Edg lastS Edg
substr Word Vtx
..^ substr substr substr Edg substr |
116 | 3, 115 | syl 17 |
. . . 4
ClWWalksN
substr Word Vtx
..^ substr substr substr Edg substr |
117 | 116 | impcom 446 |
. . 3
ClWWalksN substr
Word Vtx
..^ substr substr substr Edg substr |
118 | | nnm1nn0 11334 |
. . . . 5
|
119 | 118 | ad2antrr 762 |
. . . 4
ClWWalksN
|
120 | 1, 2 | iswwlksnx 26731 |
. . . 4
substr WWalksN
substr Word Vtx
..^ substr substr substr Edg substr |
121 | 119, 120 | syl 17 |
. . 3
ClWWalksN substr
WWalksN
substr Word Vtx
..^ substr substr substr Edg substr |
122 | 117, 121 | mpbird 247 |
. 2
ClWWalksN substr WWalksN |
123 | 122 | ex 450 |
1
ClWWalksN substr WWalksN |