Step | Hyp | Ref
| Expression |
1 | | clwwlksext2edg.v |
. . . 4
Vtx |
2 | 1 | wwlknbp 26733 |
. . 3
WWalksN
Word |
3 | | simp3 1063 |
. . . . . . . . 9
Word Word |
4 | 3 | adantr 481 |
. . . . . . . 8
Word
WWalksN
Word |
5 | | s1cl 13382 |
. . . . . . . . 9
Word
|
6 | 5 | adantr 481 |
. . . . . . . 8
Word |
7 | | ccatcl 13359 |
. . . . . . . 8
Word Word ++
Word |
8 | 4, 6, 7 | syl2an 494 |
. . . . . . 7
Word
WWalksN ++ Word |
9 | 8 | adantr 481 |
. . . . . 6
Word WWalksN
lastS
++ Word |
10 | | clwwlksext2edg.e |
. . . . . . . . . . . 12
Edg |
11 | 1, 10 | wwlknp 26734 |
. . . . . . . . . . 11
WWalksN
Word ..^ |
12 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Word
Word |
13 | 12 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word
..^
Word |
14 | 6 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word
..^ Word |
15 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
..^
|
16 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
17 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
18 | 17 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
19 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
20 | 19 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
21 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
22 | 21 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
23 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
24 | 21, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
25 | 24 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
26 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
27 | 21 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
28 | 27 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
29 | 20, 22, 25, 26, 28 | lttrd 10198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
30 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
..^
|
31 | 16, 18, 29, 30 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
..^ |
32 | 15, 31 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
..^ |
33 | 32 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Word
..^ ..^ |
34 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
..^ ..^ |
35 | 34 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Word ..^ ..^ |
36 | 35 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Word ..^
..^ |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Word ..^
..^ |
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Word
..^ ..^
..^ |
39 | 33, 38 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word
..^ ..^ |
40 | | ccatval1 13361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word Word ..^ ++ |
41 | 13, 14, 39, 40 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Word
..^ ++ |
42 | 41 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Word
..^ ++ |
43 | | fzonn0p1p1 12546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
..^ |
44 | 43 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Word
..^ ..^ |
45 | 34 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
..^ |
46 | 45 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Word
..^ ..^
..^ |
47 | 44, 46 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word
..^ ..^ |
48 | | ccatval1 13361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word Word ..^ ++ |
49 | 13, 14, 47, 48 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Word
..^ ++ |
50 | 49 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Word
..^ ++ |
51 | 42, 50 | preq12d 4276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word
..^ ++ ++ |
52 | 51 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word
..^ ++ ++ |
53 | 52 | ralbidva 2985 |
. . . . . . . . . . . . . . . . . . . . . 22
Word ..^
..^ ++ ++ |
54 | 53 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . 21
Word ..^
..^ ++ ++ |
55 | 54 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
Word
..^ ..^ ++ ++ |
56 | 55 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
Word ..^ ..^ ++ ++ |
57 | 56 | 3impia 1261 |
. . . . . . . . . . . . . . . . . 18
Word
..^
..^ ++ ++ |
58 | 57 | com12 32 |
. . . . . . . . . . . . . . . . 17
Word ..^ ..^ ++ ++ |
59 | 58 | adantr 481 |
. . . . . . . . . . . . . . . 16
lastS Word ..^ ..^ ++ ++ |
60 | 59 | impcom 446 |
. . . . . . . . . . . . . . 15
Word ..^
lastS
..^ ++ ++ |
61 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
62 | 61 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word |
63 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
64 | 63 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Word
|
65 | | pncan1 10454 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word |
67 | 62, 66 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word
|
68 | 67 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
Word ++ ++ |
69 | 6 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word Word |
70 | | nn0p1gt0 11322 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
71 | 70 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Word
|
72 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
73 | 72 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Word
|
74 | 71, 73 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word
|
75 | | hashneq0 13155 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Word
|
76 | 12, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word
|
77 | 74, 76 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word |
78 | | ccatval1lsw 13368 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word Word
++ lastS |
79 | 12, 69, 77, 78 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
Word ++ lastS |
80 | 68, 79 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . 21
Word lastS ++ |
81 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
++ ++ |
82 | 81 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . 23
++
++ |
83 | 82 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
Word ++ ++ |
84 | | ccatws1ls 13410 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word
++ |
85 | 84 | ad2ant2r 783 |
. . . . . . . . . . . . . . . . . . . . . 22
Word ++ |
86 | 83, 85 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . 21
Word
++ |
87 | 80, 86 | preq12d 4276 |
. . . . . . . . . . . . . . . . . . . 20
Word
lastS ++ ++ |
88 | 87 | 3adantl3 1219 |
. . . . . . . . . . . . . . . . . . 19
Word ..^
lastS ++ ++ |
89 | 88 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
Word ..^
lastS
++ ++ |
90 | 89 | biimpd 219 |
. . . . . . . . . . . . . . . . 17
Word ..^
lastS
++ ++
|
91 | 90 | impr 649 |
. . . . . . . . . . . . . . . 16
Word ..^
lastS ++ ++ |
92 | | simprlr 803 |
. . . . . . . . . . . . . . . . 17
Word ..^
lastS
|
93 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
++ ++ |
94 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . 21
|
95 | 94 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
++ ++ |
96 | 93, 95 | preq12d 4276 |
. . . . . . . . . . . . . . . . . . 19
++ ++ ++ ++ |
97 | 96 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
++ ++
++ ++ |
98 | 97 | ralsng 4218 |
. . . . . . . . . . . . . . . . 17
++ ++
++ ++ |
99 | 92, 98 | syl 17 |
. . . . . . . . . . . . . . . 16
Word ..^
lastS ++ ++ ++ ++
|
100 | 91, 99 | mpbird 247 |
. . . . . . . . . . . . . . 15
Word ..^
lastS
++ ++ |
101 | | ralunb 3794 |
. . . . . . . . . . . . . . 15
..^ ++ ++
..^ ++ ++ ++ ++ |
102 | 60, 100, 101 | sylanbrc 698 |
. . . . . . . . . . . . . 14
Word ..^
lastS
..^ ++ ++ |
103 | | elnn0uz 11725 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 103 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
|
105 | 104 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
lastS |
106 | 105 | adantl 482 |
. . . . . . . . . . . . . . . 16
Word ..^
lastS
|
107 | | fzosplitsn 12576 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . 15
Word ..^
lastS ..^ ..^ |
109 | 108 | raleqdv 3144 |
. . . . . . . . . . . . . 14
Word ..^
lastS ..^ ++ ++
..^ ++ ++ |
110 | 102, 109 | mpbird 247 |
. . . . . . . . . . . . 13
Word ..^
lastS
..^ ++ ++ |
111 | | simp1 1061 |
. . . . . . . . . . . . . . . . . 18
Word
..^ Word |
112 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
lastS |
113 | | ccatws1len 13398 |
. . . . . . . . . . . . . . . . . 18
Word
++ |
114 | 111, 112,
113 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
Word ..^
lastS ++ |
115 | 114 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
Word ..^
lastS ++ |
116 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
117 | 116 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
|
118 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
119 | | addcl 10018 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
120 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
121 | 119, 120 | pncand 10393 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
122 | 63, 118, 121 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
|
123 | 117, 122 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . 21
|
124 | 123 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
|
125 | 124 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
lastS |
126 | 125 | com12 32 |
. . . . . . . . . . . . . . . . . 18
lastS
|
127 | 126 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . 17
Word
..^ lastS
|
128 | 127 | imp 445 |
. . . . . . . . . . . . . . . 16
Word ..^
lastS |
129 | 115, 128 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
Word ..^
lastS ++ |
130 | 129 | oveq2d 6666 |
. . . . . . . . . . . . . 14
Word ..^
lastS ..^ ++ ..^ |
131 | 130 | raleqdv 3144 |
. . . . . . . . . . . . 13
Word ..^
lastS ..^ ++ ++ ++
..^ ++ ++ |
132 | 110, 131 | mpbird 247 |
. . . . . . . . . . . 12
Word ..^
lastS
..^ ++ ++ ++ |
133 | 132 | exp32 631 |
. . . . . . . . . . 11
Word
..^
lastS
..^ ++ ++ ++ |
134 | 11, 133 | syl 17 |
. . . . . . . . . 10
WWalksN
lastS
..^ ++ ++ ++ |
135 | 134 | adantl 482 |
. . . . . . . . 9
Word
WWalksN
lastS ..^ ++ ++ ++ |
136 | 135 | imp 445 |
. . . . . . . 8
Word
WWalksN lastS
..^ ++ ++ ++ |
137 | 136 | adantrd 484 |
. . . . . . 7
Word
WWalksN lastS
..^ ++ ++ ++ |
138 | 137 | imp 445 |
. . . . . 6
Word WWalksN
lastS
..^ ++ ++ ++ |
139 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
Word Word |
140 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
141 | | lswccats1 13411 |
. . . . . . . . . . . . . . . . . 18
Word
lastS ++ |
142 | 139, 140,
141 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
Word lastS ++ |
143 | 142 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
Word
lastS ++ |
144 | 139 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word
Word |
145 | 6 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Word Word |
146 | 70 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
Word
|
147 | 72 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
Word |
148 | 146, 147 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
Word |
149 | 148 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word
|
150 | | ccatfv0 13367 |
. . . . . . . . . . . . . . . . . 18
Word Word
++ |
151 | 150 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
Word Word
++ |
152 | 144, 145,
149, 151 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
Word ++ |
153 | 143, 152 | preq12d 4276 |
. . . . . . . . . . . . . . 15
Word lastS ++ ++ |
154 | 153 | exp31 630 |
. . . . . . . . . . . . . 14
Word
lastS ++ ++ |
155 | 154 | com12 32 |
. . . . . . . . . . . . 13
Word
lastS ++ ++ |
156 | 155 | 3ad2ant2 1083 |
. . . . . . . . . . . 12
Word Word
lastS ++ ++ |
157 | | wwlknbp2 26752 |
. . . . . . . . . . . . 13
WWalksN
Word Vtx |
158 | 1 | wrdeqi 13328 |
. . . . . . . . . . . . . . . . 17
Word Word Vtx |
159 | 158 | eqcomi 2631 |
. . . . . . . . . . . . . . . 16
Word Vtx Word |
160 | 159 | eleq2i 2693 |
. . . . . . . . . . . . . . 15
Word Vtx
Word |
161 | 160 | biimpi 206 |
. . . . . . . . . . . . . 14
Word Vtx
Word |
162 | 161 | anim1i 592 |
. . . . . . . . . . . . 13
Word Vtx
Word |
163 | 157, 162 | syl 17 |
. . . . . . . . . . . 12
WWalksN
Word |
164 | 156, 163 | impel 485 |
. . . . . . . . . . 11
Word
WWalksN
lastS ++ ++ |
165 | 164 | imp 445 |
. . . . . . . . . 10
Word
WWalksN lastS ++ ++ |
166 | 165 | eleq1d 2686 |
. . . . . . . . 9
Word
WWalksN lastS ++ ++ |
167 | 166 | biimpcd 239 |
. . . . . . . 8
Word WWalksN
lastS ++ ++ |
168 | 167 | adantl 482 |
. . . . . . 7
lastS
Word WWalksN
lastS ++ ++ |
169 | 168 | impcom 446 |
. . . . . 6
Word WWalksN
lastS
lastS ++ ++ |
170 | 9, 138, 169 | 3jca 1242 |
. . . . 5
Word WWalksN
lastS
++ Word ..^ ++ ++ ++ lastS ++ ++ |
171 | 113 | ad2ant2r 783 |
. . . . . . . . . . 11
Word ++ |
172 | 116 | adantl 482 |
. . . . . . . . . . . 12
Word |
173 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
|
174 | 63, 173, 173 | addassd 10062 |
. . . . . . . . . . . . . 14
|
175 | | 1p1e2 11134 |
. . . . . . . . . . . . . . 15
|
176 | 175 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
177 | 174, 176 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
178 | 177 | adantl 482 |
. . . . . . . . . . . 12
|
179 | 172, 178 | sylan9eq 2676 |
. . . . . . . . . . 11
Word |
180 | 171, 179 | eqtrd 2656 |
. . . . . . . . . 10
Word ++ |
181 | 180 | ex 450 |
. . . . . . . . 9
Word ++ |
182 | 163, 181 | syl 17 |
. . . . . . . 8
WWalksN
++ |
183 | 182 | adantl 482 |
. . . . . . 7
Word
WWalksN ++ |
184 | 183 | imp 445 |
. . . . . 6
Word
WWalksN ++ |
185 | 184 | adantr 481 |
. . . . 5
Word WWalksN
lastS
++ |
186 | | 2nn 11185 |
. . . . . . . . 9
|
187 | | nn0nnaddcl 11324 |
. . . . . . . . 9
|
188 | 186, 187 | mpan2 707 |
. . . . . . . 8
|
189 | 188 | 3ad2ant2 1083 |
. . . . . . 7
Word
|
190 | 1, 10 | isclwwlksnx 26889 |
. . . . . . 7
++ ClWWalksN
++ Word ..^ ++ ++ ++ lastS ++ ++
++ |
191 | 189, 190 | syl 17 |
. . . . . 6
Word ++ ClWWalksN
++ Word ..^ ++ ++ ++ lastS ++ ++
++ |
192 | 191 | ad3antrrr 766 |
. . . . 5
Word WWalksN
lastS
++ ClWWalksN
++ Word ..^ ++ ++ ++ lastS ++ ++
++ |
193 | 170, 185,
192 | mpbir2and 957 |
. . . 4
Word WWalksN
lastS
++ ClWWalksN |
194 | 193 | exp31 630 |
. . 3
Word
WWalksN lastS
++
ClWWalksN |
195 | 2, 194 | mpancom 703 |
. 2
WWalksN
lastS
++ ClWWalksN |
196 | 195 | 3impib 1262 |
1
WWalksN
lastS
++
ClWWalksN |