Step | Hyp | Ref
| Expression |
1 | | usgrav 25867 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
2 | | uzuzle23 11605 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
3 | | eluzge2nn0 11603 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈
ℕ0) |
4 | 2, 3 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
ℕ0) |
5 | 1, 4 | anim12i 588 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑉 ∈ V ∧
𝐸 ∈ V) ∧ 𝑁 ∈
ℕ0)) |
6 | | df-3an 1033 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
↔ ((𝑉 ∈ V ∧
𝐸 ∈ V) ∧ 𝑁 ∈
ℕ0)) |
7 | 5, 6 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑉 ∈ V ∧
𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
8 | | isclwwlkn 26297 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁))) |
9 | 7, 8 | syl 17 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁))) |
10 | 9 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁))) |
11 | | isclwwlk 26296 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑤 ∈ (𝑉 ClWWalks 𝐸) ↔ (𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸))) |
12 | 11 | anbi1d 737 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁) ↔ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁))) |
13 | 1, 12 | syl 17 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → ((𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁) ↔ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁))) |
14 | 13 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁) ↔ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁))) |
15 | 10, 14 | bitrd 267 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁))) |
16 | | swrdcl 13271 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ Word 𝑉 → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉) |
17 | 16 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉) |
18 | 17 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉) |
19 | 18 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉) |
20 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑤) = 𝑁 → ((#‘𝑤) − 1) = (𝑁 − 1)) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((#‘𝑤) −
1) = (𝑁 −
1)) |
22 | | 1le3 11121 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ≤
3 |
23 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ ℝ) |
24 | | 3re 10971 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 ∈
ℝ |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ∈ ℝ) |
26 | | eluzelre 11574 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℝ) |
27 | 23, 25, 26 | lesub2d 10514 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘3) → (1 ≤ 3 ↔ (𝑁 − 3) ≤ (𝑁 − 1))) |
28 | 22, 27 | mpbii 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 3) ≤ (𝑁 − 1)) |
29 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
30 | | eluzel2 11568 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ∈ ℤ) |
31 | 29, 30 | zsubcld 11363 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 3) ∈ ℤ) |
32 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
33 | 29, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ∈ ℤ) |
34 | | eluz 11577 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 − 3) ∈ ℤ ∧
(𝑁 − 1) ∈
ℤ) → ((𝑁 −
1) ∈ (ℤ≥‘(𝑁 − 3)) ↔ (𝑁 − 3) ≤ (𝑁 − 1))) |
35 | 31, 33, 34 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 3)) ↔ (𝑁 − 3) ≤ (𝑁 − 1))) |
36 | 28, 35 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 3))) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 3))) |
38 | 21, 37 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((#‘𝑤) −
1) ∈ (ℤ≥‘(𝑁 − 3))) |
39 | | fzoss2 12365 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑤)
− 1) ∈ (ℤ≥‘(𝑁 − 3)) → (0..^(𝑁 − 3)) ⊆ (0..^((#‘𝑤) − 1))) |
40 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . 18
⊢
((0..^(𝑁 − 3))
⊆ (0..^((#‘𝑤)
− 1)) → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 3)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 3)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) |
42 | 41 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 3)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) |
43 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈ (0..^(𝑁 − 3))) → 𝑤 ∈ Word 𝑉) |
44 | | 1eluzge0 11608 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
(ℤ≥‘0) |
45 | | fzss1 12251 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 ∈
(ℤ≥‘0) → (1...𝑁) ⊆ (0...𝑁)) |
46 | 44, 45 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘3) → (1...𝑁) ⊆ (0...𝑁)) |
47 | | ige3m2fz 12236 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ (1...𝑁)) |
48 | 46, 47 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ (0...𝑁)) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
(0...𝑁)) |
50 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑤) = 𝑁 → (0...(#‘𝑤)) = (0...𝑁)) |
51 | 50 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑤) = 𝑁 → ((𝑁 − 2) ∈ (0...(#‘𝑤)) ↔ (𝑁 − 2) ∈ (0...𝑁))) |
52 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑁 − 2)
∈ (0...(#‘𝑤))
↔ (𝑁 − 2) ∈
(0...𝑁))) |
53 | 49, 52 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
(0...(#‘𝑤))) |
54 | 53 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑁 − 2) ∈
(0...(#‘𝑤))) |
55 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 2 ∈
ℝ |
56 | | 2lt3 11072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 2 <
3 |
57 | 55, 24, 56 | ltleii 10039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ≤
3 |
58 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℝ) |
59 | 58, 25, 26 | lesub2d 10514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → (2 ≤ 3 ↔ (𝑁 − 3) ≤ (𝑁 − 2))) |
60 | 57, 59 | mpbii 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 3) ≤ (𝑁 − 2)) |
61 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 2 ∈
ℤ |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℤ) |
63 | 29, 62 | zsubcld 11363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℤ) |
64 | | eluz 11577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑁 − 3) ∈ ℤ ∧
(𝑁 − 2) ∈
ℤ) → ((𝑁 −
2) ∈ (ℤ≥‘(𝑁 − 3)) ↔ (𝑁 − 3) ≤ (𝑁 − 2))) |
65 | 31, 63, 64 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) ∈
(ℤ≥‘(𝑁 − 3)) ↔ (𝑁 − 3) ≤ (𝑁 − 2))) |
66 | 60, 65 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈
(ℤ≥‘(𝑁 − 3))) |
67 | | fzoss2 12365 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 − 2) ∈
(ℤ≥‘(𝑁 − 3)) → (0..^(𝑁 − 3)) ⊆ (0..^(𝑁 − 2))) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘3) → (0..^(𝑁 − 3)) ⊆ (0..^(𝑁 − 2))) |
69 | 68 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑖 ∈ (0..^(𝑁 − 3)) → 𝑖 ∈ (0..^(𝑁 − 2)))) |
70 | 69 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑖 ∈
(0..^(𝑁 − 3)) →
𝑖 ∈ (0..^(𝑁 − 2)))) |
71 | 70 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈ (0..^(𝑁 − 3))) → 𝑖 ∈ (0..^(𝑁 − 2))) |
72 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (0...(#‘𝑤)) ∧ 𝑖 ∈ (0..^(𝑁 − 2))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖) = (𝑤‘𝑖)) |
73 | 43, 54, 71, 72 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈ (0..^(𝑁 − 3))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖) = (𝑤‘𝑖)) |
74 | 73 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑤‘𝑖) = ((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖)) |
75 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^(𝑁 − 3)) → 𝑖 ∈ ℕ0) |
76 | 75 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → 𝑖 ∈ ℕ0) |
77 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℕ0) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑖 + 1) ∈
ℕ0) |
79 | | uz3m2nn 11607 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
80 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑁 − 2) ∈ ℕ) |
81 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^(𝑁 − 3)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 − 3) ∈ ℕ ∧
𝑖 < (𝑁 − 3))) |
82 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℂ) |
83 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ 1 ∈
ℂ |
84 | 82, 83 | jctir 559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑖 ∈ ℕ0
→ (𝑖 ∈ ℂ
∧ 1 ∈ ℂ)) |
85 | 84 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘3)) → (𝑖 ∈ ℂ ∧ 1 ∈
ℂ)) |
86 | | pncan 10166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑖 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑖 + 1)
− 1) = 𝑖) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘3)) → ((𝑖 + 1) − 1) = 𝑖) |
88 | 87 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘3)) → 𝑖 = ((𝑖 + 1) − 1)) |
89 | | eluzelcn 11575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℂ) |
90 | 89 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘3)) → 𝑁 ∈ ℂ) |
91 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘3)) → 2 ∈ ℂ) |
92 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘3)) → 1 ∈ ℂ) |
93 | 90, 91, 92 | subsub4d 10302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘3)) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1))) |
94 | | df-3 10957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ 3 = (2 +
1) |
95 | 94 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 − 3) = (𝑁 − (2 + 1)) |
96 | 93, 95 | syl6reqr 2663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘3)) → (𝑁 − 3) = ((𝑁 − 2) − 1)) |
97 | 88, 96 | breq12d 4596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘3)) → (𝑖 < (𝑁 − 3) ↔ ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1))) |
98 | 97 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘3)) → (𝑖 < (𝑁 − 3) → ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1))) |
99 | 98 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑖 ∈ ℕ0
∧ 𝑖 < (𝑁 − 3)) → (𝑁 ∈
(ℤ≥‘3) → ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1))) |
100 | 99 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑖 ∈ ℕ0
∧ (𝑁 − 3) ∈
ℕ ∧ 𝑖 < (𝑁 − 3)) → (𝑁 ∈
(ℤ≥‘3) → ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1))) |
101 | 100 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑖 ∈ ℕ0
∧ (𝑁 − 3) ∈
ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈
(ℤ≥‘3)) → ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1)) |
102 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
103 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑖 ∈ ℝ → (𝑖 + 1) ∈
ℝ) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℝ) |
105 | 104 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑖 ∈ ℕ0
∧ (𝑁 − 3) ∈
ℕ ∧ 𝑖 < (𝑁 − 3)) → (𝑖 + 1) ∈
ℝ) |
106 | 105 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑖 ∈ ℕ0
∧ (𝑁 − 3) ∈
ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈
(ℤ≥‘3)) → (𝑖 + 1) ∈ ℝ) |
107 | 26, 58 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℝ) |
108 | 107 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑖 ∈ ℕ0
∧ (𝑁 − 3) ∈
ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈
(ℤ≥‘3)) → (𝑁 − 2) ∈ ℝ) |
109 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑖 ∈ ℕ0
∧ (𝑁 − 3) ∈
ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈
(ℤ≥‘3)) → 1 ∈ ℝ) |
110 | 106, 108,
109 | ltsub1d 10515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑖 ∈ ℕ0
∧ (𝑁 − 3) ∈
ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈
(ℤ≥‘3)) → ((𝑖 + 1) < (𝑁 − 2) ↔ ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1))) |
111 | 101, 110 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑖 ∈ ℕ0
∧ (𝑁 − 3) ∈
ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈
(ℤ≥‘3)) → (𝑖 + 1) < (𝑁 − 2)) |
112 | 111 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑖 ∈ ℕ0
∧ (𝑁 − 3) ∈
ℕ ∧ 𝑖 < (𝑁 − 3)) → (𝑁 ∈
(ℤ≥‘3) → (𝑖 + 1) < (𝑁 − 2))) |
113 | 81, 112 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^(𝑁 − 3)) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑖 + 1) < (𝑁 − 2))) |
114 | 113 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑖 + 1) < (𝑁 − 2)) |
115 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑖 + 1) ∈ (0..^(𝑁 − 2)) ↔ ((𝑖 + 1) ∈ ℕ0
∧ (𝑁 − 2) ∈
ℕ ∧ (𝑖 + 1) <
(𝑁 −
2))) |
116 | 78, 80, 114, 115 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑖 + 1) ∈ (0..^(𝑁 − 2))) |
117 | 116 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑖 ∈ (0..^(𝑁 − 3)) → (𝑖 + 1) ∈ (0..^(𝑁 − 2)))) |
118 | 117 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑖 ∈
(0..^(𝑁 − 3)) →
(𝑖 + 1) ∈ (0..^(𝑁 − 2)))) |
119 | 118 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑖 + 1) ∈ (0..^(𝑁 − 2))) |
120 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (0...(#‘𝑤)) ∧ (𝑖 + 1) ∈ (0..^(𝑁 − 2))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1)) = (𝑤‘(𝑖 + 1))) |
121 | 43, 54, 119, 120 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈ (0..^(𝑁 − 3))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1)) = (𝑤‘(𝑖 + 1))) |
122 | 121 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑤‘(𝑖 + 1)) = ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))) |
123 | 74, 122 | preq12d 4220 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈ (0..^(𝑁 − 3))) → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))}) |
124 | 123 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑖 ∈ (0..^(𝑁 − 3))) → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
125 | 124 | ralbidva 2968 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (∀𝑖 ∈
(0..^(𝑁 − 3)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
126 | 42, 125 | sylibd 228 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
127 | 126 | impancom 455 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) → (((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∀𝑖 ∈
(0..^(𝑁 − 3)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
128 | 127 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) → (((#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∀𝑖 ∈
(0..^(𝑁 − 3)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
129 | 128 | expdimp 452 |
. . . . . . . . . . . 12
⊢ (((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ ∀𝑖 ∈
(0..^(𝑁 − 3)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
130 | 129 | impcom 445 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
131 | 130 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
132 | | simprl1 1099 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → 𝑤 ∈ Word 𝑉) |
133 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → (#‘𝑤) = 𝑁) |
134 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → 𝑁 ∈
(ℤ≥‘2)) |
135 | 132, 133,
134 | 3jca 1235 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2))) |
136 | 135 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2))) |
137 | | extwwlkfablem2lem 26602 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑤 substr
〈0, (𝑁 −
2)〉)) = (𝑁 −
2)) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) = (𝑁 − 2)) |
139 | 138 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) − 1) =
((𝑁 − 2) −
1)) |
140 | 139 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) − 1))
= (0..^((𝑁 − 2)
− 1))) |
141 | | 2cnd 10970 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℂ) |
142 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ ℂ) |
143 | 89, 141, 142 | subsub4d 10302 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1))) |
144 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . 17
⊢ (2 + 1) =
3 |
145 | 144 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → (2 + 1) = 3) |
146 | 145 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (2 + 1)) = (𝑁 − 3)) |
147 | 143, 146 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) − 1) = (𝑁 − 3)) |
148 | 147 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑁 − 2) − 1) = (𝑁 − 3)) |
149 | 148 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (0..^((𝑁 − 2) − 1)) = (0..^(𝑁 − 3))) |
150 | 140, 149 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) − 1))
= (0..^(𝑁 −
3))) |
151 | 150 | raleqdv 3121 |
. . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
152 | 131, 151 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) − 1)){((𝑤 substr 〈0, (𝑁 − 2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
153 | 20 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑤) = 𝑁 → (0..^((#‘𝑤) − 1)) = (0..^(𝑁 − 1))) |
154 | 153 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑤) = 𝑁 → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) |
155 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → 𝑤 ∈ Word 𝑉) |
156 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝑤) = 𝑁 → (1...(#‘𝑤)) = (1...𝑁)) |
157 | 156 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝑤) = 𝑁 → ((𝑁 − 2) ∈ (1...(#‘𝑤)) ↔ (𝑁 − 2) ∈ (1...𝑁))) |
158 | 47, 157 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑤) = 𝑁 → (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2) ∈
(1...(#‘𝑤)))) |
159 | 158 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2) ∈
(1...(#‘𝑤)))) |
160 | 159 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘3) → ((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 − 2) ∈ (1...(#‘𝑤)))) |
161 | 160 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 − 2) ∈ (1...(#‘𝑤)))) |
162 | 161 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑁 − 2) ∈
(1...(#‘𝑤))) |
163 | | swrd0fvlsw 13295 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))) → ( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)) = (𝑤‘((𝑁 − 2) − 1))) |
164 | 155, 162,
163 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑤‘((𝑁 − 2) −
1))) |
165 | 47 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
(1...𝑁)) |
166 | 156 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (1...(#‘𝑤)) =
(1...𝑁)) |
167 | 165, 166 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝑤) =
𝑁 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
(1...(#‘𝑤))) |
168 | 167 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑤) = 𝑁 → (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2) ∈
(1...(#‘𝑤)))) |
169 | 168 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑁 − 2) ∈
(1...(#‘𝑤)))) |
170 | 169 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘3) → ((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 − 2) ∈ (1...(#‘𝑤)))) |
171 | 170 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 − 2) ∈ (1...(#‘𝑤)))) |
172 | 171 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑁 − 2) ∈
(1...(#‘𝑤))) |
173 | | swrd0fv0 13292 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) = (𝑤‘0)) |
174 | 155, 172,
173 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0) =
(𝑤‘0)) |
175 | 164, 174 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)} =
{(𝑤‘((𝑁 − 2) − 1)), (𝑤‘0)}) |
176 | | cnm2m1cnm3 11162 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℂ → ((𝑁 − 2) − 1) = (𝑁 − 3)) |
177 | 89, 176 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) − 1) = (𝑁 − 3)) |
178 | 177 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑤‘((𝑁 − 2) − 1)) = (𝑤‘(𝑁 − 3))) |
179 | 178 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘((𝑁 − 2) − 1)) = (𝑤‘(𝑁 − 3))) |
180 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑤‘0) = (𝑤‘(𝑁 − 2)) → (𝑤‘0) = (𝑤‘(𝑁 − 2))) |
181 | 180 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → (𝑤‘0) = (𝑤‘(𝑁 − 2))) |
182 | 181 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘0) = (𝑤‘(𝑁 − 2))) |
183 | 179, 182 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {(𝑤‘((𝑁 − 2) − 1)), (𝑤‘0)} = {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))}) |
184 | | eluzfz2b 12221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈
(ℤ≥‘3) ↔ 𝑁 ∈ (3...𝑁)) |
185 | | fzval3 12404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 ∈ ℤ →
(3...𝑁) = (3..^(𝑁 + 1))) |
186 | 29, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈
(ℤ≥‘3) → (3...𝑁) = (3..^(𝑁 + 1))) |
187 | 186 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 ∈ (3...𝑁) ↔ 𝑁 ∈ (3..^(𝑁 + 1)))) |
188 | | peano2z 11295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈
ℤ) |
189 | | zadd2cl 11366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑁 ∈ ℤ → (𝑁 + 2) ∈
ℤ) |
190 | | 1le2 11118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ 1 ≤
2 |
191 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑁 ∈ ℤ → 1 ∈
ℝ) |
192 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑁 ∈ ℤ → 2 ∈
ℝ) |
193 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
194 | 191, 192,
193 | leadd2d 10501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑁 ∈ ℤ → (1 ≤ 2
↔ (𝑁 + 1) ≤ (𝑁 + 2))) |
195 | 190, 194 | mpbii 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ≤ (𝑁 + 2)) |
196 | 188, 189,
195 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℤ → ((𝑁 + 1) ∈ ℤ ∧
(𝑁 + 2) ∈ ℤ
∧ (𝑁 + 1) ≤ (𝑁 + 2))) |
197 | 29, 196 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 + 1) ∈ ℤ ∧ (𝑁 + 2) ∈ ℤ ∧
(𝑁 + 1) ≤ (𝑁 + 2))) |
198 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑁 + 2) ∈
(ℤ≥‘(𝑁 + 1)) ↔ ((𝑁 + 1) ∈ ℤ ∧ (𝑁 + 2) ∈ ℤ ∧
(𝑁 + 1) ≤ (𝑁 + 2))) |
199 | 197, 198 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 + 2) ∈
(ℤ≥‘(𝑁 + 1))) |
200 | | fzoss2 12365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑁 + 2) ∈
(ℤ≥‘(𝑁 + 1)) → (3..^(𝑁 + 1)) ⊆ (3..^(𝑁 + 2))) |
201 | 199, 200 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈
(ℤ≥‘3) → (3..^(𝑁 + 1)) ⊆ (3..^(𝑁 + 2))) |
202 | 201 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 ∈ (3..^(𝑁 + 1)) → 𝑁 ∈ (3..^(𝑁 + 2)))) |
203 | 187, 202 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 ∈ (3...𝑁) → 𝑁 ∈ (3..^(𝑁 + 2)))) |
204 | 184, 203 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 ∈ (ℤ≥‘3)
→ 𝑁 ∈ (3..^(𝑁 + 2)))) |
205 | 204 | pm2.43i 50 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ (3..^(𝑁 + 2))) |
206 | | 3cn 10972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 3 ∈
ℂ |
207 | 206 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ∈ ℂ) |
208 | 207, 89, 142 | addsub12d 10294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈
(ℤ≥‘3) → (3 + (𝑁 − 1)) = (𝑁 + (3 − 1))) |
209 | | 3m1e2 11014 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (3
− 1) = 2 |
210 | 209 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 + (3 − 1)) = (𝑁 + 2) |
211 | 208, 210 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈
(ℤ≥‘3) → (3 + (𝑁 − 1)) = (𝑁 + 2)) |
212 | 211 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈
(ℤ≥‘3) → (3..^(3 + (𝑁 − 1))) = (3..^(𝑁 + 2))) |
213 | 205, 212 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ (3..^(3 + (𝑁 − 1)))) |
214 | 213, 33 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 ∈ (3..^(3 + (𝑁 − 1))) ∧ (𝑁 − 1) ∈
ℤ)) |
215 | | fzosubel3 12396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ (3..^(3 + (𝑁 − 1))) ∧ (𝑁 − 1) ∈ ℤ)
→ (𝑁 − 3) ∈
(0..^(𝑁 −
1))) |
216 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 = (𝑁 − 3) → (𝑤‘𝑖) = (𝑤‘(𝑁 − 3))) |
217 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑖 = (𝑁 − 3) → (𝑖 + 1) = ((𝑁 − 3) + 1)) |
218 | 217 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 = (𝑁 − 3) → (𝑤‘(𝑖 + 1)) = (𝑤‘((𝑁 − 3) + 1))) |
219 | 216, 218 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 = (𝑁 − 3) → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))}) |
220 | 219 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 = (𝑁 − 3) → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ ran 𝐸)) |
221 | 220 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 − 3) ∈ (0..^(𝑁 − 1)) →
(∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ ran 𝐸)) |
222 | 214, 215,
221 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ ran 𝐸)) |
223 | 89, 207, 142 | subsubd 10299 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (3 − 1)) = ((𝑁 − 3) +
1)) |
224 | 209 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈
(ℤ≥‘3) → (3 − 1) = 2) |
225 | 224 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (3 − 1)) = (𝑁 − 2)) |
226 | 223, 225 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 3) + 1) = (𝑁 − 2)) |
227 | 226 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑤‘((𝑁 − 3) + 1)) = (𝑤‘(𝑁 − 2))) |
228 | 227 | preq2d 4219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈
(ℤ≥‘3) → {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} = {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))}) |
229 | 228 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘3) → ({(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ ran 𝐸 ↔ {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸)) |
230 | 222, 229 | sylibd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘3) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸)) |
231 | 230 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸)) |
232 | 231 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸)) |
233 | 232 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸)) |
234 | 233 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸) |
235 | 183, 234 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {(𝑤‘((𝑁 − 2) − 1)), (𝑤‘0)} ∈ ran 𝐸) |
236 | 175, 235 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((#‘𝑤) =
𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸) |
237 | 236 | exp41 636 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑤) = 𝑁 → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑤 ∈ Word 𝑉 → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)))) |
238 | 154, 237 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑤) = 𝑁 → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑤 ∈ Word 𝑉 → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)))) |
239 | 238 | com13 86 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ Word 𝑉 → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ((#‘𝑤) = 𝑁 → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)))) |
240 | 239 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) → ((#‘𝑤) = 𝑁 → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸))) |
241 | 240 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) → ((#‘𝑤) = 𝑁 → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸))) |
242 | 241 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)) |
243 | 242 | expd 451 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → {( lastS
‘(𝑤 substr 〈0,
(𝑁 − 2)〉)),
((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸))) |
244 | 243 | impcom 445 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)) |
245 | 244 | com12 32 |
. . . . . . . . . . 11
⊢ ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → ((𝑁 ∈ (ℤ≥‘3)
∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)) |
246 | 245 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((𝑁 ∈ (ℤ≥‘3)
∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)) |
247 | 246 | impcom 445 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸) |
248 | 19, 152, 247 | 3jca 1235 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)) |
249 | 248 | exp31 628 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)))) |
250 | 249 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑤 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)))) |
251 | 15, 250 | sylbid 229 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)))) |
252 | 251 | imp31 447 |
. . . 4
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸)) |
253 | | clwwlknprop 26300 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) |
254 | | simpl2 1058 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑤 ∈ Word 𝑉) |
255 | | simpl3r 1110 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (#‘𝑤) = 𝑁) |
256 | 2 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑁 ∈
(ℤ≥‘2)) |
257 | 254, 255,
256 | 3jca 1235 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁)) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2))) |
258 | 257 | ex 449 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁)) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2)))) |
259 | 253, 258 | syl 17 |
. . . . . . . . 9
⊢ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑁 ∈ (ℤ≥‘3)
→ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2)))) |
260 | 259 | com12 32 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2)))) |
261 | 260 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2)))) |
262 | 261 | imp 444 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2))) |
263 | 262 | adantr 480 |
. . . . 5
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁 ∧ 𝑁 ∈
(ℤ≥‘2))) |
264 | 263, 137 | syl 17 |
. . . 4
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) = (𝑁 − 2)) |
265 | 252, 264 | jca 553 |
. . 3
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 −
2))) |
266 | | uznn0sub 11595 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) |
267 | 2, 266 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈
ℕ0) |
268 | 1, 267 | anim12i 588 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑉 ∈ V ∧
𝐸 ∈ V) ∧ (𝑁 − 2) ∈
ℕ0)) |
269 | | df-3an 1033 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 − 2) ∈
ℕ0) ↔ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 − 2) ∈
ℕ0)) |
270 | 268, 269 | sylibr 223 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑉 ∈ V ∧
𝐸 ∈ V ∧ (𝑁 − 2) ∈
ℕ0)) |
271 | | isclwwlkn 26297 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 − 2) ∈
ℕ0) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) = (𝑁 − 2)))) |
272 | 270, 271 | syl 17 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) = (𝑁 − 2)))) |
273 | | isclwwlk 26296 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸))) |
274 | 1, 273 | syl 17 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸))) |
275 | 274 | adantr 480 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
(𝑉 ClWWalks 𝐸) ↔ ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸))) |
276 | 275 | anbi1d 737 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
(𝑉 ClWWalks 𝐸) ∧ (#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) = (𝑁 − 2)) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 −
2)))) |
277 | 272, 276 | bitrd 267 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 −
2)))) |
278 | 277 | 3adant2 1073 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑤 substr 〈0,
(𝑁 − 2)〉) ∈
((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 −
2)))) |
279 | 278 | ad2antrr 758 |
. . 3
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)) ↔ (((𝑤 substr 〈0, (𝑁 − 2)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr 〈0, (𝑁 − 2)〉)) −
1)){((𝑤 substr 〈0,
(𝑁 −
2)〉)‘𝑖), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr 〈0, (𝑁 − 2)〉)), ((𝑤 substr 〈0, (𝑁 − 2)〉)‘0)}
∈ ran 𝐸) ∧
(#‘(𝑤 substr 〈0,
(𝑁 − 2)〉)) =
(𝑁 −
2)))) |
280 | 265, 279 | mpbird 246 |
. 2
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2))) |
281 | 267 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
ℕ0) |
282 | 281 | ad2antrr 758 |
. . 3
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑁 − 2) ∈
ℕ0) |
283 | | numclwwlk.c |
. . . 4
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
284 | 283 | numclwwlkfvc 26604 |
. . 3
⊢ ((𝑁 − 2) ∈
ℕ0 → (𝐶‘(𝑁 − 2)) = ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2))) |
285 | 282, 284 | syl 17 |
. 2
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝐶‘(𝑁 − 2)) = ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2))) |
286 | 280, 285 | eleqtrrd 2691 |
1
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 substr 〈0, (𝑁 − 2)〉) ∈ (𝐶‘(𝑁 − 2))) |