Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝐺 ∈ USGraph
) |
2 | | uz3m2nn 11731 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
3 | 2 | 3ad2ant3 1084 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
ℕ) |
4 | | simp2 1062 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑋 ∈ 𝑉) |
5 | | numclwwlkovf.f |
. . . . . . 7
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
6 | | numclwwlkffin.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
7 | | numclwwlkovfel2.e |
. . . . . . 7
⊢ 𝐸 = (Edg‘𝐺) |
8 | 5, 6, 7 | numclwwlkovfel2 27216 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ (𝑁 − 2) ∈ ℕ ∧
𝑋 ∈ 𝑉) → (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋))) |
9 | 1, 3, 4, 8 | syl3anc 1326 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋))) |
10 | | simpr11 1145 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → 𝑊 ∈ Word 𝑉) |
11 | 10 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑊 ∈ Word 𝑉) |
12 | | simpll2 1101 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑋 ∈ 𝑉) |
13 | 6 | nbgrisvtx 26255 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ USGraph ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑌 ∈ 𝑉) |
14 | 13 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → 𝑌 ∈ 𝑉)) |
15 | 14 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → 𝑌 ∈ 𝑉)) |
16 | 15 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → 𝑌 ∈ 𝑉)) |
17 | 16 | imp 445 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑌 ∈ 𝑉) |
18 | | ccatw2s1cl 13401 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉) |
19 | 11, 12, 17, 18 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉) |
20 | 6, 7 | numclwwlkovf2exlem2 27212 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ ((0..^((#‘𝑊) − 1)) ∪ {((#‘𝑊) − 1), (#‘𝑊)}){(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸) |
21 | | simp11 1091 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → 𝑊 ∈ Word 𝑉) |
22 | 21 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑊 ∈ Word 𝑉) |
23 | | ccatw2s1len 13402 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (#‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) =
((#‘𝑊) +
2)) |
24 | 22, 12, 17, 23 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (#‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) =
((#‘𝑊) +
2)) |
25 | 24 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ((#‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) − 1) =
(((#‘𝑊) + 2) −
1)) |
26 | 25 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) − 1)) =
(0..^(((#‘𝑊) + 2)
− 1))) |
27 | | simp3 1063 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑁 ∈
(ℤ≥‘3)) |
28 | | simp2 1062 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (#‘𝑊) = (𝑁 − 2)) |
29 | 27, 28 | anim12i 590 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → (𝑁 ∈ (ℤ≥‘3)
∧ (#‘𝑊) = (𝑁 − 2))) |
30 | 29 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑁 ∈ (ℤ≥‘3)
∧ (#‘𝑊) = (𝑁 − 2))) |
31 | | numclwwlkovf2exlem1 27211 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (#‘𝑊) = (𝑁 − 2)) → (0..^(((#‘𝑊) + 2) − 1)) =
((0..^((#‘𝑊) −
1)) ∪ {((#‘𝑊)
− 1), (#‘𝑊)})) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (0..^(((#‘𝑊) + 2) − 1)) = ((0..^((#‘𝑊) − 1)) ∪
{((#‘𝑊) − 1),
(#‘𝑊)})) |
33 | 26, 32 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) − 1)) =
((0..^((#‘𝑊) −
1)) ∪ {((#‘𝑊)
− 1), (#‘𝑊)})) |
34 | 33 | raleqdv 3144 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) −
1)){(((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ ((0..^((#‘𝑊) − 1)) ∪ {((#‘𝑊) − 1), (#‘𝑊)}){(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
35 | 20, 34 | mpbird 247 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) −
1)){(((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸) |
36 | | ccatws1cl 13396 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑊 ++ 〈“𝑋”〉) ∈ Word 𝑉) |
37 | | lswccats1 13411 |
. . . . . . . . . . . 12
⊢ (((𝑊 ++ 〈“𝑋”〉) ∈ Word 𝑉 ∧ 𝑌 ∈ 𝑉) → ( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) = 𝑌) |
38 | 36, 37 | stoic3 1701 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) = 𝑌) |
39 | 22, 12, 17, 38 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) = 𝑌) |
40 | 2 | nngt0d 11064 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘3) → 0 < (𝑁 − 2)) |
41 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑊) =
(𝑁 − 2) → (0
< (#‘𝑊) ↔ 0
< (𝑁 −
2))) |
42 | 40, 41 | syl5ibr 236 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) =
(𝑁 − 2) → (𝑁 ∈
(ℤ≥‘3) → 0 < (#‘𝑊))) |
43 | 42 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑁 ∈ (ℤ≥‘3)
→ 0 < (#‘𝑊))) |
44 | 43 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → 0 < (#‘𝑊))) |
45 | 44 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → 0 < (#‘𝑊))) |
46 | 45 | imp 445 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → 0 < (#‘𝑊)) |
47 | 46 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → 0 < (#‘𝑊)) |
48 | | ccat2s1fst 13416 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘0) = (𝑊‘0)) |
49 | 22, 47, 12, 17, 48 | syl22anc 1327 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘0) = (𝑊‘0)) |
50 | 39, 49 | preq12d 4276 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘0)} =
{𝑌, (𝑊‘0)}) |
51 | 7 | nbusgreledg 26249 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑌, 𝑋} ∈ 𝐸)) |
52 | 51 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑌 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑌, 𝑋} ∈ 𝐸)) |
53 | 52 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑌, 𝑋} ∈ 𝐸)) |
54 | 53 | biimpa 501 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑌, 𝑋} ∈ 𝐸) |
55 | | preq2 4269 |
. . . . . . . . . . . . 13
⊢ ((𝑊‘0) = 𝑋 → {𝑌, (𝑊‘0)} = {𝑌, 𝑋}) |
56 | 55 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ ((𝑊‘0) = 𝑋 → ({𝑌, (𝑊‘0)} ∈ 𝐸 ↔ {𝑌, 𝑋} ∈ 𝐸)) |
57 | 56 | 3ad2ant3 1084 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ({𝑌, (𝑊‘0)} ∈ 𝐸 ↔ {𝑌, 𝑋} ∈ 𝐸)) |
58 | 57 | ad2antlr 763 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ({𝑌, (𝑊‘0)} ∈ 𝐸 ↔ {𝑌, 𝑋} ∈ 𝐸)) |
59 | 54, 58 | mpbird 247 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑌, (𝑊‘0)} ∈ 𝐸) |
60 | 50, 59 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘0)} ∈
𝐸) |
61 | 19, 35, 60 | 3jca 1242 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘0)} ∈ 𝐸)) |
62 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) =
(𝑁 − 2) →
((#‘𝑊) + 2) = ((𝑁 − 2) +
2)) |
63 | | eluzelcn 11699 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℂ) |
64 | | 2cn 11091 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
65 | | npcan 10290 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑁 −
2) + 2) = 𝑁) |
66 | 63, 64, 65 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) + 2) = 𝑁) |
67 | 62, 66 | sylan9eq 2676 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) =
(𝑁 − 2) ∧ 𝑁 ∈
(ℤ≥‘3)) → ((#‘𝑊) + 2) = 𝑁) |
68 | 67 | ex 450 |
. . . . . . . . . . . . 13
⊢
((#‘𝑊) =
(𝑁 − 2) → (𝑁 ∈
(ℤ≥‘3) → ((#‘𝑊) + 2) = 𝑁)) |
69 | 68 | 3ad2ant2 1083 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑁 ∈ (ℤ≥‘3)
→ ((#‘𝑊) + 2) =
𝑁)) |
70 | 69 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((#‘𝑊) + 2) = 𝑁)) |
71 | 70 | 3ad2ant3 1084 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → ((#‘𝑊) + 2) = 𝑁)) |
72 | 71 | imp 445 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) → ((#‘𝑊) + 2) = 𝑁) |
73 | 72 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ((#‘𝑊) + 2) = 𝑁) |
74 | 24, 73 | eqtrd 2656 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → (#‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) = 𝑁) |
75 | 61, 74 | jca 554 |
. . . . . 6
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) = 𝑁)) |
76 | 75 | exp31 630 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (#‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) = 𝑁)))) |
77 | 9, 76 | sylbid 230 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) = 𝑁)))) |
78 | 77 | com23 86 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑌 ∈ (𝐺 NeighbVtx 𝑋) → (𝑊 ∈ (𝑋𝐹(𝑁 − 2)) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) = 𝑁)))) |
79 | 78 | 3imp 1256 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) = 𝑁)) |
80 | | eluzge3nn 11730 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
81 | 6, 7 | isclwwlksnx 26889 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) = 𝑁))) |
82 | 80, 81 | syl 17 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) = 𝑁))) |
83 | 82 | 3ad2ant3 1084 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) = 𝑁))) |
84 | 83 | 3ad2ant1 1082 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) − 1)){(((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)), (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)) = 𝑁))) |
85 | 79, 84 | mpbird 247 |
1
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑊 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺)) |