Step | Hyp | Ref
| Expression |
1 | | peano2nn0 11333 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
2 | | iswwlksn 26730 |
. . 3
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (𝑊 ∈ (WWalks‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (𝑊 ∈ (WWalks‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)))) |
4 | | eqid 2622 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
5 | | eqid 2622 |
. . . . 5
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
6 | 4, 5 | iswwlks 26728 |
. . . 4
⊢ (𝑊 ∈ (WWalks‘𝐺) ↔ (𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
7 | | simp1 1061 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → 𝑊 ∈ Word (Vtx‘𝐺)) |
8 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
9 | 8 | 3ad2ant3 1084 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈
ℕ) |
10 | 1 | nn0red 11352 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
11 | 10 | lep1d 10955 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
12 | 11 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
13 | | breq2 4657 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ≤
(#‘𝑊) ↔ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
14 | 13 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 1) ≤ (#‘𝑊) ↔ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
15 | 12, 14 | mpbird 247 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ≤ (#‘𝑊)) |
16 | | swrdn0 13430 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ ℕ ∧ (𝑁 + 1) ≤ (#‘𝑊)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠ ∅) |
17 | 7, 9, 15, 16 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠
∅) |
18 | 17 | 3exp 1264 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠
∅))) |
19 | 18 | 3ad2ant2 1083 |
. . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠
∅))) |
20 | 19 | imp 445 |
. . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠
∅)) |
21 | 20 | impcom 446 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 substr 〈0, (𝑁 + 1)〉) ≠ ∅) |
22 | | swrdcl 13419 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word (Vtx‘𝐺)) |
23 | 22 | 3ad2ant2 1083 |
. . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word (Vtx‘𝐺)) |
24 | 23 | adantr 481 |
. . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word (Vtx‘𝐺)) |
25 | 24 | adantl 482 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word (Vtx‘𝐺)) |
26 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
((#‘𝑊) − 1) =
(((𝑁 + 1) + 1) −
1)) |
27 | 1 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
28 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
29 | 27, 28 | pncand 10393 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) |
30 | 26, 29 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ ((#‘𝑊) −
1) = (𝑁 +
1)) |
31 | 30 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (0..^((#‘𝑊)
− 1)) = (0..^(𝑁 +
1))) |
32 | 31 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
33 | 32 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
34 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
35 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) |
36 | 1, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) |
37 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
38 | 37 | lep1d 10955 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ≤ (𝑁 + 1)) |
39 | 34, 36, 38 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ∈ ℤ
∧ (𝑁 + 1) ∈
ℤ ∧ 𝑁 ≤ (𝑁 + 1))) |
40 | 39 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑁 ≤ (𝑁 + 1))) |
41 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑁 ≤ (𝑁 + 1))) |
42 | 40, 41 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
43 | | fzoss2 12496 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(𝑁 + 1))) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^𝑁) ⊆ (0..^(𝑁 + 1))) |
45 | | ssralv 3666 |
. . . . . . . . . . . . . . . . . . 19
⊢
((0..^𝑁) ⊆
(0..^(𝑁 + 1)) →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
47 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → 𝑊 ∈ Word (Vtx‘𝐺)) |
48 | 47 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑊 ∈ Word (Vtx‘𝐺)) |
49 | | nn0fz0 12437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 + 1) ∈ ℕ0
↔ (𝑁 + 1) ∈
(0...(𝑁 +
1))) |
50 | 1, 49 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(0...(𝑁 +
1))) |
51 | 50 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈ (0...(𝑁 + 1))) |
52 | | fzelp1 12393 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 + 1) ∈ (0...(𝑁 + 1)) → (𝑁 + 1) ∈ (0...((𝑁 + 1) + 1))) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈ (0...((𝑁 + 1) + 1))) |
54 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
(0...(#‘𝑊)) =
(0...((𝑁 + 1) +
1))) |
55 | 54 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ∈
(0...(#‘𝑊)) ↔
(𝑁 + 1) ∈ (0...((𝑁 + 1) + 1)))) |
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ ((𝑁 + 1) ∈
(0...(#‘𝑊)) ↔
(𝑁 + 1) ∈ (0...((𝑁 + 1) + 1)))) |
57 | 56 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → ((𝑁 + 1) ∈ (0...(#‘𝑊)) ↔ (𝑁 + 1) ∈ (0...((𝑁 + 1) + 1)))) |
58 | 53, 57 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈ (0...(#‘𝑊))) |
59 | 58 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑁 + 1) ∈ (0...(#‘𝑊))) |
60 | | fzossfzop1 12545 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ (0..^𝑁) ⊆
(0..^(𝑁 +
1))) |
61 | 60 | sseld 3602 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))) |
62 | 61 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))) |
63 | 62 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1))) |
64 | | swrd0fv 13439 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)) ∧ 𝑖 ∈ (0..^(𝑁 + 1))) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖) = (𝑊‘𝑖)) |
65 | 48, 59, 63, 64 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖) = (𝑊‘𝑖)) |
66 | 65 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊‘𝑖) = ((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖)) |
67 | | fzofzp1 12565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0...𝑁)) |
68 | 67 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0...𝑁)) |
69 | | fzval3 12536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℤ →
(0...𝑁) = (0..^(𝑁 + 1))) |
70 | 69 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℤ →
(0..^(𝑁 + 1)) = (0...𝑁)) |
71 | 34, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ (0..^(𝑁 + 1)) =
(0...𝑁)) |
72 | 71 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ ((𝑖 + 1) ∈
(0..^(𝑁 + 1)) ↔ (𝑖 + 1) ∈ (0...𝑁))) |
73 | 72 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → ((𝑖 + 1) ∈ (0..^(𝑁 + 1)) ↔ (𝑖 + 1) ∈ (0...𝑁))) |
74 | 73 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑖 + 1) ∈ (0..^(𝑁 + 1)) ↔ (𝑖 + 1) ∈ (0...𝑁))) |
75 | 68, 74 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) |
76 | | swrd0fv 13439 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)) ∧ (𝑖 + 1) ∈ (0..^(𝑁 + 1))) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
77 | 48, 59, 75, 76 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
78 | 77 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊‘(𝑖 + 1)) = ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))) |
79 | 66, 78 | preq12d 4276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))}) |
80 | 79 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
81 | 80 | biimpd 219 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
82 | 81 | ralimdva 2962 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^𝑁){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
83 | 46, 82 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^𝑁){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
84 | 33, 83 | sylbid 230 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^𝑁){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
85 | 84 | imp 445 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^𝑁){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
86 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
87 | 86, 28 | pncand 10393 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
88 | 87 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (0..^((𝑁 + 1)
− 1)) = (0..^𝑁)) |
89 | 88 | ad2antll 765 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^((𝑁 + 1) − 1)) =
(0..^𝑁)) |
90 | 89 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (0..^((𝑁 + 1) − 1)) = (0..^𝑁)) |
91 | 90 | raleqdv 3144 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
92 | 85, 91 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
93 | 1 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈
ℕ0) |
94 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (#‘𝑊) =
((𝑁 + 1) +
1)) |
95 | 94 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(#‘𝑊) = ((𝑁 + 1) + 1)) |
96 | | swrd0len0 13436 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ ℕ0 ∧
(#‘𝑊) = ((𝑁 + 1) + 1)) →
(#‘(𝑊 substr 〈0,
(𝑁 + 1)〉)) = (𝑁 + 1)) |
97 | 47, 93, 95, 96 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(#‘(𝑊 substr 〈0,
(𝑁 + 1)〉)) = (𝑁 + 1)) |
98 | 97 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1) = ((𝑁 + 1)
− 1)) |
99 | 98 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)) = (0..^((𝑁 + 1)
− 1))) |
100 | 99 | raleqdv 3144 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
101 | 100 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
102 | 92, 101 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
103 | 102 | exp31 630 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) − 1)){((𝑊 substr 〈0, (𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
104 | 103 | com23 86 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
105 | 104 | imp 445 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
106 | 105 | 3adant1 1079 |
. . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
107 | 106 | expdimp 453 |
. . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 →
∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
108 | 107 | impcom 446 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → ∀𝑖 ∈ (0..^((#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) −
1)){((𝑊 substr 〈0,
(𝑁 + 1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
109 | 4, 5 | iswwlks 26728 |
. . . . . . 7
⊢ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈
(WWalks‘𝐺) ↔
((𝑊 substr 〈0, (𝑁 + 1)〉) ≠ ∅ ∧
(𝑊 substr 〈0, (𝑁 + 1)〉) ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘(𝑊 substr
〈0, (𝑁 + 1)〉))
− 1)){((𝑊 substr
〈0, (𝑁 +
1)〉)‘𝑖), ((𝑊 substr 〈0, (𝑁 + 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
110 | 21, 25, 108, 109 | syl3anbrc 1246 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (WWalks‘𝐺)) |
111 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
112 | 1, 111 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
113 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 + 1) ∈ (0...((𝑁 + 1) + 1)) ↔ ((𝑁 + 1) ∈ ℕ0
∧ ((𝑁 + 1) + 1) ∈
ℕ0 ∧ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
114 | 1, 112, 11, 113 | syl3anbrc 1246 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1))) |
115 | 114 | adantl 482 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1))) |
116 | 115, 56 | mpbird 247 |
. . . . . . . . . . . 12
⊢
(((#‘𝑊) =
((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(0...(#‘𝑊))) |
117 | 116 | anim2i 593 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((#‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)))) |
118 | 117 | exp32 631 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)))))) |
119 | 118 | 3ad2ant2 1083 |
. . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((#‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)))))) |
120 | 119 | imp 445 |
. . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(#‘𝑊))))) |
121 | 120 | impcom 446 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(#‘𝑊)))) |
122 | | swrd0len 13422 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(#‘𝑊))) → (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)) |
123 | 121, 122 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)) |
124 | | iswwlksn 26730 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((𝑊 substr 〈0,
(𝑁 + 1)〉) ∈
(𝑁 WWalksN 𝐺) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (WWalks‘𝐺) ∧ (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)))) |
125 | 124 | adantr 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑁 WWalksN 𝐺) ↔ ((𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (WWalks‘𝐺) ∧ (#‘(𝑊 substr 〈0, (𝑁 + 1)〉)) = (𝑁 + 1)))) |
126 | 110, 123,
125 | mpbir2and 957 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑁 WWalksN 𝐺)) |
127 | 126 | expcom 451 |
. . . 4
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑁 WWalksN 𝐺))) |
128 | 6, 127 | sylanb 489 |
. . 3
⊢ ((𝑊 ∈ (WWalks‘𝐺) ∧ (#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑁 WWalksN 𝐺))) |
129 | 128 | com12 32 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((𝑊 ∈
(WWalks‘𝐺) ∧
(#‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑁 WWalksN 𝐺))) |
130 | 3, 129 | sylbid 230 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑁 WWalksN 𝐺))) |