Step | Hyp | Ref
| Expression |
1 | | simp1 1054 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝐺 ∈ USGraph
) |
2 | | uz3m2nn 11607 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
3 | 2 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
ℕ) |
4 | | simp2 1055 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑋 ∈ 𝑉) |
5 | | av-numclwwlkovf.f |
. . . . . . 7
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
6 | | av-numclwwlkffin.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
7 | | av-numclwwlkovfel2.e |
. . . . . . 7
⊢ 𝐸 = (Edg‘𝐺) |
8 | 5, 6, 7 | av-numclwwlkovfel2 41514 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ (𝑁 − 2) ∈ ℕ ∧
𝑋 ∈ 𝑉) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋))) |
9 | 1, 3, 4, 8 | syl3anc 1318 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋))) |
10 | | ccatws1cl 13249 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑃 ++ 〈“𝑋”〉) ∈ Word 𝑉) |
11 | 10 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word 𝑉 → (𝑋 ∈ 𝑉 → (𝑃 ++ 〈“𝑋”〉) ∈ Word 𝑉)) |
12 | 11 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (𝑋 ∈ 𝑉 → (𝑃 ++ 〈“𝑋”〉) ∈ Word 𝑉)) |
13 | 12 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑋 ∈ 𝑉 → (𝑃 ++ 〈“𝑋”〉) ∈ Word 𝑉)) |
14 | 13 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑉 → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ++ 〈“𝑋”〉) ∈ Word 𝑉)) |
15 | 14 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ++ 〈“𝑋”〉) ∈ Word 𝑉)) |
16 | 15 | imp 444 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑃 ++ 〈“𝑋”〉) ∈ Word 𝑉) |
17 | 6 | nbgrisvtx 40581 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ USGraph ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑄 ∈ 𝑉) |
18 | 17 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄 ∈ 𝑉)) |
19 | | s1cl 13235 |
. . . . . . . . . . . . 13
⊢ (𝑄 ∈ 𝑉 → 〈“𝑄”〉 ∈ Word 𝑉) |
20 | 18, 19 | syl6 34 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 〈“𝑄”〉 ∈ Word 𝑉)) |
21 | 20 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 〈“𝑄”〉 ∈ Word 𝑉)) |
22 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 〈“𝑄”〉 ∈ Word 𝑉)) |
23 | 22 | imp 444 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 〈“𝑄”〉 ∈ Word 𝑉) |
24 | | ccatcl 13212 |
. . . . . . . . 9
⊢ (((𝑃 ++ 〈“𝑋”〉) ∈ Word 𝑉 ∧ 〈“𝑄”〉 ∈ Word 𝑉) → ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉) |
25 | 16, 23, 24 | syl2an2r 872 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉) |
26 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → 𝑃 ∈ Word 𝑉) |
27 | 26 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → 𝑃 ∈ Word 𝑉) |
28 | 27 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈
(0..^((#‘𝑃) −
1))) → 𝑃 ∈ Word
𝑉) |
29 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 ∈
ℕ0) |
30 | 29 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈
(0..^((#‘𝑃) −
1))) → 𝑖 ∈
ℕ0) |
31 | | lencl 13179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
32 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^((#‘𝑃) − 1)) ↔ (𝑖 ∈ ℕ0
∧ ((#‘𝑃) −
1) ∈ ℕ ∧ 𝑖
< ((#‘𝑃) −
1))) |
33 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → 𝑖 ∈ ℝ) |
35 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℝ) |
36 | | peano2rem 10227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((#‘𝑃) ∈
ℝ → ((#‘𝑃)
− 1) ∈ ℝ) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 1) ∈
ℝ) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → ((#‘𝑃) − 1) ∈
ℝ) |
39 | 35 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (#‘𝑃) ∈ ℝ) |
40 | 34, 38, 39 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (𝑖 ∈ ℝ ∧ ((#‘𝑃) − 1) ∈ ℝ
∧ (#‘𝑃) ∈
ℝ)) |
41 | 35 | ltm1d 10835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 1) < (#‘𝑃)) |
42 | 41 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → ((#‘𝑃) − 1) < (#‘𝑃)) |
43 | | lttr 9993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑖 ∈ ℝ ∧
((#‘𝑃) − 1)
∈ ℝ ∧ (#‘𝑃) ∈ ℝ) → ((𝑖 < ((#‘𝑃) − 1) ∧
((#‘𝑃) − 1)
< (#‘𝑃)) →
𝑖 < (#‘𝑃))) |
44 | 43 | expcomd 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℝ ∧
((#‘𝑃) − 1)
∈ ℝ ∧ (#‘𝑃) ∈ ℝ) → (((#‘𝑃) − 1) < (#‘𝑃) → (𝑖 < ((#‘𝑃) − 1) → 𝑖 < (#‘𝑃)))) |
45 | 40, 42, 44 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (𝑖 < ((#‘𝑃) − 1) → 𝑖 < (#‘𝑃))) |
46 | 45 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑖 ∈ ℕ0
∧ 𝑖 <
((#‘𝑃) − 1))
→ ((#‘𝑃) ∈
ℕ0 → 𝑖 < (#‘𝑃))) |
47 | 46 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑖 ∈ ℕ0
∧ ((#‘𝑃) −
1) ∈ ℕ ∧ 𝑖
< ((#‘𝑃) −
1)) → ((#‘𝑃)
∈ ℕ0 → 𝑖 < (#‘𝑃))) |
48 | 32, 47 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 ∈ (0..^((#‘𝑃) − 1)) →
((#‘𝑃) ∈
ℕ0 → 𝑖 < (#‘𝑃))) |
49 | 31, 48 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ Word 𝑉 → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 < (#‘𝑃))) |
50 | 49 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → 𝑖 < (#‘𝑃))) |
51 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑖 ∈
(0..^((#‘𝑃) −
1)) → 𝑖 <
(#‘𝑃))) |
52 | 51 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈
(0..^((#‘𝑃) −
1))) → 𝑖 <
(#‘𝑃)) |
53 | 28, 30, 52 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈
(0..^((#‘𝑃) −
1))) → (𝑃 ∈ Word
𝑉 ∧ 𝑖 ∈ ℕ0 ∧ 𝑖 < (#‘𝑃))) |
54 | 4 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑋 ∈ 𝑉) |
55 | 18 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄 ∈ 𝑉)) |
56 | 55 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑄 ∈ 𝑉)) |
57 | 56 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑄 ∈ 𝑉)) |
58 | 57 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑄 ∈ 𝑉) |
59 | 54, 58 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈
(0..^((#‘𝑃) −
1))) → (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) |
61 | | ccat2s1fvw 13267 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃 ∈ Word 𝑉 ∧ 𝑖 ∈ ℕ0 ∧ 𝑖 < (#‘𝑃)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖) = (𝑃‘𝑖)) |
62 | 61 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 ∈ Word 𝑉 ∧ 𝑖 ∈ ℕ0 ∧ 𝑖 < (#‘𝑃)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → (𝑃‘𝑖) = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖)) |
63 | 53, 60, 62 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈
(0..^((#‘𝑃) −
1))) → (𝑃‘𝑖) = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖)) |
64 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑃 ∈ Word 𝑉) |
65 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℕ0) |
66 | 65 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑖 ∈ ℕ0
∧ ((#‘𝑃) −
1) ∈ ℕ ∧ 𝑖
< ((#‘𝑃) −
1)) → (𝑖 + 1) ∈
ℕ0) |
67 | 32, 66 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑖 + 1) ∈
ℕ0) |
68 | 67 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑖 + 1) ∈
ℕ0) |
69 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → 1 ∈ ℝ) |
70 | 34, 69, 39 | ltaddsubd 10506 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → ((𝑖 + 1) < (#‘𝑃) ↔ 𝑖 < ((#‘𝑃) − 1))) |
71 | 70 | biimprd 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (𝑖 < ((#‘𝑃) − 1) → (𝑖 + 1) < (#‘𝑃))) |
72 | 71 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑖 <
((#‘𝑃) − 1))
→ ((#‘𝑃) ∈
ℕ0 → (𝑖 + 1) < (#‘𝑃))) |
73 | 72 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑖 ∈ ℕ0
∧ ((#‘𝑃) −
1) ∈ ℕ ∧ 𝑖
< ((#‘𝑃) −
1)) → ((#‘𝑃)
∈ ℕ0 → (𝑖 + 1) < (#‘𝑃))) |
74 | 32, 73 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 ∈ (0..^((#‘𝑃) − 1)) →
((#‘𝑃) ∈
ℕ0 → (𝑖 + 1) < (#‘𝑃))) |
75 | 31, 74 | mpan9 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑖 + 1) < (#‘𝑃)) |
76 | 64, 68, 75 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃))) |
77 | 76 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ Word 𝑉 → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)))) |
78 | 77 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)))) |
79 | 78 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑖 ∈
(0..^((#‘𝑃) −
1)) → (𝑃 ∈ Word
𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)))) |
80 | 79 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈
(0..^((#‘𝑃) −
1))) → (𝑃 ∈ Word
𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃))) |
81 | | ccat2s1fvw 13267 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ ℕ0 ∧ (𝑖 + 1) < (#‘𝑃)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
82 | 80, 60, 81 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈
(0..^((#‘𝑃) −
1))) → (((𝑃 ++
〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
83 | 82 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈
(0..^((#‘𝑃) −
1))) → (𝑃‘(𝑖 + 1)) = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))) |
84 | 63, 83 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈
(0..^((#‘𝑃) −
1))) → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))}) |
85 | 84 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈
(0..^((#‘𝑃) −
1))) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
86 | 85 | ralbidva 2968 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (∀𝑖 ∈
(0..^((#‘𝑃) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
87 | 86 | biimpd 218 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸)) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (∀𝑖 ∈
(0..^((#‘𝑃) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
88 | 87 | exp41 636 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (∀𝑖 ∈
(0..^((#‘𝑃) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸))))) |
89 | 88 | com15 99 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑖 ∈
(0..^((#‘𝑃) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸))))) |
90 | 89 | expd 451 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
(0..^((#‘𝑃) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 → (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸)))))) |
91 | 90 | 3imp21 1269 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸)))) |
92 | 91 | 3impib 1254 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸))) |
93 | 92 | impcom 445 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
94 | 93 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸) |
95 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑃 ∈ Word 𝑉) |
96 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑃) =
(𝑁 − 2) →
((#‘𝑃) − 1) =
((𝑁 − 2) −
1)) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝑃) =
(𝑁 − 2) ∧ 𝑁 ∈
(ℤ≥‘3)) → ((#‘𝑃) − 1) = ((𝑁 − 2) − 1)) |
98 | | eluzelcn 11575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℂ) |
99 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℂ) |
100 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ ℂ) |
101 | 98, 99, 100 | subsub4d 10302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1))) |
102 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (2 + 1) =
3 |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈
(ℤ≥‘3) → (2 + 1) = 3) |
104 | 103 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (2 + 1)) = (𝑁 − 3)) |
105 | | uznn0sub 11595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 3) ∈
ℕ0) |
106 | 104, 105 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (2 + 1)) ∈
ℕ0) |
107 | 101, 106 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) − 1) ∈
ℕ0) |
108 | 107 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝑃) =
(𝑁 − 2) ∧ 𝑁 ∈
(ℤ≥‘3)) → ((𝑁 − 2) − 1) ∈
ℕ0) |
109 | 97, 108 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝑃) =
(𝑁 − 2) ∧ 𝑁 ∈
(ℤ≥‘3)) → ((#‘𝑃) − 1) ∈
ℕ0) |
110 | 109 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((#‘𝑃) −
1) ∈ ℕ0) |
111 | 31, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) < (#‘𝑃)) |
112 | 111 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((#‘𝑃) −
1) < (#‘𝑃)) |
113 | 95, 110, 112 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (𝑁 − 2)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈
ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))) |
114 | 113 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = (𝑁 − 2) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈
ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃))))) |
115 | 114 | a1dd 48 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → (𝑁 ∈ (ℤ≥‘3)
→ (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈
ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))))) |
116 | 115 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → (𝑁 ∈ (ℤ≥‘3)
→ (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈
ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))))) |
117 | 116 | 3imp 1249 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈
ℕ0 ∧ ((#‘𝑃) − 1) < (#‘𝑃)))) |
118 | 117 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0
∧ ((#‘𝑃) −
1) < (#‘𝑃)))) |
119 | 118 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0
∧ ((#‘𝑃) −
1) < (#‘𝑃)))) |
120 | 119 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0
∧ ((#‘𝑃) −
1) < (#‘𝑃))) |
121 | 18 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄 ∈ 𝑉)) |
122 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
123 | 122 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉)) → 𝑋 ∈ 𝑉) |
124 | 121, 123 | jctild 564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉))) |
125 | 124 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ Word 𝑉 → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)))) |
126 | 125 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)))) |
127 | 126 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)))) |
128 | 127 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)))) |
129 | 128 | 3adant3 1074 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)))) |
130 | 129 | imp31 447 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) |
131 | | ccat2s1fvw 13267 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ0
∧ ((#‘𝑃) −
1) < (#‘𝑃)) ∧
(𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) − 1)) = (𝑃‘((#‘𝑃) − 1))) |
132 | 120, 130,
131 | syl2an2r 872 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) − 1)) = (𝑃‘((#‘𝑃) − 1))) |
133 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℂ) |
134 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℂ |
135 | | npcan 10169 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑃) ∈
ℂ ∧ 1 ∈ ℂ) → (((#‘𝑃) − 1) + 1) = (#‘𝑃)) |
136 | 133, 134,
135 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑃) ∈
ℕ0 → (((#‘𝑃) − 1) + 1) = (#‘𝑃)) |
137 | 31, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → (((#‘𝑃) − 1) + 1) = (#‘𝑃)) |
138 | 137 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (((#‘𝑃) − 1) + 1) = (#‘𝑃)) |
139 | 138 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (((#‘𝑃) − 1) + 1) = (#‘𝑃)) |
140 | 139 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((#‘𝑃) − 1) + 1) = (#‘𝑃)) |
141 | 140 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(((#‘𝑃) − 1) + 1)) = (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘(#‘𝑃))) |
142 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑃 ∈ Word 𝑉) → 𝑃 ∈ Word 𝑉) |
143 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑃 ∈ Word 𝑉) → (#‘𝑃) = (#‘𝑃)) |
144 | 142, 143 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃))) |
145 | 144 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃))) |
146 | 122 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑋 ∈ 𝑉) |
147 | 18 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄 ∈ 𝑉)) |
148 | 147 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑄 ∈ 𝑉) |
149 | | ccatw2s1p1 13265 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)) = 𝑋) |
150 | 145, 146,
148, 149 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑃 ∈ Word 𝑉) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)) = 𝑋) |
151 | 150 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑃 ∈ Word 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)) = 𝑋)) |
152 | 151 | expcom 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ Word 𝑉 → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)) = 𝑋))) |
153 | 152 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)) = 𝑋))) |
154 | 153 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)) = 𝑋))) |
155 | 154 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)) = 𝑋))) |
156 | 155 | 3adant3 1074 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)) = 𝑋))) |
157 | 156 | imp31 447 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)) = 𝑋) |
158 | 141, 157 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(((#‘𝑃) − 1) + 1)) = 𝑋) |
159 | 132, 158 | preq12d 4220 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) − 1)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘(((#‘𝑃) − 1) + 1))} = {(𝑃‘((#‘𝑃) − 1)), 𝑋}) |
160 | | lsw 13204 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1))) |
161 | 160 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃‘0) = 𝑋 ∧ 𝑃 ∈ Word 𝑉) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1))) |
162 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃‘0) = 𝑋 ∧ 𝑃 ∈ Word 𝑉) → (𝑃‘0) = 𝑋) |
163 | 161, 162 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃‘0) = 𝑋 ∧ 𝑃 ∈ Word 𝑉) → {( lastS ‘𝑃), (𝑃‘0)} = {(𝑃‘((#‘𝑃) − 1)), 𝑋}) |
164 | 163 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃‘0) = 𝑋 ∧ 𝑃 ∈ Word 𝑉) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)) |
165 | 164 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃‘0) = 𝑋 ∧ 𝑃 ∈ Word 𝑉) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)) |
166 | 165 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘0) = 𝑋 → (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸))) |
167 | 166 | com3l 87 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸 → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸))) |
168 | 167 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)) |
169 | 168 | 3adant2 1073 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸)) |
170 | 169 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((#‘𝑃) = (𝑁 − 2) → ((𝑃‘0) = 𝑋 → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸))) |
171 | 170 | 3imp 1249 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸) |
172 | 171 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(𝑃‘((#‘𝑃) − 1)), 𝑋} ∈ 𝐸) |
173 | 159, 172 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) − 1)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘(((#‘𝑃) − 1) + 1))} ∈ 𝐸) |
174 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(#‘𝑃) =
(#‘𝑃) |
175 | 174, 149 | mpanl2 713 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)) = 𝑋) |
176 | | ccatw2s1p2 13266 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = (#‘𝑃)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1)) = 𝑄) |
177 | 174, 176 | mpanl2 713 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1)) = 𝑄) |
178 | 175, 177 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}) |
179 | 178 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉) → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})) |
180 | 179 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑄 ∈ 𝑉 → (𝑋 ∈ 𝑉 → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))) |
181 | 18, 180 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑋 ∈ 𝑉 → (𝑃 ∈ Word 𝑉 → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))) |
182 | 181 | com24 93 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 ∈ USGraph → (𝑃 ∈ Word 𝑉 → (𝑋 ∈ 𝑉 → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))) |
183 | 182 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → (𝐺 ∈ USGraph → (𝑋 ∈ 𝑉 → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄})))) |
184 | 183 | impd 446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Word 𝑉 → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))) |
185 | 184 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))) |
186 | 185 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))) |
187 | 186 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))) |
188 | 187 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}))) |
189 | 188 | imp31 447 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} = {𝑋, 𝑄}) |
190 | 7 | nbusgreledg 40575 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑄, 𝑋} ∈ 𝐸)) |
191 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑄, 𝑋} = {𝑋, 𝑄} |
192 | 191 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑄, 𝑋} ∈ 𝐸 ↔ {𝑋, 𝑄} ∈ 𝐸) |
193 | 192 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑄, 𝑋} ∈ 𝐸 → {𝑋, 𝑄} ∈ 𝐸) |
194 | 190, 193 | syl6bi 242 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ USGraph → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑄} ∈ 𝐸)) |
195 | 194 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑄} ∈ 𝐸)) |
196 | 195 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → {𝑋, 𝑄} ∈ 𝐸)) |
197 | 196 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑋, 𝑄} ∈ 𝐸) |
198 | 189, 197 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} ∈ 𝐸) |
199 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
((#‘𝑃) −
1) ∈ V |
200 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(#‘𝑃) ∈
V |
201 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = ((#‘𝑃) − 1) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖) = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) − 1))) |
202 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = ((#‘𝑃) − 1) → (𝑖 + 1) = (((#‘𝑃) − 1) + 1)) |
203 | 202 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = ((#‘𝑃) − 1) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1)) = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(((#‘𝑃) − 1) +
1))) |
204 | 201, 203 | preq12d 4220 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = ((#‘𝑃) − 1) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} = {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) − 1)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘(((#‘𝑃) − 1) +
1))}) |
205 | 204 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑖 = ((#‘𝑃) − 1) → ({(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) − 1)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘(((#‘𝑃) − 1) + 1))} ∈ 𝐸)) |
206 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (#‘𝑃) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖) = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃))) |
207 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (#‘𝑃) → (𝑖 + 1) = ((#‘𝑃) + 1)) |
208 | 207 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (#‘𝑃) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1)) = (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))) |
209 | 206, 208 | preq12d 4220 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (#‘𝑃) → {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} = {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))}) |
210 | 209 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (#‘𝑃) → ({(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} ∈ 𝐸)) |
211 | 199, 200,
205, 210 | ralpr 4185 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
{((#‘𝑃) − 1),
(#‘𝑃)} {(((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ ({(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) − 1)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘(((#‘𝑃) − 1) + 1))} ∈ 𝐸 ∧ {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(#‘𝑃)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘((#‘𝑃) + 1))} ∈ 𝐸)) |
212 | 173, 198,
211 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸) |
213 | 94, 212 | jca 553 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
214 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑃) ∈
ℕ0 → 2 ∈ ℂ) |
215 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑃) ∈
ℕ0 → 1 ∈ ℂ) |
216 | 133, 214,
215 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ
∧ 1 ∈ ℂ)) |
217 | 31, 216 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ
∧ 1 ∈ ℂ)) |
218 | 217 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → ((#‘𝑃) ∈ ℂ ∧ 2 ∈ ℂ
∧ 1 ∈ ℂ)) |
219 | 218 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((#‘𝑃) ∈
ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ)) |
220 | | addsubass 10170 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑃) ∈
ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘𝑃) + 2) − 1) =
((#‘𝑃) + (2 −
1))) |
221 | 219, 220 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (((#‘𝑃) + 2)
− 1) = ((#‘𝑃) +
(2 − 1))) |
222 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2
− 1) = 1 |
223 | 222 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑃) + (2
− 1)) = ((#‘𝑃)
+ 1) |
224 | 221, 223 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (((#‘𝑃) + 2)
− 1) = ((#‘𝑃) +
1)) |
225 | 224 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (0..^(((#‘𝑃) +
2) − 1)) = (0..^((#‘𝑃) + 1))) |
226 | | 0zd 11266 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 0 ∈ ℤ) |
227 | 31 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℤ) |
228 | 227 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) → (#‘𝑃) ∈ ℤ) |
229 | 228 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘𝑃) ∈
ℤ) |
230 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤
𝑁)) |
231 | | df-3 10957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 3 = (2 +
1) |
232 | 231 | breq1i 4590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (3 ≤
𝑁 ↔ (2 + 1) ≤ 𝑁) |
233 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 2 ∈
ℤ |
234 | | zltp1le 11304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 < 𝑁 ↔ (2 + 1) ≤ 𝑁)) |
235 | 233, 234 | mpan 702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℤ → (2 <
𝑁 ↔ (2 + 1) ≤ 𝑁)) |
236 | 235 | biimprd 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℤ → ((2 + 1)
≤ 𝑁 → 2 < 𝑁)) |
237 | 232, 236 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 → 2 < 𝑁)) |
238 | 237 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℤ ∧ 3 ≤
𝑁) → 2 < 𝑁) |
239 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
240 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 2 ∈
ℝ |
241 | 239, 240 | jctil 558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℤ → (2 ∈
ℝ ∧ 𝑁 ∈
ℝ)) |
242 | 241 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℤ ∧ 3 ≤
𝑁) → (2 ∈ ℝ
∧ 𝑁 ∈
ℝ)) |
243 | | posdif 10400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ) → (2 < 𝑁 ↔ 0 < (𝑁 − 2))) |
244 | 242, 243 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℤ ∧ 3 ≤
𝑁) → (2 < 𝑁 ↔ 0 < (𝑁 − 2))) |
245 | 238, 244 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ 3 ≤
𝑁) → 0 < (𝑁 − 2)) |
246 | 245 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 0 < (𝑁 − 2)) |
247 | 230, 246 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘3) → 0 < (𝑁 − 2)) |
248 | 247 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑃) =
(𝑁 − 2) ∧ 𝑁 ∈
(ℤ≥‘3)) → 0 < (𝑁 − 2)) |
249 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) =
(𝑁 − 2) → (0
< (#‘𝑃) ↔ 0
< (𝑁 −
2))) |
250 | 249 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑃) =
(𝑁 − 2) ∧ 𝑁 ∈
(ℤ≥‘3)) → (0 < (#‘𝑃) ↔ 0 < (𝑁 − 2))) |
251 | 248, 250 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑃) =
(𝑁 − 2) ∧ 𝑁 ∈
(ℤ≥‘3)) → 0 < (#‘𝑃)) |
252 | 251 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 0 < (#‘𝑃)) |
253 | | fzosplitprm1 12443 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℤ ∧ (#‘𝑃) ∈ ℤ ∧ 0 < (#‘𝑃)) → (0..^((#‘𝑃) + 1)) = ((0..^((#‘𝑃) − 1)) ∪
{((#‘𝑃) − 1),
(#‘𝑃)})) |
254 | 226, 229,
252, 253 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (0..^((#‘𝑃) +
1)) = ((0..^((#‘𝑃)
− 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})) |
255 | 225, 254 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ ((#‘𝑃) = (𝑁 − 2) ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (0..^(((#‘𝑃) +
2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)})) |
256 | 255 | expr 641 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2)) → (𝑁 ∈ (ℤ≥‘3)
→ (0..^(((#‘𝑃) +
2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))) |
257 | 256 | 3adant3 1074 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ≥‘3)
→ (0..^(((#‘𝑃) +
2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}))) |
258 | 257 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪
{((#‘𝑃) − 1),
(#‘𝑃)}))) |
259 | 258 | 3ad2ant3 1077 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪
{((#‘𝑃) − 1),
(#‘𝑃)}))) |
260 | 259 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪
{((#‘𝑃) − 1),
(#‘𝑃)})) |
261 | 260 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (0..^(((#‘𝑃) + 2) − 1)) = ((0..^((#‘𝑃) − 1)) ∪
{((#‘𝑃) − 1),
(#‘𝑃)})) |
262 | 261 | raleqdv 3121 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ ((0..^((#‘𝑃) − 1)) ∪ {((#‘𝑃) − 1), (#‘𝑃)}){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
263 | | ralunb 3756 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
((0..^((#‘𝑃) −
1)) ∪ {((#‘𝑃)
− 1), (#‘𝑃)}){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
264 | 262, 263 | syl6bb 275 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {((#‘𝑃) − 1), (#‘𝑃)} {(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸))) |
265 | 213, 264 | mpbird 246 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸) |
266 | | simp11 1084 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → 𝑃 ∈ Word 𝑉) |
267 | 266 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑃 ∈ Word 𝑉) |
268 | 4 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑋 ∈ 𝑉) |
269 | 55 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → 𝑄 ∈ 𝑉)) |
270 | 269 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑄 ∈ 𝑉) |
271 | | ccatw2s1len 13254 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉) → (#‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) =
((#‘𝑃) +
2)) |
272 | 267, 268,
270, 271 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (#‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) =
((#‘𝑃) +
2)) |
273 | 272 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ((#‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) − 1) =
(((#‘𝑃) + 2) −
1)) |
274 | 273 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) − 1)) =
(0..^(((#‘𝑃) + 2)
− 1))) |
275 | 274 | raleqdv 3121 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) −
1)){(((𝑃 ++
〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^(((#‘𝑃) + 2) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
276 | 265, 275 | mpbird 246 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) −
1)){(((𝑃 ++
〈“𝑋”〉) ++ 〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸) |
277 | | lswccats1 13263 |
. . . . . . . . . . . 12
⊢ (((𝑃 ++ 〈“𝑋”〉) ∈ Word 𝑉 ∧ 𝑄 ∈ 𝑉) → ( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) = 𝑄) |
278 | 10, 277 | stoic3 1692 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉) → ( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) = 𝑄) |
279 | 267, 268,
270, 278 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) = 𝑄) |
280 | 2 | nngt0d 10941 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘3) → 0 < (𝑁 − 2)) |
281 | 280, 249 | syl5ibr 235 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑃) =
(𝑁 − 2) → (𝑁 ∈
(ℤ≥‘3) → 0 < (#‘𝑃))) |
282 | 281 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ≥‘3)
→ 0 < (#‘𝑃))) |
283 | 282 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → 0 < (#‘𝑃))) |
284 | 283 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → 0 < (#‘𝑃))) |
285 | 284 | imp 444 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → 0 < (#‘𝑃)) |
286 | 285 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → 0 < (#‘𝑃)) |
287 | | ccat2s1fst 13268 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ Word 𝑉 ∧ 0 < (#‘𝑃)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑄 ∈ 𝑉)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘0) = (𝑃‘0)) |
288 | 267, 286,
268, 270, 287 | syl22anc 1319 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘0) = (𝑃‘0)) |
289 | 279, 288 | preq12d 4220 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘0)} =
{𝑄, (𝑃‘0)}) |
290 | 190 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑄, 𝑋} ∈ 𝐸)) |
291 | 290 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑄, 𝑋} ∈ 𝐸)) |
292 | 291 | biimpa 500 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑄, 𝑋} ∈ 𝐸) |
293 | | preq2 4213 |
. . . . . . . . . . . . 13
⊢ ((𝑃‘0) = 𝑋 → {𝑄, (𝑃‘0)} = {𝑄, 𝑋}) |
294 | 293 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ ((𝑃‘0) = 𝑋 → ({𝑄, (𝑃‘0)} ∈ 𝐸 ↔ {𝑄, 𝑋} ∈ 𝐸)) |
295 | 294 | 3ad2ant3 1077 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ({𝑄, (𝑃‘0)} ∈ 𝐸 ↔ {𝑄, 𝑋} ∈ 𝐸)) |
296 | 295 | ad2antlr 759 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ({𝑄, (𝑃‘0)} ∈ 𝐸 ↔ {𝑄, 𝑋} ∈ 𝐸)) |
297 | 292, 296 | mpbird 246 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {𝑄, (𝑃‘0)} ∈ 𝐸) |
298 | 289, 297 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘0)} ∈
𝐸) |
299 | 25, 276, 298 | 3jca 1235 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘0)} ∈ 𝐸)) |
300 | 266 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → 𝑃 ∈ Word 𝑉) |
301 | 4 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
302 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → 𝑄 ∈ 𝑉) |
303 | 300, 301,
302, 271 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → (#‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) =
((#‘𝑃) +
2)) |
304 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑃) =
(𝑁 − 2) →
((#‘𝑃) + 2) = ((𝑁 − 2) +
2)) |
305 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℂ |
306 | | npcan 10169 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑁 −
2) + 2) = 𝑁) |
307 | 98, 305, 306 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) + 2) = 𝑁) |
308 | 304, 307 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝑃) =
(𝑁 − 2) ∧ 𝑁 ∈
(ℤ≥‘3)) → ((#‘𝑃) + 2) = 𝑁) |
309 | 308 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑃) =
(𝑁 − 2) → (𝑁 ∈
(ℤ≥‘3) → ((#‘𝑃) + 2) = 𝑁)) |
310 | 309 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑁 ∈ (ℤ≥‘3)
→ ((#‘𝑃) + 2) =
𝑁)) |
311 | 310 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((#‘𝑃) + 2) = 𝑁)) |
312 | 311 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → ((#‘𝑃) + 2) = 𝑁)) |
313 | 312 | imp 444 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → ((#‘𝑃) + 2) = 𝑁) |
314 | 313 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → ((#‘𝑃) + 2) = 𝑁) |
315 | 303, 314 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ 𝑉) → (#‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) = 𝑁) |
316 | 315 | ex 449 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ 𝑉 → (#‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) = 𝑁)) |
317 | 269, 316 | syld 46 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (#‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) = 𝑁)) |
318 | 317 | imp 444 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → (#‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)) = 𝑁) |
319 | 299, 318 | jca 553 |
. . . . . 6
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋)) ∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋)) → ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) = 𝑁)) |
320 | 319 | exp31 628 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ 𝐸) ∧ (#‘𝑃) = (𝑁 − 2) ∧ (𝑃‘0) = 𝑋) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) = 𝑁)))) |
321 | 9, 320 | sylbid 229 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) = 𝑁)))) |
322 | 321 | com23 84 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑄 ∈ (𝐺 NeighbVtx 𝑋) → (𝑃 ∈ (𝑋𝐹(𝑁 − 2)) → ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) = 𝑁)))) |
323 | 322 | 3imp 1249 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) = 𝑁)) |
324 | | eluzge3nn 11606 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
325 | 6, 7 | isclwwlksnx 41197 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) = 𝑁))) |
326 | 324, 325 | syl 17 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) = 𝑁))) |
327 | 326 | 3ad2ant3 1077 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑃 ++
〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) = 𝑁))) |
328 | 327 | 3ad2ant1 1075 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) − 1)){(((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘𝑖), (((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉)), (((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)‘0)} ∈ 𝐸) ∧ (#‘((𝑃 ++ 〈“𝑋”〉) ++
〈“𝑄”〉)) = 𝑁))) |
329 | 323, 328 | mpbird 246 |
1
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑄 ∈ (𝐺 NeighbVtx 𝑋) ∧ 𝑃 ∈ (𝑋𝐹(𝑁 − 2))) → ((𝑃 ++ 〈“𝑋”〉) ++ 〈“𝑄”〉) ∈ (𝑁 ClWWalkSN 𝐺)) |