Step | Hyp | Ref
| Expression |
1 | | clwwlknprop 26300 |
. . 3
⊢ ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁))) |
2 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝑉 ∈ V) |
3 | 2 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁)) → 𝑉 ∈ V) |
4 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝐸 ∈ V) |
5 | 4 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁)) → 𝐸 ∈ V) |
6 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → 𝑁 ∈
ℕ0) |
7 | 6 | adantl 481 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁)) → 𝑁 ∈
ℕ0) |
8 | | isclwwlkn 26297 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑊 ++
〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁))) |
9 | 3, 5, 7, 8 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁)) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁))) |
10 | | isclwwlk 26296 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸))) |
11 | 10 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁)) → ((𝑊 ++ 〈“𝑍”〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸))) |
12 | 11 | anbi1d 737 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁)) → (((𝑊 ++ 〈“𝑍”〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁))) |
13 | 9, 12 | bitrd 267 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁)) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁))) |
14 | | ige2m2fzo 12398 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈ (0..^(𝑁 − 1))) |
15 | 14 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 − 2) ∈
(0..^(𝑁 −
1))) |
16 | 15 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (𝑁 − 2) ∈ (0..^(𝑁 − 1))) |
17 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁 → ((#‘(𝑊 ++ 〈“𝑍”〉)) − 1) = (𝑁 − 1)) |
18 | 17 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁 → (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)) = (0..^(𝑁 − 1))) |
19 | 18 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢
((#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁 → ((𝑁 − 2) ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1))
↔ (𝑁 − 2) ∈
(0..^(𝑁 −
1)))) |
20 | 19 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑁 − 2) ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1))
↔ (𝑁 − 2) ∈
(0..^(𝑁 −
1)))) |
21 | 16, 20 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (𝑁 − 2) ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) −
1))) |
22 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑁 − 2) → ((𝑊 ++ 〈“𝑍”〉)‘𝑖) = ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2))) |
23 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = (𝑁 − 2) → (𝑖 + 1) = ((𝑁 − 2) + 1)) |
24 | 23 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑁 − 2) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))) |
25 | 22, 24 | preq12d 4220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑁 − 2) → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))}) |
26 | 25 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑁 − 2) → ({((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))} ∈ ran 𝐸)) |
27 | 26 | rspcv 3278 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 − 2) ∈
(0..^((#‘(𝑊 ++
〈“𝑍”〉)) − 1)) →
(∀𝑖 ∈
(0..^((#‘(𝑊 ++
〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 → {((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))} ∈ ran 𝐸)) |
28 | 21, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 → {((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))} ∈ ran 𝐸)) |
29 | | ccatws1lenrev 13260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁 → (#‘𝑊) = (𝑁 − 1))) |
30 | 29 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁 → (#‘𝑊) = (𝑁 − 1))) |
31 | | eluzelcn 11575 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℂ) |
32 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℂ) |
33 | 31, 32, 32 | subsub4d 10302 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 1) − 1) = (𝑁 − (1 + 1))) |
34 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 + 1) =
2 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 + 1) = 2) |
36 | 35 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − (1 + 1)) = (𝑁 − 2)) |
37 | 33, 36 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) = ((𝑁 − 1) − 1)) |
38 | 37 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 − 2) =
((𝑁 − 1) −
1)) |
39 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑊) =
(𝑁 − 1) →
((#‘𝑊) − 1) =
((𝑁 − 1) −
1)) |
40 | 39 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑊) =
(𝑁 − 1) →
((𝑁 − 1) − 1) =
((#‘𝑊) −
1)) |
41 | 38, 40 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → (𝑁 − 2) = ((#‘𝑊) − 1)) |
42 | 41 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘𝑊) =
(𝑁 − 1) → (𝑁 − 2) = ((#‘𝑊) − 1))) |
43 | 30, 42 | syld 46 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁 → (𝑁 − 2) = ((#‘𝑊) − 1))) |
44 | 43 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (𝑁 − 2) = ((#‘𝑊) − 1)) |
45 | 44 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)) = ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1))) |
46 | | simpl1 1057 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → 𝑊 ∈ Word 𝑉) |
47 | | s1cl 13235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑍 ∈ 𝑉 → 〈“𝑍”〉 ∈ Word 𝑉) |
48 | 47 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ 〈“𝑍”〉 ∈ Word 𝑉) |
49 | 48 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) →
〈“𝑍”〉
∈ Word 𝑉) |
50 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤
𝑁)) |
51 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
52 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 1 ∈
ℝ) |
53 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 2 ∈
ℝ |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 2 ∈
ℝ) |
55 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 𝑁 ∈ ℝ) |
56 | | 1lt2 11071 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 1 <
2 |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 1 <
2) |
58 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 2 ≤ 𝑁) |
59 | 52, 54, 55, 57, 58 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 1 < 𝑁) |
60 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℝ → 1 ∈
ℝ) |
61 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℝ) |
62 | 60, 61 | posdifd 10493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℝ → (1 <
𝑁 ↔ 0 < (𝑁 − 1))) |
63 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → (1 < 𝑁 ↔ 0 < (𝑁 − 1))) |
64 | 59, 63 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) → 0 < (𝑁 − 1)) |
65 | 64 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℝ → (2 ≤
𝑁 → 0 < (𝑁 − 1))) |
66 | 51, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℤ → (2 ≤
𝑁 → 0 < (𝑁 − 1))) |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (2 ∈
ℤ → (𝑁 ∈
ℤ → (2 ≤ 𝑁
→ 0 < (𝑁 −
1)))) |
68 | 67 | 3imp 1249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 2 ≤ 𝑁) → 0 < (𝑁 − 1)) |
69 | 50, 68 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘2) → 0 < (𝑁 − 1)) |
70 | 69 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ 0 < (𝑁 −
1)) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → 0 <
(𝑁 −
1)) |
72 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑊) =
(𝑁 − 1) → (0
< (#‘𝑊) ↔ 0
< (𝑁 −
1))) |
73 | 72 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 −
1))) |
74 | 71, 73 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → 0 <
(#‘𝑊)) |
75 | | hashneq0 13016 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑊 ∈ Word 𝑉 → (0 < (#‘𝑊) ↔ 𝑊 ≠ ∅)) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (0 < (#‘𝑊)
↔ 𝑊 ≠
∅)) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → (0 <
(#‘𝑊) ↔ 𝑊 ≠ ∅)) |
78 | 74, 77 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → 𝑊 ≠ ∅) |
79 | 78 | 3adantl2 1211 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → 𝑊 ≠ ∅) |
80 | 46, 49, 79 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)) |
81 | 80 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘𝑊) =
(𝑁 − 1) → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅))) |
82 | 30, 81 | syld 46 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁 → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅))) |
83 | 82 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)) |
84 | | ccatval1lsw 13221 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1)) = ( lastS
‘𝑊)) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘((#‘𝑊) − 1)) = ( lastS
‘𝑊)) |
86 | 45, 85 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)) = ( lastS ‘𝑊)) |
87 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (2
− 1) = 1 |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 − 1) = 1) |
89 | 88 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 = (2 − 1)) |
90 | 89 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) = (𝑁 − (2 − 1))) |
91 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ ℂ) |
92 | 31, 91, 32 | subsubd 10299 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − (2 − 1)) = ((𝑁 − 2) +
1)) |
93 | 90, 92 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 2) + 1) = (𝑁 − 1)) |
94 | 93 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((𝑁 − 2) + 1)
= (𝑁 −
1)) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → ((𝑁 − 2) + 1) = (𝑁 − 1)) |
96 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑊) =
(𝑁 − 1) →
(((𝑁 − 2) + 1) =
(#‘𝑊) ↔ ((𝑁 − 2) + 1) = (𝑁 − 1))) |
97 | 96 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → (((𝑁 − 2) + 1) =
(#‘𝑊) ↔ ((𝑁 − 2) + 1) = (𝑁 − 1))) |
98 | 95, 97 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → ((𝑁 − 2) + 1) =
(#‘𝑊)) |
99 | 98 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘𝑊) =
(𝑁 − 1) →
((𝑁 − 2) + 1) =
(#‘𝑊))) |
100 | 30, 99 | syld 46 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁 → ((𝑁 − 2) + 1) = (#‘𝑊))) |
101 | 100 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑁 − 2) + 1) = (#‘𝑊)) |
102 | 101 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊))) |
103 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉)) |
104 | 103 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉)) |
105 | 104 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉)) |
106 | | ccatws1ls 13262 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊)) = 𝑍) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘(#‘𝑊)) = 𝑍) |
108 | 102, 107 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1)) = 𝑍) |
109 | 86, 108 | preq12d 4220 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → {((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))} = {( lastS ‘𝑊), 𝑍}) |
110 | 109 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → ({((𝑊 ++ 〈“𝑍”〉)‘(𝑁 − 2)), ((𝑊 ++ 〈“𝑍”〉)‘((𝑁 − 2) + 1))} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), 𝑍} ∈ ran 𝐸)) |
111 | 28, 110 | sylibd 228 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁) → (∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 → {( lastS ‘𝑊), 𝑍} ∈ ran 𝐸)) |
112 | 111 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁 → (∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 → {( lastS ‘𝑊), 𝑍} ∈ ran 𝐸))) |
113 | 112 | com13 86 |
. . . . . . . . . 10
⊢
(∀𝑖 ∈
(0..^((#‘(𝑊 ++
〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 → ((#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁 → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ {( lastS ‘𝑊),
𝑍} ∈ ran 𝐸))) |
114 | 113 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) → ((#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁 → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ {( lastS ‘𝑊),
𝑍} ∈ ran 𝐸))) |
115 | 114 | imp 444 |
. . . . . . . 8
⊢ ((((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁) → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ {( lastS ‘𝑊),
𝑍} ∈ ran 𝐸)) |
116 | 115 | imp 444 |
. . . . . . 7
⊢
(((((𝑊 ++
〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {( lastS ‘𝑊),
𝑍} ∈ ran 𝐸) |
117 | 104 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉)) |
118 | | lswccats1 13263 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ( lastS ‘(𝑊 ++ 〈“𝑍”〉)) = 𝑍) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → ( lastS
‘(𝑊 ++
〈“𝑍”〉)) = 𝑍) |
120 | 69 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ 0 < (𝑁 −
1)) |
121 | 120 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → 0 <
(𝑁 −
1)) |
122 | 72 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → (0 <
(#‘𝑊) ↔ 0 <
(𝑁 −
1))) |
123 | 121, 122 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → 0 <
(#‘𝑊)) |
124 | | ccatfv0 13220 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → ((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) |
125 | 46, 49, 123, 124 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → ((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) |
126 | 119, 125 | preq12d 4220 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (#‘𝑊) = (𝑁 − 1)) → {( lastS
‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} = {𝑍, (𝑊‘0)}) |
127 | 126 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘𝑊) =
(𝑁 − 1) → {(
lastS ‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} = {𝑍, (𝑊‘0)})) |
128 | 30, 127 | syld 46 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁 → {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} = {𝑍, (𝑊‘0)})) |
129 | 128 | impcom 445 |
. . . . . . . . . . 11
⊢
(((#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {( lastS ‘(𝑊
++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} = {𝑍, (𝑊‘0)}) |
130 | 129 | eleq1d 2672 |
. . . . . . . . . 10
⊢
(((#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ ({( lastS ‘(𝑊
++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸 ↔ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) |
131 | 130 | biimpcd 238 |
. . . . . . . . 9
⊢ ({( lastS
‘(𝑊 ++
〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸 → (((#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) |
132 | 131 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) → (((#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁 ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) |
133 | 132 | impl 648 |
. . . . . . 7
⊢
(((((𝑊 ++
〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ {𝑍, (𝑊‘0)} ∈ ran 𝐸) |
134 | 116, 133 | jca 553 |
. . . . . 6
⊢
(((((𝑊 ++
〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) − 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ ({( lastS ‘𝑊),
𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) |
135 | 134 | ex 449 |
. . . . 5
⊢ ((((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑊 ++ 〈“𝑍”〉)) = 𝑁) → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ({( lastS ‘𝑊),
𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸))) |
136 | 13, 135 | syl6bi 242 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ (#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁)) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ({( lastS ‘𝑊),
𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)))) |
137 | 136 | 3adant2 1073 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘(𝑊 ++
〈“𝑍”〉)) = 𝑁)) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ({( lastS ‘𝑊),
𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)))) |
138 | 1, 137 | mpcom 37 |
. 2
⊢ ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ({( lastS ‘𝑊),
𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸))) |
139 | 138 | impcom 445 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ (𝑊 ++
〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ({( lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) |