Proof of Theorem clwlknf1oclwwlknlem1
Step | Hyp | Ref
| Expression |
1 | | clwlkwlk 28143 |
. . 3
⊢ (𝐶 ∈ (ClWalks‘𝐺) → 𝐶 ∈ (Walks‘𝐺)) |
2 | | wlkcpr 27996 |
. . . 4
⊢ (𝐶 ∈ (Walks‘𝐺) ↔ (1st
‘𝐶)(Walks‘𝐺)(2nd ‘𝐶)) |
3 | | eqid 2738 |
. . . . . . . 8
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
4 | 3 | wlkpwrd 27984 |
. . . . . . 7
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (2nd ‘𝐶) ∈ Word (Vtx‘𝐺)) |
5 | | lencl 14236 |
. . . . . . . . 9
⊢
((2nd ‘𝐶) ∈ Word (Vtx‘𝐺) → (♯‘(2nd
‘𝐶)) ∈
ℕ0) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (♯‘(2nd
‘𝐶)) ∈
ℕ0) |
7 | | wlklenvm1 27989 |
. . . . . . . . . . 11
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (♯‘(1st
‘𝐶)) =
((♯‘(2nd ‘𝐶)) − 1)) |
8 | 7 | breq2d 5086 |
. . . . . . . . . 10
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (1 ≤
(♯‘(1st ‘𝐶)) ↔ 1 ≤
((♯‘(2nd ‘𝐶)) − 1))) |
9 | | 1red 10976 |
. . . . . . . . . . . . 13
⊢
((♯‘(2nd ‘𝐶)) ∈ ℕ0 → 1
∈ ℝ) |
10 | | nn0re 12242 |
. . . . . . . . . . . . 13
⊢
((♯‘(2nd ‘𝐶)) ∈ ℕ0 →
(♯‘(2nd ‘𝐶)) ∈ ℝ) |
11 | 9, 9, 10 | leaddsub2d 11577 |
. . . . . . . . . . . 12
⊢
((♯‘(2nd ‘𝐶)) ∈ ℕ0 → ((1 +
1) ≤ (♯‘(2nd ‘𝐶)) ↔ 1 ≤
((♯‘(2nd ‘𝐶)) − 1))) |
12 | | 1p1e2 12098 |
. . . . . . . . . . . . . 14
⊢ (1 + 1) =
2 |
13 | 12 | breq1i 5081 |
. . . . . . . . . . . . 13
⊢ ((1 + 1)
≤ (♯‘(2nd ‘𝐶)) ↔ 2 ≤
(♯‘(2nd ‘𝐶))) |
14 | 13 | biimpi 215 |
. . . . . . . . . . . 12
⊢ ((1 + 1)
≤ (♯‘(2nd ‘𝐶)) → 2 ≤
(♯‘(2nd ‘𝐶))) |
15 | 11, 14 | syl6bir 253 |
. . . . . . . . . . 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 239 |
. . . . . . . . 9
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (1 ≤
(♯‘(1st ‘𝐶)) → 2 ≤
(♯‘(2nd ‘𝐶)))) |
18 | 17 | imp 407 |
. . . . . . . 8
⊢
(((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) ∧ 1 ≤
(♯‘(1st ‘𝐶))) → 2 ≤
(♯‘(2nd ‘𝐶))) |
19 | | ige2m1fz 13346 |
. . . . . . . 8
⊢
(((♯‘(2nd ‘𝐶)) ∈ ℕ0 ∧ 2 ≤
(♯‘(2nd ‘𝐶))) → ((♯‘(2nd
‘𝐶)) − 1)
∈ (0...(♯‘(2nd ‘𝐶)))) |
20 | 6, 18, 19 | syl2an2r 682 |
. . . . . . 7
⊢
(((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) ∧ 1 ≤
(♯‘(1st ‘𝐶))) → ((♯‘(2nd
‘𝐶)) − 1)
∈ (0...(♯‘(2nd ‘𝐶)))) |
21 | | pfxlen 14396 |
. . . . . . 7
⊢
(((2nd ‘𝐶) ∈ Word (Vtx‘𝐺) ∧ ((♯‘(2nd
‘𝐶)) − 1)
∈ (0...(♯‘(2nd ‘𝐶)))) → (♯‘((2nd
‘𝐶) prefix
((♯‘(2nd ‘𝐶)) − 1))) =
((♯‘(2nd ‘𝐶)) − 1)) |
22 | 4, 20, 21 | syl2an2r 682 |
. . . . . 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 481 |
. . . . . 6
⊢
(((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) ∧ 1 ≤
(♯‘(1st ‘𝐶))) → ((♯‘(2nd
‘𝐶)) − 1) =
(♯‘(1st ‘𝐶))) |
25 | 22, 24 | eqtrd 2778 |
. . . . 5
⊢
(((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) ∧ 1 ≤
(♯‘(1st ‘𝐶))) → (♯‘((2nd
‘𝐶) prefix
((♯‘(2nd ‘𝐶)) − 1))) =
(♯‘(1st ‘𝐶))) |
26 | 25 | ex 413 |
. . . 4
⊢
((1st ‘𝐶)(Walks‘𝐺)(2nd ‘𝐶) → (1 ≤
(♯‘(1st ‘𝐶)) → (♯‘((2nd
‘𝐶) prefix
((♯‘(2nd ‘𝐶)) − 1))) =
(♯‘(1st ‘𝐶)))) |
27 | 2, 26 | sylbi 216 |
. . 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 407 |
1
⊢ ((𝐶 ∈ (ClWalks‘𝐺) ∧ 1 ≤
(♯‘(1st ‘𝐶))) → (♯‘((2nd
‘𝐶) prefix
((♯‘(2nd ‘𝐶)) − 1))) =
(♯‘(1st ‘𝐶))) |