Step | Hyp | Ref
| Expression |
1 | | peano2nn0 11333 |
. . . . . . . . . . . 12
|
2 | | iswwlksn 26730 |
. . . . . . . . . . . 12
WWalksN WWalks |
3 | 1, 2 | syl 17 |
. . . . . . . . . . 11
WWalksN WWalks |
4 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
Vtx Vtx |
5 | 4 | wwlkbp 26732 |
. . . . . . . . . . . . . . . . . 18
WWalks
Word Vtx |
6 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx
|
7 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
8 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
9 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
10 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
11 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
12 | 1, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
13 | 12 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
14 | | subadd2 10285 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
15 | 14 | bicomd 213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
16 | 9, 10, 13, 15 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
17 | 7, 16 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . . . 22
|
18 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
19 | 18 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . 22
|
20 | 17, 19 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . 21
|
21 | 20 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
|
22 | 21 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
|
23 | 6, 22 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
|
24 | 5, 23 | simpl2im 658 |
. . . . . . . . . . . . . . . . 17
WWalks
|
25 | 24 | imp 445 |
. . . . . . . . . . . . . . . 16
WWalks
|
26 | 25 | imp 445 |
. . . . . . . . . . . . . . 15
WWalks
|
27 | 26 | opeq2d 4409 |
. . . . . . . . . . . . . 14
WWalks
|
28 | 27 | oveq2d 6666 |
. . . . . . . . . . . . 13
WWalks substr
substr |
29 | | simpll 790 |
. . . . . . . . . . . . . . 15
WWalks WWalks |
30 | | nn0ge0 11318 |
. . . . . . . . . . . . . . . . . . 19
|
31 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . 20
|
34 | 32, 33 | addge02d 10616 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 30, 34 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
36 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . 20
|
38 | 36, 37, 37 | addassd 10062 |
. . . . . . . . . . . . . . . . . . 19
|
39 | | 1p1e2 11134 |
. . . . . . . . . . . . . . . . . . . . 21
|
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | 40 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 38, 41 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
43 | 35, 42 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . 17
|
44 | 43 | adantl 482 |
. . . . . . . . . . . . . . . 16
WWalks |
45 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
|
46 | 45 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
WWalks
|
47 | 44, 46 | mpbird 247 |
. . . . . . . . . . . . . . 15
WWalks |
48 | 29, 47 | jca 554 |
. . . . . . . . . . . . . 14
WWalks
WWalks
|
49 | | wwlksm1edg 26767 |
. . . . . . . . . . . . . 14
WWalks substr
WWalks |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
WWalks substr
WWalks |
51 | 28, 50 | eqeltrd 2701 |
. . . . . . . . . . . 12
WWalks substr
WWalks |
52 | 51 | expcom 451 |
. . . . . . . . . . 11
WWalks substr
WWalks |
53 | 3, 52 | sylbid 230 |
. . . . . . . . . 10
WWalksN
substr WWalks |
54 | 53 | com12 32 |
. . . . . . . . 9
WWalksN
substr WWalks |
55 | 54 | adantr 481 |
. . . . . . . 8
WWalksN
substr
WWalks |
56 | 55 | imp 445 |
. . . . . . 7
WWalksN substr
WWalks |
57 | | wwlksnextprop.e |
. . . . . . . . . . . 12
Edg |
58 | 4, 57 | wwlknp 26734 |
. . . . . . . . . . 11
WWalksN
Word Vtx ..^ |
59 | | simpll 790 |
. . . . . . . . . . . . . 14
Word Vtx Word Vtx |
60 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 1, 60 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
62 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | 33, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
64 | 63 | lep1d 10955 |
. . . . . . . . . . . . . . . . . 18
|
65 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . 18
|
66 | 1, 61, 64, 65 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . 17
|
67 | 66 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
68 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
70 | 67, 69 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
|
71 | 70 | adantll 750 |
. . . . . . . . . . . . . 14
Word Vtx
|
72 | 59, 71 | jca 554 |
. . . . . . . . . . . . 13
Word Vtx
Word Vtx
|
73 | 72 | ex 450 |
. . . . . . . . . . . 12
Word Vtx
Word Vtx
|
74 | 73 | 3adant3 1081 |
. . . . . . . . . . 11
Word Vtx ..^ Word Vtx |
75 | 58, 74 | syl 17 |
. . . . . . . . . 10
WWalksN
Word Vtx |
76 | 75 | adantr 481 |
. . . . . . . . 9
WWalksN
Word Vtx
|
77 | 76 | imp 445 |
. . . . . . . 8
WWalksN
Word Vtx
|
78 | | swrd0len 13422 |
. . . . . . . 8
Word Vtx
substr |
79 | 77, 78 | syl 17 |
. . . . . . 7
WWalksN substr |
80 | 56, 79 | jca 554 |
. . . . . 6
WWalksN substr
WWalks substr |
81 | | iswwlksn 26730 |
. . . . . . 7
substr
WWalksN
substr
WWalks substr |
82 | 81 | adantl 482 |
. . . . . 6
WWalksN substr
WWalksN
substr
WWalks substr |
83 | 80, 82 | mpbird 247 |
. . . . 5
WWalksN substr
WWalksN |
84 | 83 | exp31 630 |
. . . 4
WWalksN
substr WWalksN |
85 | | wwlksnextprop.x |
. . . 4
WWalksN
|
86 | 84, 85 | eleq2s 2719 |
. . 3
substr WWalksN
|
87 | 86 | 3imp 1256 |
. 2
substr
WWalksN |
88 | 85 | wwlksnextproplem1 26804 |
. . . 4
substr |
89 | 88 | 3adant2 1080 |
. . 3
substr
|
90 | | simp2 1062 |
. . 3
|
91 | 89, 90 | eqtrd 2656 |
. 2
substr
|
92 | | fveq1 6190 |
. . . 4
substr substr |
93 | 92 | eqeq1d 2624 |
. . 3
substr substr |
94 | | wwlksnextprop.y |
. . 3
WWalksN |
95 | 93, 94 | elrab2 3366 |
. 2
substr
substr WWalksN
substr |
96 | 87, 91, 95 | sylanbrc 698 |
1
substr
|