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