Step | Hyp | Ref
| Expression |
1 | | wlkv 26508 |
. . 3
Walks
|
2 | | eqid 2622 |
. . . . 5
Vtx Vtx |
3 | | eqid 2622 |
. . . . 5
iEdg iEdg |
4 | 2, 3 | iswlk 26506 |
. . . 4
Walks Word iEdg Vtx
..^if- iEdg iEdg |
5 | | wrdred1 13349 |
. . . . . . . . 9
Word
iEdg
..^ Word iEdg |
6 | 5 | a1i 11 |
. . . . . . . 8
Walks
Word iEdg ..^ Word iEdg |
7 | 3 | wlkf 26510 |
. . . . . . . . . 10
Walks Word iEdg |
8 | | redwlklem 26568 |
. . . . . . . . . . 11
Word iEdg
Vtx
..^ ..^ Vtx |
9 | 8 | 3exp 1264 |
. . . . . . . . . 10
Word
iEdg
Vtx ..^ ..^ Vtx |
10 | 7, 9 | syl 17 |
. . . . . . . . 9
Walks Vtx ..^ ..^ Vtx |
11 | 10 | imp 445 |
. . . . . . . 8
Walks Vtx ..^ ..^ Vtx |
12 | | wlkcl 26511 |
. . . . . . . . 9
Walks |
13 | | wrdred1hash 13350 |
. . . . . . . . . 10
Word iEdg ..^ |
14 | 7, 13 | sylan 488 |
. . . . . . . . 9
Walks ..^ |
15 | | nn0z 11400 |
. . . . . . . . . . . . . 14
|
16 | | fzossrbm1 12497 |
. . . . . . . . . . . . . 14
..^
..^ |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
..^
..^ |
18 | | ssralv 3666 |
. . . . . . . . . . . . 13
..^ ..^
..^if- iEdg iEdg ..^ if- iEdg iEdg |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . 12
..^if- iEdg iEdg ..^ if- iEdg iEdg |
20 | 17 | sselda 3603 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
21 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
23 | 22 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
24 | | fzo0ss1 12498 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
25 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
26 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
27 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
28 | | fzoaddel2 12523 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
29 | 25, 26, 27, 28 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
30 | 24, 29 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
31 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
33 | 32 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
34 | 23, 33 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
..^
..^
..^ |
35 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
36 | 35 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
37 | 36 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
38 | 37 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
..^ iEdg iEdg ..^ |
39 | 23 | sneqd 4189 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
40 | 38, 39 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
..^ iEdg
iEdg ..^ ..^ |
41 | 23, 33 | preq12d 4276 |
. . . . . . . . . . . . . . . 16
..^ ..^ ..^ |
42 | 41, 38 | sseq12d 3634 |
. . . . . . . . . . . . . . 15
..^
iEdg ..^ ..^ iEdg ..^ |
43 | 34, 40, 42 | ifpbi123d 1027 |
. . . . . . . . . . . . . 14
..^ if- iEdg iEdg
if- ..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
44 | 43 | biimpd 219 |
. . . . . . . . . . . . 13
..^ if- iEdg iEdg if- ..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
45 | 44 | ralimdva 2962 |
. . . . . . . . . . . 12
..^ if- iEdg iEdg
..^ if- ..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
46 | 19, 45 | syld 47 |
. . . . . . . . . . 11
..^if- iEdg iEdg ..^ if- ..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
47 | 46 | adantr 481 |
. . . . . . . . . 10
..^
..^if- iEdg iEdg ..^ if- ..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
48 | | oveq2 6658 |
. . . . . . . . . . . . 13
..^ ..^ ..^ ..^ |
49 | 48 | eqcomd 2628 |
. . . . . . . . . . . 12
..^ ..^ ..^ ..^ |
50 | 49 | raleqdv 3144 |
. . . . . . . . . . 11
..^ ..^ if- ..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^
..^ ..^ if- ..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
51 | 50 | adantl 482 |
. . . . . . . . . 10
..^
..^ if-
..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^
..^ ..^ if- ..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
52 | 47, 51 | sylibd 229 |
. . . . . . . . 9
..^
..^if- iEdg iEdg ..^ ..^ if-
..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
53 | 12, 14, 52 | syl2an2r 876 |
. . . . . . . 8
Walks
..^if- iEdg iEdg ..^ ..^ if-
..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
54 | 6, 11, 53 | 3anim123d 1406 |
. . . . . . 7
Walks Word iEdg Vtx
..^if- iEdg iEdg ..^ Word iEdg ..^ ..^ Vtx
..^ ..^ if-
..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
55 | 54 | imp 445 |
. . . . . 6
Walks
Word iEdg Vtx
..^if- iEdg iEdg ..^ Word iEdg ..^ ..^ Vtx
..^ ..^ if-
..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
56 | | id 22 |
. . . . . . 7
|
57 | | resexg 5442 |
. . . . . . 7
..^ |
58 | | resexg 5442 |
. . . . . . 7
..^ |
59 | 2, 3 | iswlk 26506 |
. . . . . . . 8
..^ ..^ ..^ Walks ..^ ..^ Word iEdg ..^ ..^ Vtx
..^ ..^ if-
..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ |
60 | 59 | bicomd 213 |
. . . . . . 7
..^ ..^ ..^ Word iEdg ..^ ..^ Vtx
..^ ..^ if-
..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ ..^ Walks ..^ |
61 | 56, 57, 58, 60 | syl3an 1368 |
. . . . . 6
..^ Word iEdg ..^ ..^ Vtx
..^ ..^ if-
..^ ..^ iEdg ..^ ..^
..^ ..^ iEdg ..^ ..^ Walks ..^ |
62 | 55, 61 | syl5ib 234 |
. . . . 5
Walks
Word iEdg Vtx
..^if- iEdg iEdg ..^ Walks ..^ |
63 | 62 | expcomd 454 |
. . . 4
Word iEdg Vtx
..^if- iEdg iEdg Walks ..^ Walks ..^ |
64 | 4, 63 | sylbid 230 |
. . 3
Walks Walks ..^ Walks ..^ |
65 | 1, 64 | mpcom 38 |
. 2
Walks Walks ..^ Walks ..^ |
66 | 65 | anabsi5 858 |
1
Walks ..^ Walks ..^ |