| Step | Hyp | Ref
| Expression |
| 1 | | clwwlknnn 30052 |
. . 3
⊢ ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑁 ClWWalksN 𝐺) → 𝑁 ∈ ℕ) |
| 2 | | clwwlkext2edg.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
| 3 | | clwwlkext2edg.e |
. . . . 5
⊢ 𝐸 = (Edg‘𝐺) |
| 4 | 2, 3 | isclwwlknx 30055 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑁 ClWWalksN 𝐺) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁))) |
| 5 | | ige2m2fzo 13767 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈ (0..^(𝑁 − 1))) |
| 6 | 5 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 − 2) ∈
(0..^(𝑁 −
1))) |
| 7 | 6 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (𝑁 − 2) ∈ (0..^(𝑁 − 1))) |
| 8 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘(𝑊
++ 〈“𝑍”〉)) = 𝑁 → ((♯‘(𝑊 ++ 〈“𝑍”〉)) − 1) = (𝑁 − 1)) |
| 9 | 8 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢
((♯‘(𝑊
++ 〈“𝑍”〉)) = 𝑁 → (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) − 1)) =
(0..^(𝑁 −
1))) |
| 10 | 9 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢
((♯‘(𝑊
++ 〈“𝑍”〉)) = 𝑁 → ((𝑁 − 2) ∈
(0..^((♯‘(𝑊 ++
〈“𝑍”〉)) − 1)) ↔ (𝑁 − 2) ∈ (0..^(𝑁 − 1)))) |
| 11 | 10 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑁 − 2) ∈
(0..^((♯‘(𝑊 ++
〈“𝑍”〉)) − 1)) ↔ (𝑁 − 2) ∈ (0..^(𝑁 − 1)))) |
| 12 | 7, 11 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (𝑁 − 2) ∈
(0..^((♯‘(𝑊 ++
〈“𝑍”〉)) −
1))) |
| 13 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑁 − 2) → ((𝑊 ++ 〈“𝑍”〉)‘𝑖) = ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2))) |
| 14 | | fvoveq1 7454 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑁 − 2) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))) |
| 15 | 13, 14 | preq12d 4741 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑁 − 2) → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))}) |
| 16 | 15 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑁 − 2) → ({((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))} ∈ 𝐸)) |
| 17 | 16 | rspcv 3618 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 2) ∈
(0..^((♯‘(𝑊 ++
〈“𝑍”〉)) − 1)) →
(∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 → {((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))} ∈ 𝐸)) |
| 18 | 12, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 → {((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))} ∈ 𝐸)) |
| 19 | | wrdlenccats1lenm1 14660 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑊 ∈ Word 𝑉 → ((♯‘(𝑊 ++ 〈“𝑍”〉)) − 1) =
(♯‘𝑊)) |
| 20 | 19 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) = ((♯‘(𝑊 ++ 〈“𝑍”〉)) − 1)) |
| 21 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (♯‘𝑊) = ((♯‘(𝑊 ++ 〈“𝑍”〉)) − 1)) |
| 22 | 21, 8 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) ∧ (♯‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁) → (♯‘𝑊) = (𝑁 − 1)) |
| 23 | 22 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((♯‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁 → (♯‘𝑊) = (𝑁 − 1))) |
| 24 | 23 | 3adant3 1133 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘(𝑊
++ 〈“𝑍”〉)) = 𝑁 → (♯‘𝑊) = (𝑁 − 1))) |
| 25 | | eluzelcn 12890 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℂ) |
| 26 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℂ) |
| 27 | 25, 26, 26 | subsub4d 11651 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 1) − 1) = (𝑁 − (1 + 1))) |
| 28 | | 1p1e2 12391 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 + 1) =
2 |
| 29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 + 1) = 2) |
| 30 | 29 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − (1 + 1)) = (𝑁 − 2)) |
| 31 | 27, 30 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) = ((𝑁 − 1) − 1)) |
| 32 | 31 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 − 2) =
((𝑁 − 1) −
1)) |
| 33 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑊) =
(𝑁 − 1) →
((♯‘𝑊) −
1) = ((𝑁 − 1) −
1)) |
| 34 | 33 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑊) =
(𝑁 − 1) →
((𝑁 − 1) − 1) =
((♯‘𝑊) −
1)) |
| 35 | 32, 34 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) →
(𝑁 − 2) =
((♯‘𝑊) −
1)) |
| 36 | 35 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘𝑊) =
(𝑁 − 1) → (𝑁 − 2) =
((♯‘𝑊) −
1))) |
| 37 | 24, 36 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘(𝑊
++ 〈“𝑍”〉)) = 𝑁 → (𝑁 − 2) = ((♯‘𝑊) − 1))) |
| 38 | 37 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (𝑁 − 2) = ((♯‘𝑊) − 1)) |
| 39 | 38 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)) = ((𝑊 ++ 〈“𝑍”〉)‘((♯‘𝑊) − 1))) |
| 40 | | simpl1 1192 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) → 𝑊 ∈ Word 𝑉) |
| 41 | | s1cl 14640 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑍 ∈ 𝑉 → 〈“𝑍”〉 ∈ Word 𝑉) |
| 42 | 41 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ 〈“𝑍”〉 ∈ Word 𝑉) |
| 43 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) →
〈“𝑍”〉
∈ Word 𝑉) |
| 44 | | eluz2 12884 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤
𝑁)) |
| 45 | | zre 12617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
| 46 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 1 ∈
ℝ) |
| 47 | | 2re 12340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 2 ∈
ℝ |
| 48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 2 ∈
ℝ) |
| 49 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 𝑁 ∈ ℝ) |
| 50 | | 1lt2 12437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 1 <
2 |
| 51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 1 <
2) |
| 52 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 2 ≤ 𝑁) |
| 53 | 46, 48, 49, 51, 52 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 1 < 𝑁) |
| 54 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈ ℝ → 1 ∈
ℝ) |
| 55 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℝ) |
| 56 | 54, 55 | posdifd 11850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℝ → (1 <
𝑁 ↔ 0 < (𝑁 − 1))) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → (1 < 𝑁 ↔ 0 < (𝑁 − 1))) |
| 58 | 53, 57 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 0 < (𝑁 − 1)) |
| 59 | 58 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℝ → (2 ≤
𝑁 → 0 < (𝑁 − 1))) |
| 60 | 45, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℤ → (2 ≤
𝑁 → 0 < (𝑁 − 1))) |
| 61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 ∈
ℤ → (𝑁 ∈
ℤ → (2 ≤ 𝑁
→ 0 < (𝑁 −
1)))) |
| 62 | 61 | 3imp 1111 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 2 ≤ 𝑁) → 0 < (𝑁 − 1)) |
| 63 | 44, 62 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘2) → 0 < (𝑁 − 1)) |
| 64 | 63 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) → 0
< (𝑁 −
1)) |
| 65 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝑊) =
(𝑁 − 1) → (0
< (♯‘𝑊)
↔ 0 < (𝑁 −
1))) |
| 66 | 65 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) → (0
< (♯‘𝑊)
↔ 0 < (𝑁 −
1))) |
| 67 | 64, 66 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) → 0
< (♯‘𝑊)) |
| 68 | | hashneq0 14403 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑊 ∈ Word 𝑉 → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅)) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅)) |
| 70 | 69 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) → (0
< (♯‘𝑊)
↔ 𝑊 ≠
∅)) |
| 71 | 67, 70 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) → 𝑊 ≠ ∅) |
| 72 | 71 | 3adantl2 1168 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) → 𝑊 ≠ ∅) |
| 73 | 40, 43, 72 | 3jca 1129 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) →
(𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)) |
| 74 | 73 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘𝑊) =
(𝑁 − 1) → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅))) |
| 75 | 24, 74 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘(𝑊
++ 〈“𝑍”〉)) = 𝑁 → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅))) |
| 76 | 75 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)) |
| 77 | | ccatval1lsw 14622 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“𝑍”〉)‘((♯‘𝑊) − 1)) =
(lastS‘𝑊)) |
| 78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘((♯‘𝑊) − 1)) =
(lastS‘𝑊)) |
| 79 | 39, 78 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)) = (lastS‘𝑊)) |
| 80 | | 2m1e1 12392 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2
− 1) = 1 |
| 81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 − 1) = 1) |
| 82 | 81 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 = (2 − 1)) |
| 83 | 82 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) = (𝑁 − (2 − 1))) |
| 84 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ ℂ) |
| 85 | 25, 84, 26 | subsubd 11648 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − (2 − 1)) = ((𝑁 − 2) +
1)) |
| 86 | 83, 85 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 2) + 1) = (𝑁 − 1)) |
| 87 | 86 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((𝑁 − 2) + 1)
= (𝑁 −
1)) |
| 88 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑊) =
(𝑁 − 1) →
(((𝑁 − 2) + 1) =
(♯‘𝑊) ↔
((𝑁 − 2) + 1) =
(𝑁 −
1))) |
| 89 | 87, 88 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘𝑊) =
(𝑁 − 1) →
((𝑁 − 2) + 1) =
(♯‘𝑊))) |
| 90 | 24, 89 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘(𝑊
++ 〈“𝑍”〉)) = 𝑁 → ((𝑁 − 2) + 1) = (♯‘𝑊))) |
| 91 | 90 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑁 − 2) + 1) = (♯‘𝑊)) |
| 92 | 91 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(♯‘𝑊))) |
| 93 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉)) |
| 94 | 93 | 3adant3 1133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉)) |
| 95 | 94 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉)) |
| 96 | | ccatws1ls 14671 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ 〈“𝑍”〉)‘(♯‘𝑊)) = 𝑍) |
| 97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘(♯‘𝑊)) = 𝑍) |
| 98 | 92, 97 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1)) = 𝑍) |
| 99 | 79, 98 | preq12d 4741 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → {((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))} = {(lastS‘𝑊), 𝑍}) |
| 100 | 99 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ({((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))} ∈ 𝐸 ↔ {(lastS‘𝑊), 𝑍} ∈ 𝐸)) |
| 101 | 18, 100 | sylibd 239 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 → {(lastS‘𝑊), 𝑍} ∈ 𝐸)) |
| 102 | 101 | ex 412 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘(𝑊
++ 〈“𝑍”〉)) = 𝑁 → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 → {(lastS‘𝑊), 𝑍} ∈ 𝐸))) |
| 103 | 102 | com13 88 |
. . . . . . . 8
⊢
(∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 → ((♯‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁 → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ {(lastS‘𝑊),
𝑍} ∈ 𝐸))) |
| 104 | 103 | 3ad2ant2 1135 |
. . . . . . 7
⊢ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) → ((♯‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁 → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ {(lastS‘𝑊),
𝑍} ∈ 𝐸))) |
| 105 | 104 | imp31 417 |
. . . . . 6
⊢
(((((𝑊 ++
〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {(lastS‘𝑊),
𝑍} ∈ 𝐸) |
| 106 | 94 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) →
(𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉)) |
| 107 | | lswccats1 14672 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (lastS‘(𝑊 ++ 〈“𝑍”〉)) = 𝑍) |
| 108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) →
(lastS‘(𝑊 ++
〈“𝑍”〉)) = 𝑍) |
| 109 | 63 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ 0 < (𝑁 −
1)) |
| 110 | 109 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) → 0
< (𝑁 −
1)) |
| 111 | 65 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) → (0
< (♯‘𝑊)
↔ 0 < (𝑁 −
1))) |
| 112 | 110, 111 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) → 0
< (♯‘𝑊)) |
| 113 | | ccatfv0 14621 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) → ((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) |
| 114 | 40, 43, 112, 113 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) →
((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) |
| 115 | 108, 114 | preq12d 4741 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (♯‘𝑊) =
(𝑁 − 1)) →
{(lastS‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} = {𝑍, (𝑊‘0)}) |
| 116 | 115 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘𝑊) =
(𝑁 − 1) →
{(lastS‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} = {𝑍, (𝑊‘0)})) |
| 117 | 24, 116 | syld 47 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘(𝑊
++ 〈“𝑍”〉)) = 𝑁 → {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} = {𝑍, (𝑊‘0)})) |
| 118 | 117 | impcom 407 |
. . . . . . . . . 10
⊢
(((♯‘(𝑊
++ 〈“𝑍”〉)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {(lastS‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} = {𝑍, (𝑊‘0)}) |
| 119 | 118 | eleq1d 2826 |
. . . . . . . . 9
⊢
(((♯‘(𝑊
++ 〈“𝑍”〉)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ ({(lastS‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸 ↔ {𝑍, (𝑊‘0)} ∈ 𝐸)) |
| 120 | 119 | biimpcd 249 |
. . . . . . . 8
⊢
({(lastS‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸 → (((♯‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {𝑍, (𝑊‘0)} ∈ 𝐸)) |
| 121 | 120 | 3ad2ant3 1136 |
. . . . . . 7
⊢ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) → (((♯‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {𝑍, (𝑊‘0)} ∈ 𝐸)) |
| 122 | 121 | impl 455 |
. . . . . 6
⊢
(((((𝑊 ++
〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {𝑍, (𝑊‘0)} ∈ 𝐸) |
| 123 | 105, 122 | jca 511 |
. . . . 5
⊢
(((((𝑊 ++
〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ ({(lastS‘𝑊),
𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) |
| 124 | 123 | ex 412 |
. . . 4
⊢ ((((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁) → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ({(lastS‘𝑊),
𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸))) |
| 125 | 4, 124 | biimtrdi 253 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑁 ClWWalksN 𝐺) → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ({(lastS‘𝑊),
𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)))) |
| 126 | 1, 125 | mpcom 38 |
. 2
⊢ ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑁 ClWWalksN 𝐺) → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ({(lastS‘𝑊),
𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸))) |
| 127 | 126 | impcom 407 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (𝑊 ++
〈“𝑍”〉) ∈ (𝑁 ClWWalksN 𝐺)) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) |