Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | wwlksnextprop.e |
. . . . 5
⊢ 𝐸 = (Edg‘𝐺) |
3 | 1, 2 | wwlknp 41045 |
. . . 4
⊢ (𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) |
4 | | fzonn0p1 12411 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0..^(𝑁 + 1))) |
5 | 4 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ (0..^(𝑁 + 1))) |
6 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑁 → (𝑊‘𝑖) = (𝑊‘𝑁)) |
7 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑁 → (𝑖 + 1) = (𝑁 + 1)) |
8 | 7 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑁 → (𝑊‘(𝑖 + 1)) = (𝑊‘(𝑁 + 1))) |
9 | 6, 8 | preq12d 4220 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑁 → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))}) |
10 | 9 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑁 → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
11 | 10 | rspcv 3278 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (0..^(𝑁 + 1)) → (∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
12 | 5, 11 | syl 17 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
13 | 12 | imp 444 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸) |
14 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 𝑊 ∈ Word (Vtx‘𝐺)) |
15 | | 1zzd 11285 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 1 ∈
ℤ) |
16 | | lencl 13179 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (#‘𝑊) ∈
ℕ0) |
17 | 16 | nn0zd 11356 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (#‘𝑊) ∈
ℤ) |
18 | 17 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
(#‘𝑊) ∈
ℤ) |
19 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
20 | 19 | nn0zd 11356 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈
ℤ) |
22 | 15, 18, 21 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (1
∈ ℤ ∧ (#‘𝑊) ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ)) |
23 | | nn0ge0 11195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
24 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℝ) |
25 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
26 | 24, 25 | addge02d 10495 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (0 ≤ 𝑁 ↔ 1
≤ (𝑁 +
1))) |
27 | 23, 26 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ 1 ≤ (𝑁 +
1)) |
28 | 27 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 1 ≤
(𝑁 + 1)) |
29 | 19 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
30 | 29 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
31 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ≤
(#‘𝑊) ↔ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
32 | 30, 31 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ ((#‘𝑊) =
((𝑁 + 1) + 1) → (𝑁 + 1) ≤ (#‘𝑊))) |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑊) ∈
ℕ0 → (𝑁 ∈ ℕ0 →
((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 + 1) ≤ (#‘𝑊)))) |
34 | 33 | com23 84 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑊) ∈
ℕ0 → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑁 + 1) ≤ (#‘𝑊)))) |
35 | 16, 34 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑁 + 1) ≤ (#‘𝑊)))) |
36 | 35 | imp31 447 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ≤ (#‘𝑊)) |
37 | 28, 36 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (1 ≤
(𝑁 + 1) ∧ (𝑁 + 1) ≤ (#‘𝑊))) |
38 | | elfz2 12204 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 + 1) ∈ (1...(#‘𝑊)) ↔ ((1 ∈ ℤ
∧ (#‘𝑊) ∈
ℤ ∧ (𝑁 + 1)
∈ ℤ) ∧ (1 ≤ (𝑁 + 1) ∧ (𝑁 + 1) ≤ (#‘𝑊)))) |
39 | 22, 37, 38 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈ (1...(#‘𝑊))) |
40 | 14, 39 | jca 553 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(#‘𝑊)))) |
41 | | swrd0fvlsw 13295 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(#‘𝑊))) → ( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑊‘((𝑁 + 1) − 1))) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → ( lastS
‘(𝑊 substr 〈0,
(𝑁 + 1)〉)) = (𝑊‘((𝑁 + 1) − 1))) |
43 | | nn0cn 11179 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
44 | | 1cnd 9935 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
45 | 43, 44 | pncand 10272 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
46 | 45 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑊‘((𝑁 + 1) − 1)) = (𝑊‘𝑁)) |
47 | 46 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑊‘((𝑁 + 1) − 1)) = (𝑊‘𝑁)) |
48 | 42, 47 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → ( lastS
‘(𝑊 substr 〈0,
(𝑁 + 1)〉)) = (𝑊‘𝑁)) |
49 | | lsw 13204 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
50 | 49 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → ( lastS
‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
51 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
((#‘𝑊) − 1) =
(((𝑁 + 1) + 1) −
1)) |
52 | 51 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) → (𝑊‘((#‘𝑊) − 1)) = (𝑊‘(((𝑁 + 1) + 1) − 1))) |
53 | 52 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊‘((#‘𝑊) − 1)) = (𝑊‘(((𝑁 + 1) + 1) − 1))) |
54 | 19 | nn0cnd 11230 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
55 | 54, 44 | pncand 10272 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) |
56 | 55 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑊‘(((𝑁 + 1) + 1) − 1)) = (𝑊‘(𝑁 + 1))) |
57 | 53, 56 | sylan9eq 2664 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑊‘((#‘𝑊) − 1)) = (𝑊‘(𝑁 + 1))) |
58 | 50, 57 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → ( lastS
‘𝑊) = (𝑊‘(𝑁 + 1))) |
59 | 48, 58 | preq12d 4220 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → {( lastS
‘(𝑊 substr 〈0,
(𝑁 + 1)〉)), ( lastS
‘𝑊)} = {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))}) |
60 | 59 | eleq1d 2672 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → ({(
lastS ‘(𝑊 substr
〈0, (𝑁 + 1)〉)), (
lastS ‘𝑊)} ∈
𝐸 ↔ {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
61 | 60 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ({( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑊)} ∈ 𝐸 ↔ {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
62 | 13, 61 | mpbird 246 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → {( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑊)} ∈ 𝐸) |
63 | 62 | exp31 628 |
. . . . . 6
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → {( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑊)} ∈ 𝐸))) |
64 | 63 | com23 84 |
. . . . 5
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → (𝑁 ∈ ℕ0 → {( lastS
‘(𝑊 substr 〈0,
(𝑁 + 1)〉)), ( lastS
‘𝑊)} ∈ 𝐸))) |
65 | 64 | 3impia 1253 |
. . . 4
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (𝑁 ∈ ℕ0 → {( lastS
‘(𝑊 substr 〈0,
(𝑁 + 1)〉)), ( lastS
‘𝑊)} ∈ 𝐸)) |
66 | 3, 65 | syl 17 |
. . 3
⊢ (𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺) → (𝑁 ∈ ℕ0 → {( lastS
‘(𝑊 substr 〈0,
(𝑁 + 1)〉)), ( lastS
‘𝑊)} ∈ 𝐸)) |
67 | | wwlksnextprop.x |
. . 3
⊢ 𝑋 = ((𝑁 + 1) WWalkSN 𝐺) |
68 | 66, 67 | eleq2s 2706 |
. 2
⊢ (𝑊 ∈ 𝑋 → (𝑁 ∈ ℕ0 → {( lastS
‘(𝑊 substr 〈0,
(𝑁 + 1)〉)), ( lastS
‘𝑊)} ∈ 𝐸)) |
69 | 68 | imp 444 |
1
⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → {( lastS
‘(𝑊 substr 〈0,
(𝑁 + 1)〉)), ( lastS
‘𝑊)} ∈ 𝐸) |