Proof of Theorem wwlksnextproplem1
Step | Hyp | Ref
| Expression |
1 | | wwlknbp2 41063 |
. . . . 5
⊢ (𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) |
2 | | 0zd 11266 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ ℤ) |
3 | | peano2nn0 11210 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
4 | 3 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) |
5 | 2, 4 | jca 553 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (0 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ)) |
6 | | 1z 11284 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
7 | 6 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℤ) |
8 | 7, 7 | jca 553 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (1 ∈ ℤ ∧ 1 ∈ ℤ)) |
9 | 5, 8 | jca 553 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ((0 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) ∧ (1 ∈
ℤ ∧ 1 ∈ ℤ))) |
10 | 9 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → ((0
∈ ℤ ∧ (𝑁 +
1) ∈ ℤ) ∧ (1 ∈ ℤ ∧ 1 ∈
ℤ))) |
11 | | fzssp1 12255 |
. . . . . . . . . . . 12
⊢
(0...𝑁) ⊆
(0...(𝑁 +
1)) |
12 | | nn0fz0 12306 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈ (0...𝑁)) |
13 | 12 | biimpi 205 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0...𝑁)) |
14 | 11, 13 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0...(𝑁 + 1))) |
15 | 14 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ (0...(𝑁 + 1))) |
16 | | elfz3 12222 |
. . . . . . . . . . 11
⊢ (1 ∈
ℤ → 1 ∈ (1...1)) |
17 | 6, 16 | mp1i 13 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 1 ∈
(1...1)) |
18 | 15, 17 | jca 553 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑁 ∈ (0...(𝑁 + 1)) ∧ 1 ∈
(1...1))) |
19 | | fzadd2 12247 |
. . . . . . . . 9
⊢ (((0
∈ ℤ ∧ (𝑁 +
1) ∈ ℤ) ∧ (1 ∈ ℤ ∧ 1 ∈ ℤ)) →
((𝑁 ∈ (0...(𝑁 + 1)) ∧ 1 ∈ (1...1))
→ (𝑁 + 1) ∈ ((0 +
1)...((𝑁 + 1) +
1)))) |
20 | 10, 18, 19 | sylc 63 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈ ((0 + 1)...((𝑁 + 1) + 1))) |
21 | | 1e0p1 11428 |
. . . . . . . . . 10
⊢ 1 = (0 +
1) |
22 | 21 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 1 = (0 +
1)) |
23 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
(#‘𝑊) = ((𝑁 + 1) + 1)) |
24 | 22, 23 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
(1...(#‘𝑊)) = ((0 +
1)...((𝑁 + 1) +
1))) |
25 | 20, 24 | eleqtrrd 2691 |
. . . . . . 7
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈ (1...(#‘𝑊))) |
26 | 25 | ex 449 |
. . . . . 6
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ (1...(#‘𝑊)))) |
27 | | simpl 472 |
. . . . . 6
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → 𝑊 ∈ Word (Vtx‘𝐺)) |
28 | 26, 27 | jctild 564 |
. . . . 5
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(#‘𝑊))))) |
29 | 1, 28 | syl 17 |
. . . 4
⊢ (𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(#‘𝑊))))) |
30 | | wwlksnextprop.x |
. . . 4
⊢ 𝑋 = ((𝑁 + 1) WWalkSN 𝐺) |
31 | 29, 30 | eleq2s 2706 |
. . 3
⊢ (𝑊 ∈ 𝑋 → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(#‘𝑊))))) |
32 | 31 | imp 444 |
. 2
⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(#‘𝑊)))) |
33 | | swrd0fv0 13292 |
. 2
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(#‘𝑊))) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑊‘0)) |
34 | 32, 33 | syl 17 |
1
⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑊‘0)) |