Metamath Proof Explorer


Theorem wwlksext2clwwlk

Description: If a word represents a walk in (in a graph) and there are edges between the last vertex of the word and another vertex and between this other vertex and the first vertex of the word, then the concatenation of the word representing the walk with this other vertex represents a closed walk. (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 27-Apr-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Hypotheses clwwlkext2edg.v V = Vtx G
clwwlkext2edg.e E = Edg G
Assertion wwlksext2clwwlk W N WWalksN G Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G

Proof

Step Hyp Ref Expression
1 clwwlkext2edg.v V = Vtx G
2 clwwlkext2edg.e E = Edg G
3 wwlknbp1 W N WWalksN G N 0 W Word Vtx G W = N + 1
4 1 wrdeqi Word V = Word Vtx G
5 4 eleq2i W Word V W Word Vtx G
6 5 biimpri W Word Vtx G W Word V
7 6 3ad2ant2 N 0 W Word Vtx G W = N + 1 W Word V
8 7 ad2antlr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V W Word V
9 s1cl Z V ⟨“ Z ”⟩ Word V
10 9 adantl W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V ⟨“ Z ”⟩ Word V
11 ccatcl W Word V ⟨“ Z ”⟩ Word V W ++ ⟨“ Z ”⟩ Word V
12 8 10 11 syl2anc W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V W ++ ⟨“ Z ”⟩ Word V
13 12 adantr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ Word V
14 1 2 wwlknp W N WWalksN G W Word V W = N + 1 i 0 ..^ N W i W i + 1 E
15 simplll W Word V W = N + 1 Z V N 0 i 0 ..^ N W Word V
16 9 adantr Z V N 0 ⟨“ Z ”⟩ Word V
17 16 ad2antlr W Word V W = N + 1 Z V N 0 i 0 ..^ N ⟨“ Z ”⟩ Word V
18 elfzo0 i 0 ..^ N i 0 N i < N
19 simp1 i 0 N i < N i 0
20 peano2nn N N + 1
21 20 3ad2ant2 i 0 N i < N N + 1
22 nn0re i 0 i
23 22 3ad2ant1 i 0 N i < N i
24 nnre N N
25 24 3ad2ant2 i 0 N i < N N
26 peano2re N N + 1
27 24 26 syl N N + 1
28 27 3ad2ant2 i 0 N i < N N + 1
29 simp3 i 0 N i < N i < N
30 24 ltp1d N N < N + 1
31 30 3ad2ant2 i 0 N i < N N < N + 1
32 23 25 28 29 31 lttrd i 0 N i < N i < N + 1
33 elfzo0 i 0 ..^ N + 1 i 0 N + 1 i < N + 1
34 19 21 32 33 syl3anbrc i 0 N i < N i 0 ..^ N + 1
35 18 34 sylbi i 0 ..^ N i 0 ..^ N + 1
36 35 adantl W Word V W = N + 1 Z V N 0 i 0 ..^ N i 0 ..^ N + 1
37 oveq2 W = N + 1 0 ..^ W = 0 ..^ N + 1
38 37 adantl W Word V W = N + 1 0 ..^ W = 0 ..^ N + 1
39 38 eleq2d W Word V W = N + 1 i 0 ..^ W i 0 ..^ N + 1
40 39 ad2antrr W Word V W = N + 1 Z V N 0 i 0 ..^ N i 0 ..^ W i 0 ..^ N + 1
41 36 40 mpbird W Word V W = N + 1 Z V N 0 i 0 ..^ N i 0 ..^ W
42 ccatval1 W Word V ⟨“ Z ”⟩ Word V i 0 ..^ W W ++ ⟨“ Z ”⟩ i = W i
43 15 17 41 42 syl3anc W Word V W = N + 1 Z V N 0 i 0 ..^ N W ++ ⟨“ Z ”⟩ i = W i
44 fzonn0p1p1 i 0 ..^ N i + 1 0 ..^ N + 1
45 44 adantl W Word V W = N + 1 Z V N 0 i 0 ..^ N i + 1 0 ..^ N + 1
46 37 eleq2d W = N + 1 i + 1 0 ..^ W i + 1 0 ..^ N + 1
47 46 ad3antlr W Word V W = N + 1 Z V N 0 i 0 ..^ N i + 1 0 ..^ W i + 1 0 ..^ N + 1
48 45 47 mpbird W Word V W = N + 1 Z V N 0 i 0 ..^ N i + 1 0 ..^ W
49 ccatval1 W Word V ⟨“ Z ”⟩ Word V i + 1 0 ..^ W W ++ ⟨“ Z ”⟩ i + 1 = W i + 1
50 15 17 48 49 syl3anc W Word V W = N + 1 Z V N 0 i 0 ..^ N W ++ ⟨“ Z ”⟩ i + 1 = W i + 1
51 43 50 preq12d W Word V W = N + 1 Z V N 0 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
52 51 ex W Word V W = N + 1 Z V N 0 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
53 52 expcom Z V N 0 W Word V W = N + 1 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
54 53 expcom N 0 Z V W Word V W = N + 1 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
55 54 3ad2ant1 N 0 W Word Vtx G W = N + 1 Z V W Word V W = N + 1 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
56 55 imp N 0 W Word Vtx G W = N + 1 Z V W Word V W = N + 1 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
57 56 expdcom W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
58 57 3imp1 W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
59 58 eleq1d W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E W i W i + 1 E
60 59 ralbidva W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E i 0 ..^ N W i W i + 1 E
61 60 biimprd W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W i W i + 1 E i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
62 61 3exp W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W i W i + 1 E i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
63 62 com34 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
64 63 3imp1 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
65 64 adantr W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
66 simpll W Word V W = N + 1 Z V N 0 W Word V
67 9 ad2antrl W Word V W = N + 1 Z V N 0 ⟨“ Z ”⟩ Word V
68 nn0p1gt0 N 0 0 < N + 1
69 68 ad2antll W Word V W = N + 1 Z V N 0 0 < N + 1
70 breq2 W = N + 1 0 < W 0 < N + 1
71 70 ad2antlr W Word V W = N + 1 Z V N 0 0 < W 0 < N + 1
72 69 71 mpbird W Word V W = N + 1 Z V N 0 0 < W
73 hashneq0 W Word V 0 < W W
74 73 ad2antrr W Word V W = N + 1 Z V N 0 0 < W W
75 72 74 mpbid W Word V W = N + 1 Z V N 0 W
76 ccatval1lsw W Word V ⟨“ Z ”⟩ Word V W W ++ ⟨“ Z ”⟩ W 1 = lastS W
77 66 67 75 76 syl3anc W Word V W = N + 1 Z V N 0 W ++ ⟨“ Z ”⟩ W 1 = lastS W
78 oveq1 W = N + 1 W 1 = N + 1 - 1
79 78 ad2antlr W Word V W = N + 1 Z V N 0 W 1 = N + 1 - 1
80 nn0cn N 0 N
81 80 ad2antll W Word V W = N + 1 Z V N 0 N
82 pncan1 N N + 1 - 1 = N
83 81 82 syl W Word V W = N + 1 Z V N 0 N + 1 - 1 = N
84 79 83 eqtrd W Word V W = N + 1 Z V N 0 W 1 = N
85 84 fveq2d W Word V W = N + 1 Z V N 0 W ++ ⟨“ Z ”⟩ W 1 = W ++ ⟨“ Z ”⟩ N
86 77 85 eqtr3d W Word V W = N + 1 Z V N 0 lastS W = W ++ ⟨“ Z ”⟩ N
87 ccatws1ls W Word V Z V W ++ ⟨“ Z ”⟩ W = Z
88 87 ad2ant2r W Word V W = N + 1 Z V N 0 W ++ ⟨“ Z ”⟩ W = Z
89 fveq2 W = N + 1 W ++ ⟨“ Z ”⟩ W = W ++ ⟨“ Z ”⟩ N + 1
90 89 ad2antlr W Word V W = N + 1 Z V N 0 W ++ ⟨“ Z ”⟩ W = W ++ ⟨“ Z ”⟩ N + 1
91 88 90 eqtr3d W Word V W = N + 1 Z V N 0 Z = W ++ ⟨“ Z ”⟩ N + 1
92 86 91 preq12d W Word V W = N + 1 Z V N 0 lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
93 92 expcom Z V N 0 W Word V W = N + 1 lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
94 93 expcom N 0 Z V W Word V W = N + 1 lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
95 94 3ad2ant1 N 0 W Word Vtx G W = N + 1 Z V W Word V W = N + 1 lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
96 95 imp N 0 W Word Vtx G W = N + 1 Z V W Word V W = N + 1 lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
97 96 com12 W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
98 97 3adant3 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
99 98 imp W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
100 99 eleq1d W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1 E
101 100 biimpa W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1 E
102 simprl1 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V N 0
103 102 adantr W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E N 0
104 fveq2 i = N W ++ ⟨“ Z ”⟩ i = W ++ ⟨“ Z ”⟩ N
105 fvoveq1 i = N W ++ ⟨“ Z ”⟩ i + 1 = W ++ ⟨“ Z ”⟩ N + 1
106 104 105 preq12d i = N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
107 106 eleq1d i = N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1 E
108 107 ralsng N 0 i N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1 E
109 103 108 syl W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1 E
110 101 109 mpbird W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
111 ralunb i 0 ..^ N N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E i N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
112 65 110 111 sylanbrc W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ N N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
113 elnn0uz N 0 N 0
114 102 113 sylib W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V N 0
115 114 adantr W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E N 0
116 fzosplitsn N 0 0 ..^ N + 1 = 0 ..^ N N
117 115 116 syl W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E 0 ..^ N + 1 = 0 ..^ N N
118 112 117 raleqtrrdv W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ N + 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
119 ccatws1len W Word V W ++ ⟨“ Z ”⟩ = W + 1
120 119 3ad2ant1 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E W ++ ⟨“ Z ”⟩ = W + 1
121 120 ad2antrr W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W ++ ⟨“ Z ”⟩ = W + 1
122 121 oveq1d W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W ++ ⟨“ Z ”⟩ 1 = W + 1 - 1
123 oveq1 W = N + 1 W + 1 = N + 1 + 1
124 123 oveq1d W = N + 1 W + 1 - 1 = N + 1 + 1 - 1
125 1cnd N 0 1
126 80 125 addcld N 0 N + 1
127 126 125 pncand N 0 N + 1 + 1 - 1 = N + 1
128 127 3ad2ant1 N 0 W Word Vtx G W = N + 1 N + 1 + 1 - 1 = N + 1
129 128 adantr N 0 W Word Vtx G W = N + 1 Z V N + 1 + 1 - 1 = N + 1
130 124 129 sylan9eq W = N + 1 N 0 W Word Vtx G W = N + 1 Z V W + 1 - 1 = N + 1
131 130 3ad2antl2 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V W + 1 - 1 = N + 1
132 131 adantr W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W + 1 - 1 = N + 1
133 122 132 eqtrd W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W ++ ⟨“ Z ”⟩ 1 = N + 1
134 133 oveq2d W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E 0 ..^ W ++ ⟨“ Z ”⟩ 1 = 0 ..^ N + 1
135 118 134 raleqtrrdv W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
136 135 exp42 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
137 14 136 syl W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
138 137 imp41 W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
139 138 adantrr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
140 lswccats1 W Word V Z V lastS W ++ ⟨“ Z ”⟩ = Z
141 8 140 sylancom W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W ++ ⟨“ Z ”⟩ = Z
142 68 3ad2ant1 N 0 W Word Vtx G W = N + 1 0 < N + 1
143 70 3ad2ant3 N 0 W Word Vtx G W = N + 1 0 < W 0 < N + 1
144 142 143 mpbird N 0 W Word Vtx G W = N + 1 0 < W
145 144 ad2antlr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V 0 < W
146 ccatfv0 W Word V ⟨“ Z ”⟩ Word V 0 < W W ++ ⟨“ Z ”⟩ 0 = W 0
147 8 10 145 146 syl3anc W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V W ++ ⟨“ Z ”⟩ 0 = W 0
148 141 147 preq12d W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 = Z W 0
149 148 eleq1d W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E Z W 0 E
150 149 biimprcd Z W 0 E W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E
151 150 adantl lastS W Z E Z W 0 E W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E
152 151 impcom W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E
153 13 139 152 3jca W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ Word V i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E
154 ccatws1len W Word Vtx G W ++ ⟨“ Z ”⟩ = W + 1
155 154 3ad2ant2 N 0 W Word Vtx G W = N + 1 W ++ ⟨“ Z ”⟩ = W + 1
156 123 3ad2ant3 N 0 W Word Vtx G W = N + 1 W + 1 = N + 1 + 1
157 80 125 125 addassd N 0 N + 1 + 1 = N + 1 + 1
158 1p1e2 1 + 1 = 2
159 158 oveq2i N + 1 + 1 = N + 2
160 157 159 eqtrdi N 0 N + 1 + 1 = N + 2
161 160 3ad2ant1 N 0 W Word Vtx G W = N + 1 N + 1 + 1 = N + 2
162 155 156 161 3eqtrd N 0 W Word Vtx G W = N + 1 W ++ ⟨“ Z ”⟩ = N + 2
163 162 ad3antlr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ = N + 2
164 2nn 2
165 nn0nnaddcl N 0 2 N + 2
166 164 165 mpan2 N 0 N + 2
167 166 3ad2ant1 N 0 W Word Vtx G W = N + 1 N + 2
168 1 2 isclwwlknx N + 2 W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G W ++ ⟨“ Z ”⟩ Word V i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E W ++ ⟨“ Z ”⟩ = N + 2
169 167 168 syl N 0 W Word Vtx G W = N + 1 W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G W ++ ⟨“ Z ”⟩ Word V i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E W ++ ⟨“ Z ”⟩ = N + 2
170 169 ad3antlr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G W ++ ⟨“ Z ”⟩ Word V i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E W ++ ⟨“ Z ”⟩ = N + 2
171 153 163 170 mpbir2and W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G
172 171 exp31 W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G
173 3 172 mpdan W N WWalksN G Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G
174 173 imp W N WWalksN G Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G