Proof of Theorem clwlkclwwlklem2a1
Step | Hyp | Ref
| Expression |
1 | | lencl 13502 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈
ℕ0) |
2 | | nn0cn 11486 |
. . . . . . . . . . . 12
⊢
((♯‘𝑃)
∈ ℕ0 → (♯‘𝑃) ∈ ℂ) |
3 | | peano2cnm 10531 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑃)
∈ ℂ → ((♯‘𝑃) − 1) ∈
ℂ) |
4 | 3 | subid1d 10565 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑃)
∈ ℂ → (((♯‘𝑃) − 1) − 0) =
((♯‘𝑃) −
1)) |
5 | 4 | oveq1d 6820 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑃)
∈ ℂ → ((((♯‘𝑃) − 1) − 0) − 1) =
(((♯‘𝑃) −
1) − 1)) |
6 | | sub1m1 11468 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑃)
∈ ℂ → (((♯‘𝑃) − 1) − 1) =
((♯‘𝑃) −
2)) |
7 | 5, 6 | eqtrd 2786 |
. . . . . . . . . . . 12
⊢
((♯‘𝑃)
∈ ℂ → ((((♯‘𝑃) − 1) − 0) − 1) =
((♯‘𝑃) −
2)) |
8 | 1, 2, 7 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ Word 𝑉 → ((((♯‘𝑃) − 1) − 0) − 1) =
((♯‘𝑃) −
2)) |
9 | 8 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) →
((((♯‘𝑃)
− 1) − 0) − 1) = ((♯‘𝑃) − 2)) |
10 | 9 | oveq2d 6821 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) →
(0..^((((♯‘𝑃)
− 1) − 0) − 1)) = (0..^((♯‘𝑃) − 2))) |
11 | 10 | raleqdv 3275 |
. . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∀𝑖 ∈
(0..^((((♯‘𝑃)
− 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((♯‘𝑃) − 2)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
12 | 11 | biimpcd 239 |
. . . . . . 7
⊢
(∀𝑖 ∈
(0..^((((♯‘𝑃)
− 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ∀𝑖 ∈
(0..^((♯‘𝑃)
− 2)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
13 | 12 | adantr 472 |
. . . . . 6
⊢
((∀𝑖 ∈
(0..^((((♯‘𝑃)
− 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) → ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ∀𝑖 ∈
(0..^((♯‘𝑃)
− 2)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
14 | 13 | adantl 473 |
. . . . 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 13530 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘((♯‘𝑃) − 1))) |
17 | | 2m1e1 11319 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
− 1) = 1 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ Word 𝑉 → (2 − 1) = 1) |
19 | 18 | eqcomd 2758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → 1 = (2 − 1)) |
20 | 19 | oveq2d 6821 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) = ((♯‘𝑃) − (2 −
1))) |
21 | 1, 2 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈ ℂ) |
22 | | 2cnd 11277 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → 2 ∈ ℂ) |
23 | | 1cnd 10240 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → 1 ∈ ℂ) |
24 | 21, 22, 23 | subsubd 10604 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − (2 − 1)) =
(((♯‘𝑃) −
2) + 1)) |
25 | 20, 24 | eqtrd 2786 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) = (((♯‘𝑃) − 2) +
1)) |
26 | 25 | fveq2d 6348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → (𝑃‘((♯‘𝑃) − 1)) = (𝑃‘(((♯‘𝑃) − 2) + 1))) |
27 | 16, 26 | eqtrd 2786 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘(((♯‘𝑃) − 2) + 1))) |
28 | 27 | adantr 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ( lastS ‘𝑃) = (𝑃‘(((♯‘𝑃) − 2) + 1))) |
29 | 28 | adantr 472 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ( lastS ‘𝑃) = (𝑃‘0)) → ( lastS ‘𝑃) = (𝑃‘(((♯‘𝑃) − 2) + 1))) |
30 | | eqeq1 2756 |
. . . . . . . . . . . . . 14
⊢ (( lastS
‘𝑃) = (𝑃‘0) → (( lastS
‘𝑃) = (𝑃‘(((♯‘𝑃) − 2) + 1)) ↔ (𝑃‘0) = (𝑃‘(((♯‘𝑃) − 2) + 1)))) |
31 | 30 | adantl 473 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ( lastS ‘𝑃) = (𝑃‘0)) → (( lastS ‘𝑃) = (𝑃‘(((♯‘𝑃) − 2) + 1)) ↔ (𝑃‘0) = (𝑃‘(((♯‘𝑃) − 2) + 1)))) |
32 | 29, 31 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ( lastS ‘𝑃) = (𝑃‘0)) → (𝑃‘0) = (𝑃‘(((♯‘𝑃) − 2) + 1))) |
33 | 32 | preq2d 4411 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ( lastS ‘𝑃) = (𝑃‘0)) → {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘(((♯‘𝑃) − 2) + 1))}) |
34 | 33 | eleq1d 2816 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ ( lastS ‘𝑃) = (𝑃‘0)) → ({(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘(((♯‘𝑃) − 2) + 1))} ∈ ran 𝐸)) |
35 | 34 | biimpd 219 |
. . . . . . . . 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 88 |
. . . . . . 7
⊢ ({(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 → (( lastS ‘𝑃) = (𝑃‘0) → ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘(((♯‘𝑃) − 2) + 1))} ∈ ran 𝐸))) |
38 | 37 | adantl 473 |
. . . . . 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 | | ovexd 6835 |
. . . . 5
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → ((♯‘𝑃) − 2) ∈ V) |
42 | | fveq2 6344 |
. . . . . . . 8
⊢ (𝑖 = ((♯‘𝑃) − 2) → (𝑃‘𝑖) = (𝑃‘((♯‘𝑃) − 2))) |
43 | | oveq1 6812 |
. . . . . . . . 9
⊢ (𝑖 = ((♯‘𝑃) − 2) → (𝑖 + 1) = (((♯‘𝑃) − 2) +
1)) |
44 | 43 | fveq2d 6348 |
. . . . . . . 8
⊢ (𝑖 = ((♯‘𝑃) − 2) → (𝑃‘(𝑖 + 1)) = (𝑃‘(((♯‘𝑃) − 2) + 1))) |
45 | 42, 44 | preq12d 4412 |
. . . . . . 7
⊢ (𝑖 = ((♯‘𝑃) − 2) → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘(((♯‘𝑃) − 2) + 1))}) |
46 | 45 | eleq1d 2816 |
. . . . . 6
⊢ (𝑖 = ((♯‘𝑃) − 2) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘(((♯‘𝑃) − 2) + 1))} ∈ ran 𝐸)) |
47 | 46 | ralunsn 4566 |
. . . . 5
⊢
(((♯‘𝑃)
− 2) ∈ V → (∀𝑖 ∈ ((0..^((♯‘𝑃) − 2)) ∪
{((♯‘𝑃) −
2)}){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (∀𝑖 ∈ (0..^((♯‘𝑃) − 2)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘(((♯‘𝑃) − 2) + 1))} ∈ ran 𝐸))) |
48 | 41, 47 | 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 𝐸))) |
49 | 15, 40, 48 | mpbir2and 995 |
. . 3
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → ∀𝑖 ∈ ((0..^((♯‘𝑃) − 2)) ∪
{((♯‘𝑃) −
2)}){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) |
50 | | 1e2m1 11320 |
. . . . . . . . . . 11
⊢ 1 = (2
− 1) |
51 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Word 𝑉 → 1 = (2 − 1)) |
52 | 51 | oveq2d 6821 |
. . . . . . . . 9
⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) = ((♯‘𝑃) − (2 −
1))) |
53 | 52, 24 | eqtrd 2786 |
. . . . . . . 8
⊢ (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) = (((♯‘𝑃) − 2) +
1)) |
54 | 53 | oveq2d 6821 |
. . . . . . 7
⊢ (𝑃 ∈ Word 𝑉 → (0..^((♯‘𝑃) − 1)) =
(0..^(((♯‘𝑃)
− 2) + 1))) |
55 | 54 | adantr 472 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) →
(0..^((♯‘𝑃)
− 1)) = (0..^(((♯‘𝑃) − 2) + 1))) |
56 | | nn0re 11485 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑃)
∈ ℕ0 → (♯‘𝑃) ∈ ℝ) |
57 | | 2re 11274 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑃)
∈ ℕ0 → 2 ∈ ℝ) |
59 | 56, 58 | subge0d 10801 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑃)
∈ ℕ0 → (0 ≤ ((♯‘𝑃) − 2) ↔ 2 ≤
(♯‘𝑃))) |
60 | 59 | biimprd 238 |
. . . . . . . . . . . 12
⊢
((♯‘𝑃)
∈ ℕ0 → (2 ≤ (♯‘𝑃) → 0 ≤ ((♯‘𝑃) − 2))) |
61 | | nn0z 11584 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑃)
∈ ℕ0 → (♯‘𝑃) ∈ ℤ) |
62 | | 2z 11593 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
63 | 62 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑃)
∈ ℕ0 → 2 ∈ ℤ) |
64 | 61, 63 | zsubcld 11671 |
. . . . . . . . . . . 12
⊢
((♯‘𝑃)
∈ ℕ0 → ((♯‘𝑃) − 2) ∈
ℤ) |
65 | 60, 64 | jctild 567 |
. . . . . . . . . . 11
⊢
((♯‘𝑃)
∈ ℕ0 → (2 ≤ (♯‘𝑃) → (((♯‘𝑃) − 2) ∈ ℤ ∧ 0 ≤
((♯‘𝑃) −
2)))) |
66 | 1, 65 | syl 17 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Word 𝑉 → (2 ≤ (♯‘𝑃) → (((♯‘𝑃) − 2) ∈ ℤ
∧ 0 ≤ ((♯‘𝑃) − 2)))) |
67 | 66 | imp 444 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((♯‘𝑃) − 2) ∈ ℤ
∧ 0 ≤ ((♯‘𝑃) − 2))) |
68 | | elnn0z 11574 |
. . . . . . . . 9
⊢
(((♯‘𝑃)
− 2) ∈ ℕ0 ↔ (((♯‘𝑃) − 2) ∈ ℤ ∧ 0 ≤
((♯‘𝑃) −
2))) |
69 | 67, 68 | sylibr 224 |
. . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 2) ∈
ℕ0) |
70 | | elnn0uz 11910 |
. . . . . . . 8
⊢
(((♯‘𝑃)
− 2) ∈ ℕ0 ↔ ((♯‘𝑃) − 2) ∈
(ℤ≥‘0)) |
71 | 69, 70 | sylib 208 |
. . . . . . 7
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 2) ∈
(ℤ≥‘0)) |
72 | | fzosplitsn 12762 |
. . . . . . 7
⊢
(((♯‘𝑃)
− 2) ∈ (ℤ≥‘0) →
(0..^(((♯‘𝑃)
− 2) + 1)) = ((0..^((♯‘𝑃) − 2)) ∪ {((♯‘𝑃) − 2)})) |
73 | 71, 72 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) →
(0..^(((♯‘𝑃)
− 2) + 1)) = ((0..^((♯‘𝑃) − 2)) ∪ {((♯‘𝑃) − 2)})) |
74 | 55, 73 | eqtrd 2786 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) →
(0..^((♯‘𝑃)
− 1)) = ((0..^((♯‘𝑃) − 2)) ∪ {((♯‘𝑃) − 2)})) |
75 | 74 | adantr 472 |
. . . 4
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → (0..^((♯‘𝑃) − 1)) =
((0..^((♯‘𝑃)
− 2)) ∪ {((♯‘𝑃) − 2)})) |
76 | 75 | raleqdv 3275 |
. . 3
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ ((0..^((♯‘𝑃) − 2)) ∪
{((♯‘𝑃) −
2)}){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
77 | 49, 76 | mpbird 247 |
. 2
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) |
78 | 77 | ex 449 |
1
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |