Proof of Theorem clwlknf1oclwwlknlem1
Step | Hyp | Ref
| Expression |
1 | | clwlkwlk 27716 |
. . 3
⊢ (𝐶 ∈ (ClWalks‘𝐺) → 𝐶 ∈ (Walks‘𝐺)) |
2 | | wlkcpr 27570 |
. . . 4
⊢ (𝐶 ∈ (Walks‘𝐺) ↔ (1st
‘𝐶)(Walks‘𝐺)(2nd ‘𝐶)) |
3 | | eqid 2738 |
. . . . . . . 8
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
4 | 3 | wlkpwrd 27559 |
. . . . . . 7
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (2nd ‘𝐶) ∈ Word (Vtx‘𝐺)) |
5 | | lencl 13974 |
. . . . . . . . 9
⊢
((2nd ‘𝐶) ∈ Word (Vtx‘𝐺) → (♯‘(2nd
‘𝐶)) ∈
ℕ0) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (♯‘(2nd
‘𝐶)) ∈
ℕ0) |
7 | | wlklenvm1 27563 |
. . . . . . . . . . 11
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (♯‘(1st
‘𝐶)) =
((♯‘(2nd ‘𝐶)) − 1)) |
8 | 7 | breq2d 5042 |
. . . . . . . . . 10
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (1 ≤
(♯‘(1st ‘𝐶)) ↔ 1 ≤
((♯‘(2nd ‘𝐶)) − 1))) |
9 | | 1red 10720 |
. . . . . . . . . . . . 13
⊢
((♯‘(2nd ‘𝐶)) ∈ ℕ0 → 1
∈ ℝ) |
10 | | nn0re 11985 |
. . . . . . . . . . . . 13
⊢
((♯‘(2nd ‘𝐶)) ∈ ℕ0 →
(♯‘(2nd ‘𝐶)) ∈ ℝ) |
11 | 9, 9, 10 | leaddsub2d 11320 |
. . . . . . . . . . . 12
⊢
((♯‘(2nd ‘𝐶)) ∈ ℕ0 → ((1 +
1) ≤ (♯‘(2nd ‘𝐶)) ↔ 1 ≤
((♯‘(2nd ‘𝐶)) − 1))) |
12 | | 1p1e2 11841 |
. . . . . . . . . . . . . 14
⊢ (1 + 1) =
2 |
13 | 12 | breq1i 5037 |
. . . . . . . . . . . . 13
⊢ ((1 + 1)
≤ (♯‘(2nd ‘𝐶)) ↔ 2 ≤
(♯‘(2nd ‘𝐶))) |
14 | 13 | biimpi 219 |
. . . . . . . . . . . 12
⊢ ((1 + 1)
≤ (♯‘(2nd ‘𝐶)) → 2 ≤
(♯‘(2nd ‘𝐶))) |
15 | 11, 14 | syl6bir 257 |
. . . . . . . . . . 11
⊢
((♯‘(2nd ‘𝐶)) ∈ ℕ0 → (1 ≤
((♯‘(2nd ‘𝐶)) − 1) → 2 ≤
(♯‘(2nd ‘𝐶)))) |
16 | 4, 5, 15 | 3syl 18 |
. . . . . . . . . 10
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (1 ≤
((♯‘(2nd ‘𝐶)) − 1) → 2 ≤
(♯‘(2nd ‘𝐶)))) |
17 | 8, 16 | sylbid 243 |
. . . . . . . . 9
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (1 ≤
(♯‘(1st ‘𝐶)) → 2 ≤
(♯‘(2nd ‘𝐶)))) |
18 | 17 | imp 410 |
. . . . . . . 8
⊢
(((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) ∧ 1 ≤
(♯‘(1st ‘𝐶))) → 2 ≤
(♯‘(2nd ‘𝐶))) |
19 | | ige2m1fz 13088 |
. . . . . . . 8
⊢
(((♯‘(2nd ‘𝐶)) ∈ ℕ0 ∧ 2 ≤
(♯‘(2nd ‘𝐶))) → ((♯‘(2nd
‘𝐶)) − 1)
∈ (0...(♯‘(2nd ‘𝐶)))) |
20 | 6, 18, 19 | syl2an2r 685 |
. . . . . . 7
⊢
(((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) ∧ 1 ≤
(♯‘(1st ‘𝐶))) → ((♯‘(2nd
‘𝐶)) − 1)
∈ (0...(♯‘(2nd ‘𝐶)))) |
21 | | pfxlen 14134 |
. . . . . . 7
⊢
(((2nd ‘𝐶) ∈ Word (Vtx‘𝐺) ∧ ((♯‘(2nd
‘𝐶)) − 1)
∈ (0...(♯‘(2nd ‘𝐶)))) → (♯‘((2nd
‘𝐶) prefix
((♯‘(2nd ‘𝐶)) − 1))) =
((♯‘(2nd ‘𝐶)) − 1)) |
22 | 4, 20, 21 | syl2an2r 685 |
. . . . . 6
⊢
(((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) ∧ 1 ≤
(♯‘(1st ‘𝐶))) → (♯‘((2nd
‘𝐶) prefix
((♯‘(2nd ‘𝐶)) − 1))) =
((♯‘(2nd ‘𝐶)) − 1)) |
23 | 7 | eqcomd 2744 |
. . . . . . 7
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → ((♯‘(2nd
‘𝐶)) − 1) =
(♯‘(1st ‘𝐶))) |
24 | 23 | adantr 484 |
. . . . . 6
⊢
(((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) ∧ 1 ≤
(♯‘(1st ‘𝐶))) → ((♯‘(2nd
‘𝐶)) − 1) =
(♯‘(1st ‘𝐶))) |
25 | 22, 24 | eqtrd 2773 |
. . . . 5
⊢
(((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) ∧ 1 ≤
(♯‘(1st ‘𝐶))) → (♯‘((2nd
‘𝐶) prefix
((♯‘(2nd ‘𝐶)) − 1))) =
(♯‘(1st ‘𝐶))) |
26 | 25 | ex 416 |
. . . 4
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (1 ≤
(♯‘(1st ‘𝐶)) → (♯‘((2nd
‘𝐶) prefix
((♯‘(2nd ‘𝐶)) − 1))) =
(♯‘(1st ‘𝐶)))) |
27 | 2, 26 | sylbi 220 |
. . 3
⊢ (𝐶 ∈ (Walks‘𝐺) → (1 ≤
(♯‘(1st ‘𝐶)) → (♯‘((2nd
‘𝐶) prefix
((♯‘(2nd ‘𝐶)) − 1))) =
(♯‘(1st ‘𝐶)))) |
28 | 1, 27 | syl 17 |
. 2
⊢ (𝐶 ∈ (ClWalks‘𝐺) → (1 ≤
(♯‘(1st ‘𝐶)) → (♯‘((2nd
‘𝐶) prefix
((♯‘(2nd ‘𝐶)) − 1))) =
(♯‘(1st ‘𝐶)))) |
29 | 28 | imp 410 |
1
⊢ ((𝐶 ∈ (ClWalks‘𝐺) ∧ 1 ≤
(♯‘(1st ‘𝐶))) → (♯‘((2nd
‘𝐶) prefix
((♯‘(2nd ‘𝐶)) − 1))) =
(♯‘(1st ‘𝐶))) |