Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | eqid 2610 |
. . . . . 6
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
3 | 1, 2 | clwwlknp 41195 |
. . . . 5
⊢ (𝑤 ∈ (𝑁 ClWWalkSN 𝐺) → ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺))) |
4 | | swrdcl 13271 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺)) |
5 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺)) |
6 | 5 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺)) |
7 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
Word (Vtx‘𝐺)) |
8 | 7 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺)) |
9 | | simpl1l 1105 |
. . . . . . . . . . 11
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑤 ∈ Word
(Vtx‘𝐺)) |
10 | 9 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → 𝑤 ∈ Word (Vtx‘𝐺)) |
11 | | uz3m2nn 11607 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
12 | 11 | ad2antlr 759 |
. . . . . . . . . 10
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑁 − 2) ∈
ℕ) |
13 | | 0le2 10988 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
2 |
14 | | eluzelre 11574 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℝ) |
15 | | 2re 10967 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℝ) |
17 | 14, 16 | subge02d 10498 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → (0 ≤ 2 ↔ (𝑁 − 2) ≤ 𝑁)) |
18 | 13, 17 | mpbii 222 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ≤ 𝑁) |
19 | 18 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ≤
𝑁) |
20 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) = 𝑁 → ((𝑁 − 2) ≤ (#‘𝑤) ↔ (𝑁 − 2) ≤ 𝑁)) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) → ((𝑁 − 2) ≤ (#‘𝑤) ↔ (𝑁 − 2) ≤ 𝑁)) |
22 | 21 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) → ((𝑁 − 2) ≤ (#‘𝑤) ↔ (𝑁 − 2) ≤ 𝑁)) |
23 | 22 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑁 − 2) ≤
(#‘𝑤) ↔ (𝑁 − 2) ≤ 𝑁)) |
24 | 19, 23 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ≤
(#‘𝑤)) |
25 | 24 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑁 − 2) ≤ (#‘𝑤)) |
26 | | swrdn0 13282 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (𝑁 − 2) ∈ ℕ ∧ (𝑁 − 2) ≤ (#‘𝑤)) → (𝑤 substr 〈0, (𝑁 − 2)〉) ≠
∅) |
27 | 10, 12, 25, 26 | syl3anc 1318 |
. . . . . . . . 9
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤 substr 〈0, (𝑁 − 2)〉) ≠
∅) |
28 | 8, 27 | jca 553 |
. . . . . . . 8
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝑤 substr 〈0, (𝑁 − 2)〉) ≠
∅)) |
29 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
30 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℤ |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℤ) |
32 | 29, 31 | zsubcld 11363 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℤ) |
33 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 2) ∈ ℤ
→ ((𝑁 − 2)
− 1) ∈ ℤ) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) − 1) ∈
ℤ) |
35 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
36 | 29, 35 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ∈ ℤ) |
37 | 14, 16 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℝ) |
38 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ ℝ) |
39 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℝ) |
40 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℝ → 2 ∈
ℝ) |
41 | 39, 40 | subge02d 10498 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℝ → (0 ≤ 2
↔ (𝑁 − 2) ≤
𝑁)) |
42 | 13, 41 | mpbii 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℝ → (𝑁 − 2) ≤ 𝑁) |
43 | 42 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 − 2) ∈ ℝ ∧
𝑁 ∈ ℝ ∧ 1
∈ ℝ) → (𝑁
− 2) ≤ 𝑁) |
44 | | lesub1 10401 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 − 2) ∈ ℝ ∧
𝑁 ∈ ℝ ∧ 1
∈ ℝ) → ((𝑁
− 2) ≤ 𝑁 ↔
((𝑁 − 2) − 1)
≤ (𝑁 −
1))) |
45 | 43, 44 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 − 2) ∈ ℝ ∧
𝑁 ∈ ℝ ∧ 1
∈ ℝ) → ((𝑁
− 2) − 1) ≤ (𝑁 − 1)) |
46 | 37, 14, 38, 45 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) − 1) ≤ (𝑁 − 1)) |
47 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 − 1) ∈
(ℤ≥‘((𝑁 − 2) − 1)) ↔ (((𝑁 − 2) − 1) ∈
ℤ ∧ (𝑁 − 1)
∈ ℤ ∧ ((𝑁
− 2) − 1) ≤ (𝑁 − 1))) |
48 | 34, 36, 46, 47 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ∈
(ℤ≥‘((𝑁 − 2) − 1))) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 1) ∈
(ℤ≥‘((𝑁 − 2) − 1))) |
50 | | simpll 786 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑤 ∈ Word
(Vtx‘𝐺)) |
51 | | simplr 788 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (#‘𝑤) = 𝑁) |
52 | | uzuzle23 11605 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑁 ∈
(ℤ≥‘2)) |
54 | | av-extwwlkfablem2lem 41507 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) = (𝑁 −
2)) |
55 | 50, 51, 53, 54 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) = (𝑁 −
2)) |
56 | 55 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1) = ((𝑁
− 2) − 1)) |
57 | 56 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (ℤ≥‘((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) − 1)) =
(ℤ≥‘((𝑁 − 2) − 1))) |
58 | 49, 57 | eleqtrrd 2691 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 1) ∈
(ℤ≥‘((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1))) |
59 | | fzoss2 12365 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 1) ∈
(ℤ≥‘((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) − 1)) →
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)) ⊆ (0..^(𝑁 − 1))) |
60 | | ssralv 3629 |
. . . . . . . . . . . . . . 15
⊢
((0..^((#‘(𝑤
substr 〈0, (𝑁 −
2)〉)) − 1)) ⊆ (0..^(𝑁 − 1)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
62 | 52 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ 𝑁 ∈
(ℤ≥‘2))) |
63 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘2))
↔ ((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ 𝑁 ∈
(ℤ≥‘2))) |
64 | 62, 63 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2))) |
65 | 64, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) = (𝑁 −
2)) |
66 | 65 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1) = ((𝑁
− 2) − 1)) |
67 | 66 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (0..^((#‘(𝑤
substr 〈0, (𝑁 −
2)〉)) − 1)) = (0..^((𝑁 − 2) − 1))) |
68 | 67 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)) ↔ 𝑖 ∈ (0..^((𝑁 − 2) − 1)))) |
69 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
𝑤 ∈ Word
(Vtx‘𝐺)) |
70 | | fzossfz 12357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(0..^(𝑁 − 1))
⊆ (0...(𝑁 −
1)) |
71 | 14 | lem1d 10836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ≤ 𝑁) |
72 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) ↔ ((𝑁 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ≤ 𝑁)) |
73 | 36, 29, 71, 72 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
74 | | fzss2 12252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
76 | 70, 75 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘3) → (0..^(𝑁 − 1)) ⊆ (0...𝑁)) |
77 | | ige2m2fzo 12398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈ (0..^(𝑁 − 1))) |
78 | 52, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ (0..^(𝑁 − 1))) |
79 | 76, 78 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ (0...𝑁)) |
80 | 79 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
(0...𝑁)) |
81 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑤) = 𝑁 → (0...(#‘𝑤)) = (0...𝑁)) |
82 | 81 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑤) = 𝑁 → ((𝑁 − 2) ∈ (0...(#‘𝑤)) ↔ (𝑁 − 2) ∈ (0...𝑁))) |
83 | 82 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑁 − 2)
∈ (0...(#‘𝑤))
↔ (𝑁 − 2) ∈
(0...𝑁))) |
84 | 80, 83 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
(0...(#‘𝑤))) |
85 | 84 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
(𝑁 − 2) ∈
(0...(#‘𝑤))) |
86 | | elfzom1elfzo 12403 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 − 2) ∈ ℤ ∧
𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
𝑖 ∈ (0..^(𝑁 − 2))) |
87 | 32, 86 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (0..^((𝑁 − 2) − 1))) → 𝑖 ∈ (0..^(𝑁 − 2))) |
88 | 87 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
𝑖 ∈ (0..^(𝑁 − 2))) |
89 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (𝑁 − 2) ∈ (0...(#‘𝑤)) ∧ 𝑖 ∈ (0..^(𝑁 − 2))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖) = (𝑤‘𝑖)) |
90 | 69, 85, 88, 89 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖) = (𝑤‘𝑖)) |
91 | 90 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
(𝑤‘𝑖) = ((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖)) |
92 | 79 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
(0...𝑁)) |
93 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑁 − 2)
∈ (0...(#‘𝑤))
↔ (𝑁 − 2) ∈
(0...𝑁))) |
94 | 92, 93 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
(0...(#‘𝑤))) |
95 | 94 | ad4ant23 1289 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
(𝑁 − 2) ∈
(0...(#‘𝑤))) |
96 | 32 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
ℤ) |
97 | | elfzom1elp1fzo 12402 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 − 2) ∈ ℤ ∧
𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
(𝑖 + 1) ∈ (0..^(𝑁 − 2))) |
98 | 96, 97 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
(𝑖 + 1) ∈ (0..^(𝑁 − 2))) |
99 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (𝑁 − 2) ∈ (0...(#‘𝑤)) ∧ (𝑖 + 1) ∈ (0..^(𝑁 − 2))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1)) = (𝑤‘(𝑖 + 1))) |
100 | 69, 95, 98, 99 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1)) = (𝑤‘(𝑖 + 1))) |
101 | 100 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
(𝑤‘(𝑖 + 1)) = ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))) |
102 | 91, 101 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈ (0..^((𝑁 − 2) − 1))) →
{(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))}) |
103 | 102 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑖 ∈
(0..^((𝑁 − 2) −
1)) → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))})) |
104 | 68, 103 | sylbid 229 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)) → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))})) |
105 | 104 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1))) → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))}) |
106 | 105 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1))) → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
107 | 106 | ralbidva 2968 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) − 1)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
108 | 61, 107 | sylibd 228 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) − 1)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
109 | 108 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) − 1)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
110 | 109 | com23 84 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑁 ∈ (ℤ≥‘3)
→ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
111 | 110 | a1dd 48 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ({( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺) → (𝑁 ∈ (ℤ≥‘3)
→ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))) |
112 | 111 | 3imp1 1272 |
. . . . . . . . 9
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
113 | 112 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
114 | | ige3m2fz 12236 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ (1...𝑁)) |
115 | 114 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
(1...𝑁)) |
116 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑤) = 𝑁 → (1...(#‘𝑤)) = (1...𝑁)) |
117 | 116 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) = 𝑁 → ((𝑁 − 2) ∈ (1...(#‘𝑤)) ↔ (𝑁 − 2) ∈ (1...𝑁))) |
118 | 117 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑁 − 2)
∈ (1...(#‘𝑤))
↔ (𝑁 − 2) ∈
(1...𝑁))) |
119 | 115, 118 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
(1...(#‘𝑤))) |
120 | | swrd0fvlsw 13295 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))) → ( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)) = (𝑤‘((𝑁 − 2) − 1))) |
121 | 50, 119, 120 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ( lastS ‘(𝑤
substr 〈0, (𝑁 −
2)〉)) = (𝑤‘((𝑁 − 2) − 1))) |
122 | | swrd0fv0 13292 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = (𝑤‘0)) |
123 | 50, 119, 122 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤 substr 〈0,
(𝑁 −
2)〉)‘0) = (𝑤‘0)) |
124 | 121, 123 | preq12d 4220 |
. . . . . . . . . . . 12
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ {( lastS ‘(𝑤
substr 〈0, (𝑁 −
2)〉)), ((𝑤 substr
〈0, (𝑁 −
2)〉)‘0)} = {(𝑤‘((𝑁 − 2) − 1)), (𝑤‘0)}) |
125 | 124 | 3ad2antl1 1216 |
. . . . . . . . . . 11
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ {( lastS ‘(𝑤
substr 〈0, (𝑁 −
2)〉)), ((𝑤 substr
〈0, (𝑁 −
2)〉)‘0)} = {(𝑤‘((𝑁 − 2) − 1)), (𝑤‘0)}) |
126 | 125 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)} =
{(𝑤‘((𝑁 − 2) − 1)), (𝑤‘0)}) |
127 | | eluzelcn 11575 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℂ) |
128 | | cnm2m1cnm3 11162 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℂ → ((𝑁 − 2) − 1) = (𝑁 − 3)) |
129 | 128 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℂ → (𝑤‘((𝑁 − 2) − 1)) = (𝑤‘(𝑁 − 3))) |
130 | 127, 129 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑤‘((𝑁 − 2) − 1)) = (𝑤‘(𝑁 − 3))) |
131 | 130 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘((𝑁 − 2) − 1)) = (𝑤‘(𝑁 − 3))) |
132 | | eqcom 2617 |
. . . . . . . . . . . . . 14
⊢ ((𝑤‘(𝑁 − 2)) = (𝑤‘0) ↔ (𝑤‘0) = (𝑤‘(𝑁 − 2))) |
133 | 132 | biimpi 205 |
. . . . . . . . . . . . 13
⊢ ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → (𝑤‘0) = (𝑤‘(𝑁 − 2))) |
134 | | 3m1e2 11014 |
. . . . . . . . . . . . . . . . 17
⊢ (3
− 1) = 2 |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → (3 − 1) = 2) |
136 | 135 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (3 − 1)) = (𝑁 − 2)) |
137 | | 3cn 10972 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℂ |
138 | 137 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ∈ ℂ) |
139 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ ℂ) |
140 | 127, 138,
139 | subsubd 10299 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (3 − 1)) = ((𝑁 − 3) +
1)) |
141 | 136, 140 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) = ((𝑁 − 3) + 1)) |
142 | 141 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑤‘(𝑁 − 2)) = (𝑤‘((𝑁 − 3) + 1))) |
143 | 133, 142 | sylan9eqr 2666 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤‘0) = (𝑤‘((𝑁 − 3) + 1))) |
144 | 131, 143 | preq12d 4220 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {(𝑤‘((𝑁 − 2) − 1)), (𝑤‘0)} = {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))}) |
145 | 144 | adantll 746 |
. . . . . . . . . 10
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {(𝑤‘((𝑁 − 2) − 1)), (𝑤‘0)} = {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))}) |
146 | 126, 145 | eqtrd 2644 |
. . . . . . . . 9
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)} =
{(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))}) |
147 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘3)) |
148 | | eluzel2 11568 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ∈ ℤ) |
149 | 148, 36 | zaddcld 11362 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → (3 + (𝑁 − 1)) ∈
ℤ) |
150 | | 2pos 10989 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
2 |
151 | 16, 14 | ltaddposd 10490 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘3) → (0 < 2 ↔ 𝑁 < (𝑁 + 2))) |
152 | 150, 151 | mpbii 222 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 < (𝑁 + 2)) |
153 | 138, 127,
139 | addsub12d 10294 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘3) → (3 + (𝑁 − 1)) = (𝑁 + (3 − 1))) |
154 | 134 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 + (3 − 1)) = (𝑁 + 2) |
155 | 153, 154 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘3) → (3 + (𝑁 − 1)) = (𝑁 + 2)) |
156 | 152, 155 | breqtrrd 4611 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 < (3 + (𝑁 − 1))) |
157 | | elfzo2 12342 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (3..^(3 + (𝑁 − 1))) ↔ (𝑁 ∈
(ℤ≥‘3) ∧ (3 + (𝑁 − 1)) ∈ ℤ ∧ 𝑁 < (3 + (𝑁 − 1)))) |
158 | 147, 149,
156, 157 | syl3anbrc 1239 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ (3..^(3 + (𝑁 − 1)))) |
159 | 158, 36 | jca 553 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 ∈ (3..^(3 + (𝑁 − 1))) ∧ (𝑁 − 1) ∈
ℤ)) |
160 | | fzosubel3 12396 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ (3..^(3 + (𝑁 − 1))) ∧ (𝑁 − 1) ∈ ℤ)
→ (𝑁 − 3) ∈
(0..^(𝑁 −
1))) |
161 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑁 − 3) → (𝑤‘𝑖) = (𝑤‘(𝑁 − 3))) |
162 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = (𝑁 − 3) → (𝑖 + 1) = ((𝑁 − 3) + 1)) |
163 | 162 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑁 − 3) → (𝑤‘(𝑖 + 1)) = (𝑤‘((𝑁 − 3) + 1))) |
164 | 161, 163 | preq12d 4220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑁 − 3) → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))}) |
165 | 164 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑁 − 3) → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ (Edg‘𝐺))) |
166 | 165 | rspcv 3278 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 − 3) ∈ (0..^(𝑁 − 1)) →
(∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ (Edg‘𝐺))) |
167 | 159, 160,
166 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ (Edg‘𝐺))) |
168 | 167 | com12 32 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (𝑁 ∈ (ℤ≥‘3)
→ {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ (Edg‘𝐺))) |
169 | 168 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) → (𝑁 ∈ (ℤ≥‘3)
→ {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ (Edg‘𝐺))) |
170 | 169 | imp 444 |
. . . . . . . . . 10
⊢ ((((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ (Edg‘𝐺)) |
171 | 170 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ (Edg‘𝐺)) |
172 | 146, 171 | eqeltrd 2688 |
. . . . . . . 8
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺)) |
173 | 28, 113, 172 | 3jca 1235 |
. . . . . . 7
⊢
(((((𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝑤 substr 〈0, (𝑁 − 2)〉) ≠ ∅)
∧ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺))) |
174 | 173 | exp31 628 |
. . . . . 6
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) → (𝑁 ∈ (ℤ≥‘3)
→ ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝑤 substr 〈0, (𝑁 − 2)〉) ≠ ∅)
∧ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺))))) |
175 | 174 | adantld 482 |
. . . . 5
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝐺)) → ((𝐺 ∈ USGraph ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝑤 substr 〈0, (𝑁 − 2)〉) ≠ ∅)
∧ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺))))) |
176 | 3, 175 | syl 17 |
. . . 4
⊢ (𝑤 ∈ (𝑁 ClWWalkSN 𝐺) → ((𝐺 ∈ USGraph ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝑤 substr 〈0, (𝑁 − 2)〉) ≠ ∅)
∧ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺))))) |
177 | 176 | 3imp21 1269 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) ∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝑤 substr 〈0, (𝑁 − 2)〉) ≠ ∅)
∧ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺))) |
178 | 1 | clwwlknbp 41193 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝑁 ClWWalkSN 𝐺) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁)) |
179 | 50, 51, 53 | 3jca 1235 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2))) |
180 | 179 | ex 449 |
. . . . . . . . 9
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2)))) |
181 | 178, 180 | syl 17 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝑁 ClWWalkSN 𝐺) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑤 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2)))) |
182 | 181 | com12 32 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑤 ∈ (𝑁 ClWWalkSN 𝐺) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2)))) |
183 | 182 | adantl 481 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) → (𝑤 ∈ (𝑁 ClWWalkSN 𝐺) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2)))) |
184 | 183 | imp 444 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) ∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2))) |
185 | 184 | 3adant3 1074 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) ∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2))) |
186 | 185, 54 | syl 17 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) ∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) = (𝑁 − 2)) |
187 | 177, 186 | jca 553 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) ∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝑤 substr 〈0, (𝑁 − 2)〉) ≠ ∅)
∧ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺)) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 −
2))) |
188 | 11 | adantl 481 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) → (𝑁 − 2) ∈ ℕ) |
189 | | isclwwlksn 41190 |
. . . . 5
⊢ ((𝑁 − 2) ∈ ℕ
→ ((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
((𝑁 − 2) ClWWalkSN
𝐺) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈
(ClWWalkS‘𝐺) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 −
2)))) |
190 | 188, 189 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈
(ClWWalkS‘𝐺) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 −
2)))) |
191 | 1, 2 | isclwwlks 41188 |
. . . . . 6
⊢ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈
(ClWWalkS‘𝐺) ↔
(((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝑤 substr 〈0, (𝑁 − 2)〉) ≠ ∅)
∧ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺))) |
192 | 191 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈
(ClWWalkS‘𝐺) ↔
(((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝑤 substr 〈0, (𝑁 − 2)〉) ≠ ∅)
∧ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺)))) |
193 | 192 | anbi1d 737 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈
(ClWWalkS‘𝐺) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 − 2)) ↔
((((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
Word (Vtx‘𝐺) ∧
(𝑤 substr 〈0, (𝑁 − 2)〉) ≠ ∅)
∧ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺)) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 −
2)))) |
194 | 190, 193 | bitrd 267 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ↔ ((((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝑤 substr 〈0, (𝑁 − 2)〉) ≠ ∅)
∧ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺)) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 −
2)))) |
195 | 194 | 3ad2ant1 1075 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) ∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺) ↔ ((((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝑤 substr 〈0, (𝑁 − 2)〉) ≠ ∅)
∧ ∀𝑖 ∈
(0..^((#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) − 1)){((𝑤
substr 〈0, (𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ (Edg‘𝐺)) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 −
2)))) |
196 | 187, 195 | mpbird 246 |
1
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘3)) ∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑁 − 2) ClWWalkSN 𝐺)) |