Step | Hyp | Ref
| Expression |
1 | | eleq1w 2684 |
. . . . . . . . 9
|
2 | | fveq2 6191 |
. . . . . . . . . 10
|
3 | | oveq1 6657 |
. . . . . . . . . 10
substr
substr |
4 | 2, 3 | eqeq12d 2637 |
. . . . . . . . 9
substr substr |
5 | 1, 4 | imbi12d 334 |
. . . . . . . 8
substr
substr |
6 | 5 | imbi2d 330 |
. . . . . . 7
substr
substr |
7 | | numclwwlk.v |
. . . . . . . 8
Vtx |
8 | | numclwwlk.q |
. . . . . . . 8
WWalksN lastS |
9 | | numclwwlk.f |
. . . . . . . 8
ClWWalksN |
10 | | numclwwlk.h |
. . . . . . . 8
ClWWalksN |
11 | | numclwwlk.r |
. . . . . . . 8
substr |
12 | 7, 8, 9, 10, 11 | numclwlk2lem2fv 27237 |
. . . . . . 7
substr |
13 | 6, 12 | chvarv 2263 |
. . . . . 6
substr |
14 | 13 | 3adant1 1079 |
. . . . 5
FriendGraph substr |
15 | 14 | imp 445 |
. . . 4
FriendGraph
substr |
16 | 7, 8, 9, 10, 11 | numclwlk2lem2f 27236 |
. . . . 5
FriendGraph |
17 | 16 | ffvelrnda 6359 |
. . . 4
FriendGraph
|
18 | 15, 17 | eqeltrrd 2702 |
. . 3
FriendGraph
substr
|
19 | 18 | ralrimiva 2966 |
. 2
FriendGraph substr |
20 | 7, 8, 9, 10 | numclwwlk2lem1 27235 |
. . . . 5
FriendGraph
++
|
21 | 20 | imp 445 |
. . . 4
FriendGraph
++ |
22 | 7, 8 | numclwwlkovq 27232 |
. . . . . . . . 9
WWalksN
lastS |
23 | 22 | eleq2d 2687 |
. . . . . . . 8
WWalksN
lastS |
24 | 23 | 3adant1 1079 |
. . . . . . 7
FriendGraph
WWalksN lastS |
25 | | fveq1 6190 |
. . . . . . . . . 10
|
26 | 25 | eqeq1d 2624 |
. . . . . . . . 9
|
27 | | fveq2 6191 |
. . . . . . . . . 10
lastS lastS |
28 | 27 | neeq1d 2853 |
. . . . . . . . 9
lastS
lastS |
29 | 26, 28 | anbi12d 747 |
. . . . . . . 8
lastS lastS |
30 | 29 | elrab 3363 |
. . . . . . 7
WWalksN
lastS WWalksN
lastS |
31 | 24, 30 | syl6bb 276 |
. . . . . 6
FriendGraph
WWalksN
lastS |
32 | | wwlknbp2 26752 |
. . . . . . . . . . . . . . 15
WWalksN
Word Vtx |
33 | 7 | wrdeqi 13328 |
. . . . . . . . . . . . . . . . 17
Word Word Vtx |
34 | 33 | eleq2i 2693 |
. . . . . . . . . . . . . . . 16
Word
Word Vtx |
35 | 34 | anbi1i 731 |
. . . . . . . . . . . . . . 15
Word
Word Vtx |
36 | 32, 35 | sylibr 224 |
. . . . . . . . . . . . . 14
WWalksN
Word |
37 | | simpll 790 |
. . . . . . . . . . . . . . . 16
Word FriendGraph
Word |
38 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
39 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
41 | 38, 40 | nnaddcld 11067 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
42 | 7, 8, 9, 10 | numclwwlkovh 27234 |
. . . . . . . . . . . . . . . . . . . . . . 23
ClWWalksN |
43 | 41, 42 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . 22
ClWWalksN
|
44 | 43 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . 21
ClWWalksN
|
45 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
46 | 45 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
47 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
48 | 47, 45 | neeq12d 2855 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
49 | 46, 48 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . 22
|
50 | 49 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . . 21
ClWWalksN
ClWWalksN
|
51 | 44, 50 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . 20
ClWWalksN |
52 | 51 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . 19
FriendGraph
ClWWalksN
|
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
Word FriendGraph
ClWWalksN
|
54 | 7 | clwwlknbp 26885 |
. . . . . . . . . . . . . . . . . . . . 21
ClWWalksN
Word |
55 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word |
56 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Word Word |
57 | | df-2 11079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
59 | 58 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
60 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
61 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
62 | 60, 61, 61 | addassd 10062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
63 | 59, 62 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
64 | 63 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
65 | 64 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
66 | 65 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
67 | 66 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Word |
68 | 67 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Word |
69 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
70 | 69 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Word |
71 | 68, 70 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Word |
72 | 56, 71 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Word Word
|
73 | 72 | exp31 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word
Word |
74 | 55, 73 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Word Word
Word |
75 | 74 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Word Word Word
|
76 | 75 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . 24
FriendGraph Word Word Word
|
77 | 76 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word FriendGraph
Word Word
|
78 | 77 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
Word Word
FriendGraph Word |
79 | 78 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . 21
Word Word
FriendGraph Word |
80 | 54, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
ClWWalksN
Word FriendGraph
Word |
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
ClWWalksN
Word FriendGraph
Word |
82 | 81 | com12 32 |
. . . . . . . . . . . . . . . . . 18
Word FriendGraph
ClWWalksN
Word |
83 | 53, 82 | sylbid 230 |
. . . . . . . . . . . . . . . . 17
Word FriendGraph
Word |
84 | 83 | ralrimiv 2965 |
. . . . . . . . . . . . . . . 16
Word FriendGraph
Word |
85 | 37, 84 | jca 554 |
. . . . . . . . . . . . . . 15
Word FriendGraph
Word Word |
86 | 85 | ex 450 |
. . . . . . . . . . . . . 14
Word FriendGraph
Word Word |
87 | 36, 86 | syl 17 |
. . . . . . . . . . . . 13
WWalksN
FriendGraph Word
Word |
88 | 87 | adantr 481 |
. . . . . . . . . . . 12
WWalksN lastS FriendGraph
Word Word |
89 | 88 | imp 445 |
. . . . . . . . . . 11
WWalksN lastS
FriendGraph
Word Word |
90 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
91 | | nfmpt21 6722 |
. . . . . . . . . . . . . 14
ClWWalksN |
92 | 10, 91 | nfcxfr 2762 |
. . . . . . . . . . . . 13
|
93 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
94 | 90, 92, 93 | nfov 6676 |
. . . . . . . . . . . 12
|
95 | 94 | reuccats1 13480 |
. . . . . . . . . . 11
Word Word ++
substr |
96 | 89, 95 | syl 17 |
. . . . . . . . . 10
WWalksN lastS
FriendGraph
++
substr |
97 | 96 | imp 445 |
. . . . . . . . 9
WWalksN
lastS FriendGraph
++
substr |
98 | | simpr 477 |
. . . . . . . . . . . . . . . 16
Word |
99 | 98 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
Word |
100 | 36, 99 | syl 17 |
. . . . . . . . . . . . . 14
WWalksN
|
101 | 100 | ad4antr 768 |
. . . . . . . . . . . . 13
WWalksN
lastS
FriendGraph
++
|
102 | 101 | opeq2d 4409 |
. . . . . . . . . . . 12
WWalksN
lastS
FriendGraph
++
|
103 | 102 | oveq2d 6666 |
. . . . . . . . . . 11
WWalksN
lastS
FriendGraph
++
substr
substr |
104 | 103 | eqeq2d 2632 |
. . . . . . . . . 10
WWalksN
lastS
FriendGraph
++
substr
substr |
105 | 104 | reubidva 3125 |
. . . . . . . . 9
WWalksN
lastS FriendGraph
++
substr substr |
106 | 97, 105 | mpbird 247 |
. . . . . . . 8
WWalksN
lastS FriendGraph
++
substr |
107 | 106 | exp31 630 |
. . . . . . 7
WWalksN lastS FriendGraph
++
substr |
108 | 107 | com12 32 |
. . . . . 6
FriendGraph WWalksN lastS ++
substr |
109 | 31, 108 | sylbid 230 |
. . . . 5
FriendGraph ++
substr |
110 | 109 | imp 445 |
. . . 4
FriendGraph
++
substr |
111 | 21, 110 | mpd 15 |
. . 3
FriendGraph
substr |
112 | 111 | ralrimiva 2966 |
. 2
FriendGraph substr |
113 | 11 | f1ompt 6382 |
. 2
substr substr |
114 | 19, 112, 113 | sylanbrc 698 |
1
FriendGraph |