Proof of Theorem clwlkclwwlklem2a1
Step | Hyp | Ref
| Expression |
1 | | lencl 13179 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
2 | | nn0cn 11179 |
. . . . . . . . . . . 12
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℂ) |
3 | | peano2cnm 10226 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑃) ∈
ℂ → ((#‘𝑃)
− 1) ∈ ℂ) |
4 | 3 | subid1d 10260 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑃) ∈
ℂ → (((#‘𝑃) − 1) − 0) = ((#‘𝑃) − 1)) |
5 | 4 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢
((#‘𝑃) ∈
ℂ → ((((#‘𝑃) − 1) − 0) − 1) =
(((#‘𝑃) − 1)
− 1)) |
6 | | sub1m1 11161 |
. . . . . . . . . . . . 13
⊢
((#‘𝑃) ∈
ℂ → (((#‘𝑃) − 1) − 1) = ((#‘𝑃) − 2)) |
7 | 5, 6 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢
((#‘𝑃) ∈
ℂ → ((((#‘𝑃) − 1) − 0) − 1) =
((#‘𝑃) −
2)) |
8 | 1, 2, 7 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ Word 𝑉 → ((((#‘𝑃) − 1) − 0) − 1) =
((#‘𝑃) −
2)) |
9 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((((#‘𝑃) − 1) − 0) − 1) =
((#‘𝑃) −
2)) |
10 | 9 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (0..^((((#‘𝑃) − 1) − 0) − 1)) =
(0..^((#‘𝑃) −
2))) |
11 | 10 | raleqdv 3121 |
. . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘𝑃) − 2)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
12 | 11 | biimpcd 238 |
. . . . . . 7
⊢
(∀𝑖 ∈
(0..^((((#‘𝑃) −
1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ∀𝑖 ∈ (0..^((#‘𝑃) − 2)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
13 | 12 | adantr 480 |
. . . . . 6
⊢
((∀𝑖 ∈
(0..^((((#‘𝑃) −
1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) → ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ∀𝑖 ∈ (0..^((#‘𝑃) − 2)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
14 | 13 | adantl 481 |
. . . . 5
⊢ ((( lastS
‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ∀𝑖 ∈ (0..^((#‘𝑃) − 2)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
15 | 14 | impcom 445 |
. . . 4
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → ∀𝑖 ∈ (0..^((#‘𝑃) − 2)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) |
16 | | lsw 13204 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1))) |
17 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
− 1) = 1 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ Word 𝑉 → (2 − 1) = 1) |
19 | 18 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → 1 = (2 − 1)) |
20 | 19 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) = ((#‘𝑃) − (2 − 1))) |
21 | 1, 2 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℂ) |
22 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → 2 ∈ ℂ) |
23 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → 1 ∈ ℂ) |
24 | 21, 22, 23 | subsubd 10299 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − (2 − 1)) = (((#‘𝑃) − 2) +
1)) |
25 | 20, 24 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) = (((#‘𝑃) − 2) + 1)) |
26 | 25 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → (𝑃‘((#‘𝑃) − 1)) = (𝑃‘(((#‘𝑃) − 2) + 1))) |
27 | 16, 26 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘(((#‘𝑃) − 2) + 1))) |
28 | 27 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ( lastS ‘𝑃) = (𝑃‘(((#‘𝑃) − 2) + 1))) |
29 | 28 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ( lastS ‘𝑃) = (𝑃‘0)) → ( lastS ‘𝑃) = (𝑃‘(((#‘𝑃) − 2) + 1))) |
30 | | eqeq1 2614 |
. . . . . . . . . . . . . 14
⊢ (( lastS
‘𝑃) = (𝑃‘0) → (( lastS
‘𝑃) = (𝑃‘(((#‘𝑃) − 2) + 1)) ↔ (𝑃‘0) = (𝑃‘(((#‘𝑃) − 2) + 1)))) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ( lastS ‘𝑃) = (𝑃‘0)) → (( lastS ‘𝑃) = (𝑃‘(((#‘𝑃) − 2) + 1)) ↔ (𝑃‘0) = (𝑃‘(((#‘𝑃) − 2) + 1)))) |
32 | 29, 31 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ( lastS ‘𝑃) = (𝑃‘0)) → (𝑃‘0) = (𝑃‘(((#‘𝑃) − 2) + 1))) |
33 | 32 | preq2d 4219 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ( lastS ‘𝑃) = (𝑃‘0)) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))}) |
34 | 33 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ( lastS ‘𝑃) = (𝑃‘0)) → ({(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} ∈ ran 𝐸)) |
35 | 34 | biimpd 218 |
. . . . . . . . 9
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ( lastS ‘𝑃) = (𝑃‘0)) → ({(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} ∈ ran 𝐸)) |
36 | 35 | ex 449 |
. . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (( lastS ‘𝑃) = (𝑃‘0) → ({(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} ∈ ran 𝐸))) |
37 | 36 | com13 86 |
. . . . . . 7
⊢ ({(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 → (( lastS ‘𝑃) = (𝑃‘0) → ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} ∈ ran 𝐸))) |
38 | 37 | adantl 481 |
. . . . . 6
⊢
((∀𝑖 ∈
(0..^((((#‘𝑃) −
1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) → (( lastS ‘𝑃) = (𝑃‘0) → ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} ∈ ran 𝐸))) |
39 | 38 | impcom 445 |
. . . . 5
⊢ ((( lastS
‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} ∈ ran 𝐸)) |
40 | 39 | impcom 445 |
. . . 4
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} ∈ ran 𝐸) |
41 | | ovex 6577 |
. . . . . 6
⊢
((#‘𝑃) −
2) ∈ V |
42 | 41 | a1i 11 |
. . . . 5
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → ((#‘𝑃) − 2) ∈ V) |
43 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑖 = ((#‘𝑃) − 2) → (𝑃‘𝑖) = (𝑃‘((#‘𝑃) − 2))) |
44 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑖 = ((#‘𝑃) − 2) → (𝑖 + 1) = (((#‘𝑃) − 2) + 1)) |
45 | 44 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑖 = ((#‘𝑃) − 2) → (𝑃‘(𝑖 + 1)) = (𝑃‘(((#‘𝑃) − 2) + 1))) |
46 | 43, 45 | preq12d 4220 |
. . . . . . 7
⊢ (𝑖 = ((#‘𝑃) − 2) → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))}) |
47 | 46 | eleq1d 2672 |
. . . . . 6
⊢ (𝑖 = ((#‘𝑃) − 2) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} ∈ ran 𝐸)) |
48 | 47 | ralunsn 4360 |
. . . . 5
⊢
(((#‘𝑃)
− 2) ∈ V → (∀𝑖 ∈ ((0..^((#‘𝑃) − 2)) ∪ {((#‘𝑃) − 2)}){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 2)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} ∈ ran 𝐸))) |
49 | 42, 48 | syl 17 |
. . . 4
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → (∀𝑖 ∈ ((0..^((#‘𝑃) − 2)) ∪ {((#‘𝑃) − 2)}){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 2)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} ∈ ran 𝐸))) |
50 | 15, 40, 49 | mpbir2and 959 |
. . 3
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → ∀𝑖 ∈ ((0..^((#‘𝑃) − 2)) ∪ {((#‘𝑃) − 2)}){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) |
51 | | 1e2m1 11013 |
. . . . . . . . . . 11
⊢ 1 = (2
− 1) |
52 | 51 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Word 𝑉 → 1 = (2 − 1)) |
53 | 52 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) = ((#‘𝑃) − (2 − 1))) |
54 | 53, 24 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) = (((#‘𝑃) − 2) + 1)) |
55 | 54 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑃 ∈ Word 𝑉 → (0..^((#‘𝑃) − 1)) = (0..^(((#‘𝑃) − 2) +
1))) |
56 | 55 | adantr 480 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (0..^((#‘𝑃) − 1)) = (0..^(((#‘𝑃) − 2) +
1))) |
57 | | nn0re 11178 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℝ) |
58 | | 2re 10967 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑃) ∈
ℕ0 → 2 ∈ ℝ) |
60 | 57, 59 | subge0d 10496 |
. . . . . . . . . . . . 13
⊢
((#‘𝑃) ∈
ℕ0 → (0 ≤ ((#‘𝑃) − 2) ↔ 2 ≤ (#‘𝑃))) |
61 | 60 | biimprd 237 |
. . . . . . . . . . . 12
⊢
((#‘𝑃) ∈
ℕ0 → (2 ≤ (#‘𝑃) → 0 ≤ ((#‘𝑃) − 2))) |
62 | | nn0z 11277 |
. . . . . . . . . . . . 13
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℤ) |
63 | | 2z 11286 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
64 | 63 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((#‘𝑃) ∈
ℕ0 → 2 ∈ ℤ) |
65 | 62, 64 | zsubcld 11363 |
. . . . . . . . . . . 12
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 2) ∈
ℤ) |
66 | 61, 65 | jctild 564 |
. . . . . . . . . . 11
⊢
((#‘𝑃) ∈
ℕ0 → (2 ≤ (#‘𝑃) → (((#‘𝑃) − 2) ∈ ℤ ∧ 0 ≤
((#‘𝑃) −
2)))) |
67 | 1, 66 | syl 17 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Word 𝑉 → (2 ≤ (#‘𝑃) → (((#‘𝑃) − 2) ∈ ℤ ∧ 0 ≤
((#‘𝑃) −
2)))) |
68 | 67 | imp 444 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (((#‘𝑃) − 2) ∈ ℤ ∧ 0 ≤
((#‘𝑃) −
2))) |
69 | | elnn0z 11267 |
. . . . . . . . 9
⊢
(((#‘𝑃)
− 2) ∈ ℕ0 ↔ (((#‘𝑃) − 2) ∈ ℤ ∧ 0 ≤
((#‘𝑃) −
2))) |
70 | 68, 69 | sylibr 223 |
. . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 2) ∈
ℕ0) |
71 | | elnn0uz 11601 |
. . . . . . . 8
⊢
(((#‘𝑃)
− 2) ∈ ℕ0 ↔ ((#‘𝑃) − 2) ∈
(ℤ≥‘0)) |
72 | 70, 71 | sylib 207 |
. . . . . . 7
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 2) ∈
(ℤ≥‘0)) |
73 | | fzosplitsn 12442 |
. . . . . . 7
⊢
(((#‘𝑃)
− 2) ∈ (ℤ≥‘0) → (0..^(((#‘𝑃) − 2) + 1)) =
((0..^((#‘𝑃) −
2)) ∪ {((#‘𝑃)
− 2)})) |
74 | 72, 73 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (0..^(((#‘𝑃) − 2) + 1)) = ((0..^((#‘𝑃) − 2)) ∪
{((#‘𝑃) −
2)})) |
75 | 56, 74 | eqtrd 2644 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (0..^((#‘𝑃) − 1)) = ((0..^((#‘𝑃) − 2)) ∪
{((#‘𝑃) −
2)})) |
76 | 75 | adantr 480 |
. . . 4
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → (0..^((#‘𝑃) − 1)) = ((0..^((#‘𝑃) − 2)) ∪
{((#‘𝑃) −
2)})) |
77 | 76 | raleqdv 3121 |
. . 3
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ ((0..^((#‘𝑃) − 2)) ∪ {((#‘𝑃) − 2)}){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
78 | 50, 77 | mpbird 246 |
. 2
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) |
79 | 78 | ex 449 |
1
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |