Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
Vtx Vtx |
2 | | eqid 2622 |
. . . 4
Edg Edg |
3 | 1, 2 | iswwlks 26728 |
. . 3
WWalks Word Vtx
..^ Edg |
4 | | lencl 13324 |
. . . . . . . . 9
Word Vtx
|
5 | | simpl 473 |
. . . . . . . . . . . . 13
|
6 | | 1red 10055 |
. . . . . . . . . . . . . 14
|
7 | | 2re 11090 |
. . . . . . . . . . . . . . 15
|
8 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
|
9 | | nn0re 11301 |
. . . . . . . . . . . . . . 15
|
10 | 9 | adantr 481 |
. . . . . . . . . . . . . 14
|
11 | | 1le2 11241 |
. . . . . . . . . . . . . . 15
|
12 | 11 | a1i 11 |
. . . . . . . . . . . . . 14
|
13 | | simpr 477 |
. . . . . . . . . . . . . 14
|
14 | 6, 8, 10, 12, 13 | letrd 10194 |
. . . . . . . . . . . . 13
|
15 | 5, 14 | jca 554 |
. . . . . . . . . . . 12
|
16 | | elnnnn0c 11338 |
. . . . . . . . . . . 12
|
17 | 15, 16 | sylibr 224 |
. . . . . . . . . . 11
|
18 | | lbfzo0 12507 |
. . . . . . . . . . 11
..^ |
19 | 17, 18 | sylibr 224 |
. . . . . . . . . 10
..^ |
20 | | nn0ge2m1nn 11360 |
. . . . . . . . . . 11
|
21 | | lbfzo0 12507 |
. . . . . . . . . . 11
..^ |
22 | 20, 21 | sylibr 224 |
. . . . . . . . . 10
..^ |
23 | 19, 22 | jca 554 |
. . . . . . . . 9
..^ ..^ |
24 | 4, 23 | sylan 488 |
. . . . . . . 8
Word Vtx ..^ ..^ |
25 | | inelcm 4032 |
. . . . . . . 8
..^ ..^
..^ ..^ |
26 | 24, 25 | syl 17 |
. . . . . . 7
Word Vtx ..^ ..^ |
27 | | wrdfn 13319 |
. . . . . . . . . . 11
Word Vtx
..^ |
28 | 27 | adantr 481 |
. . . . . . . . . 10
Word Vtx ..^ |
29 | | fnresdisj 6001 |
. . . . . . . . . 10
..^
..^ ..^
..^ |
30 | 28, 29 | syl 17 |
. . . . . . . . 9
Word Vtx ..^
..^ ..^ |
31 | | nn0ge2m1nn0 11361 |
. . . . . . . . . . . . 13
|
32 | 10 | lem1d 10957 |
. . . . . . . . . . . . 13
|
33 | 31, 5, 32 | 3jca 1242 |
. . . . . . . . . . . 12
|
34 | 4, 33 | sylan 488 |
. . . . . . . . . . 11
Word Vtx
|
35 | | elfz2nn0 12431 |
. . . . . . . . . . 11
|
36 | 34, 35 | sylibr 224 |
. . . . . . . . . 10
Word Vtx |
37 | | swrd0val 13421 |
. . . . . . . . . . . 12
Word Vtx
substr ..^ |
38 | 37 | eqeq1d 2624 |
. . . . . . . . . . 11
Word Vtx
substr
..^ |
39 | 38 | bicomd 213 |
. . . . . . . . . 10
Word Vtx
..^ substr
|
40 | 36, 39 | syldan 487 |
. . . . . . . . 9
Word Vtx ..^ substr |
41 | 30, 40 | bitr2d 269 |
. . . . . . . 8
Word Vtx substr
..^ ..^ |
42 | 41 | necon3bid 2838 |
. . . . . . 7
Word Vtx substr
..^ ..^ |
43 | 26, 42 | mpbird 247 |
. . . . . 6
Word Vtx substr
|
44 | 43 | 3ad2antl2 1224 |
. . . . 5
Word Vtx ..^
Edg substr |
45 | | swrdcl 13419 |
. . . . . . . 8
Word Vtx
substr Word
Vtx |
46 | 45 | a1d 25 |
. . . . . . 7
Word Vtx
substr Word
Vtx |
47 | 46 | 3ad2ant2 1083 |
. . . . . 6
Word Vtx ..^
Edg substr Word Vtx |
48 | 47 | imp 445 |
. . . . 5
Word Vtx ..^
Edg substr Word Vtx |
49 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
52 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . 18
|
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
55 | 51 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
56 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . . 19
|
57 | 9, 56 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
58 | 57 | lem1d 10957 |
. . . . . . . . . . . . . . . . 17
|
59 | 58 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
60 | 54, 55, 59 | 3jca 1242 |
. . . . . . . . . . . . . . 15
|
61 | 4, 60 | sylan 488 |
. . . . . . . . . . . . . 14
Word Vtx |
62 | | eluz2 11693 |
. . . . . . . . . . . . . 14
|
63 | 61, 62 | sylibr 224 |
. . . . . . . . . . . . 13
Word Vtx |
64 | 9 | lem1d 10957 |
. . . . . . . . . . . . . . . . . . 19
|
65 | 64 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
66 | 31, 5, 65 | 3jca 1242 |
. . . . . . . . . . . . . . . . 17
|
67 | 4, 66 | sylan 488 |
. . . . . . . . . . . . . . . 16
Word Vtx
|
68 | 67, 35 | sylibr 224 |
. . . . . . . . . . . . . . 15
Word Vtx |
69 | | swrd0len 13422 |
. . . . . . . . . . . . . . . 16
Word Vtx
substr |
70 | 69 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
Word Vtx
substr |
71 | 68, 70 | syldan 487 |
. . . . . . . . . . . . . 14
Word Vtx substr |
72 | 71 | fveq2d 6195 |
. . . . . . . . . . . . 13
Word Vtx substr |
73 | 63, 72 | eleqtrrd 2704 |
. . . . . . . . . . . 12
Word Vtx substr |
74 | | fzoss2 12496 |
. . . . . . . . . . . 12
substr ..^ substr ..^ |
75 | 73, 74 | syl 17 |
. . . . . . . . . . 11
Word Vtx ..^ substr ..^ |
76 | | ssralv 3666 |
. . . . . . . . . . 11
..^ substr ..^
..^
Edg
..^ substr Edg |
77 | 75, 76 | syl 17 |
. . . . . . . . . 10
Word Vtx
..^
Edg
..^ substr Edg |
78 | 68, 69 | syldan 487 |
. . . . . . . . . . . . . . . . . 18
Word Vtx substr |
79 | 78 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
Word Vtx substr |
80 | 79 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
Word Vtx ..^ substr ..^ |
81 | 80 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
Word Vtx ..^ substr
..^ |
82 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
Word Vtx Word Vtx |
83 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx ..^
Word Vtx |
84 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx ..^
|
85 | 4, 31 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . 21
Word Vtx |
86 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . 22
|
87 | | fzossrbm1 12497 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^ |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ |
89 | 85, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
Word Vtx ..^ ..^ |
90 | 89 | sselda 3603 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx ..^
..^ |
91 | | swrd0fv 13439 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx ..^ substr |
92 | 83, 84, 90, 91 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
Word Vtx ..^
substr |
93 | 92 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
Word Vtx ..^
substr |
94 | 4, 20 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
Word Vtx |
95 | | elfzom1p1elfzo 12547 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
96 | 94, 95 | sylan 488 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx ..^
..^ |
97 | | swrd0fv 13439 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx ..^ substr |
98 | 83, 84, 96, 97 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
Word Vtx ..^
substr
|
99 | 98 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
Word Vtx ..^
substr |
100 | 93, 99 | preq12d 4276 |
. . . . . . . . . . . . . . . 16
Word Vtx ..^
substr substr |
101 | 100 | ex 450 |
. . . . . . . . . . . . . . 15
Word Vtx ..^
substr substr |
102 | 81, 101 | sylbid 230 |
. . . . . . . . . . . . . 14
Word Vtx ..^ substr
substr substr |
103 | 102 | imp 445 |
. . . . . . . . . . . . 13
Word Vtx ..^ substr substr substr |
104 | 103 | eleq1d 2686 |
. . . . . . . . . . . 12
Word Vtx ..^ substr Edg
substr
substr Edg |
105 | 104 | biimpd 219 |
. . . . . . . . . . 11
Word Vtx ..^ substr Edg substr substr Edg |
106 | 105 | ralimdva 2962 |
. . . . . . . . . 10
Word Vtx
..^ substr Edg
..^ substr substr substr Edg |
107 | 77, 106 | syld 47 |
. . . . . . . . 9
Word Vtx
..^
Edg
..^ substr substr substr Edg |
108 | 107 | expcom 451 |
. . . . . . . 8
Word Vtx ..^ Edg ..^ substr substr substr Edg |
109 | 108 | com3l 89 |
. . . . . . 7
Word Vtx
..^ Edg
..^ substr substr substr Edg |
110 | 109 | a1i 11 |
. . . . . 6
Word Vtx ..^ Edg
..^ substr substr substr Edg |
111 | 110 | 3imp1 1280 |
. . . . 5
Word Vtx ..^
Edg ..^ substr substr substr Edg |
112 | 1, 2 | iswwlks 26728 |
. . . . 5
substr
WWalks
substr
substr
Word Vtx
..^ substr substr substr Edg |
113 | 44, 48, 111, 112 | syl3anbrc 1246 |
. . . 4
Word Vtx ..^
Edg substr WWalks |
114 | 113 | ex 450 |
. . 3
Word Vtx ..^
Edg substr WWalks |
115 | 3, 114 | sylbi 207 |
. 2
WWalks
substr WWalks |
116 | 115 | imp 445 |
1
WWalks substr
WWalks |