| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) | 
| 2 |  | eqid 2737 | . . . . . 6
⊢
(Edg‘𝐺) =
(Edg‘𝐺) | 
| 3 | 1, 2 | clwwlknp 30056 | . . . . 5
⊢ (𝑋 ∈ (𝑁 ClWWalksN 𝐺) → ((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑋), (𝑋‘0)} ∈ (Edg‘𝐺))) | 
| 4 |  | pfxcl 14715 | . . . . . . . . . 10
⊢ (𝑋 ∈ Word (Vtx‘𝐺) → (𝑋 prefix 𝑀) ∈ Word (Vtx‘𝐺)) | 
| 5 | 4 | adantr 480 | . . . . . . . . 9
⊢ ((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) → (𝑋 prefix 𝑀) ∈ Word (Vtx‘𝐺)) | 
| 6 | 5 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑋 prefix 𝑀) ∈ Word (Vtx‘𝐺)) | 
| 7 |  | nnz 12634 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) | 
| 8 |  | eluzp1m1 12904 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) | 
| 9 | 8 | ex 412 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℤ → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑀))) | 
| 10 | 7, 9 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑀))) | 
| 11 |  | peano2zm 12660 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) | 
| 12 | 7, 11 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℤ) | 
| 13 |  | nnre 12273 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) | 
| 14 | 13 | lem1d 12201 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ≤ 𝑀) | 
| 15 |  | eluzuzle 12887 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 − 1) ∈ ℤ ∧
(𝑀 − 1) ≤ 𝑀) → ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)))) | 
| 16 | 12, 14, 15 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)))) | 
| 17 | 10, 16 | syld 47 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)))) | 
| 18 | 17 | imp 406 | . . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1))) | 
| 19 |  | fzoss2 13727 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)) → (0..^(𝑀 − 1)) ⊆ (0..^(𝑁 − 1))) | 
| 20 | 18, 19 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (0..^(𝑀 − 1)) ⊆ (0..^(𝑁 − 1))) | 
| 21 | 20 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (0..^(𝑀 − 1)) ⊆ (0..^(𝑁 − 1))) | 
| 22 |  | ssralv 4052 | . . . . . . . . . . . . 13
⊢
((0..^(𝑀 − 1))
⊆ (0..^(𝑁 − 1))
→ (∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑀 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 23 | 21, 22 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑀 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 24 |  | simpll 767 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑋 ∈ Word (Vtx‘𝐺)) | 
| 25 | 24 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → 𝑋 ∈ Word (Vtx‘𝐺)) | 
| 26 |  | eluz2 12884 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) | 
| 27 | 13 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑀 ∈ ℝ) | 
| 28 |  | peano2re 11434 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) | 
| 29 | 13, 28 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑀 ∈ ℕ → (𝑀 + 1) ∈
ℝ) | 
| 30 | 29 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → (𝑀 + 1) ∈ ℝ) | 
| 31 |  | zre 12617 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) | 
| 32 | 31 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑁 ∈ ℝ) | 
| 33 | 13 | lep1d 12199 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑀 ∈ ℕ → 𝑀 ≤ (𝑀 + 1)) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑀 ≤ (𝑀 + 1)) | 
| 35 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 + 1) ≤ 𝑁) | 
| 36 | 35 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → (𝑀 + 1) ≤ 𝑁) | 
| 37 | 27, 30, 32, 34, 36 | letrd 11418 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑀 ≤ 𝑁) | 
| 38 |  | nnnn0 12533 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) | 
| 39 | 38 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈
ℕ0) | 
| 40 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℤ) | 
| 41 | 40 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈ ℤ) | 
| 42 |  | 0red 11264 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 0 ∈
ℝ) | 
| 43 | 13 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈
ℝ) | 
| 44 | 31 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℝ) | 
| 45 | 42, 43, 44 | 3jca 1129 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (0
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 𝑁
∈ ℝ)) | 
| 46 | 45 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → (0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈
ℝ)) | 
| 47 | 38 | nn0ge0d 12590 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑀 ∈ ℕ → 0 ≤
𝑀) | 
| 48 | 47 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 0 ≤
𝑀) | 
| 49 | 48 | anim1i 615 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) | 
| 50 |  | letr 11355 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 𝑁
∈ ℝ) → ((0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁) → 0 ≤ 𝑁)) | 
| 51 | 46, 49, 50 | sylc 65 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 0 ≤ 𝑁) | 
| 52 |  | elnn0z 12626 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℤ
∧ 0 ≤ 𝑁)) | 
| 53 | 41, 51, 52 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈
ℕ0) | 
| 54 | 53 | adantlrr 721 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈
ℕ0) | 
| 55 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ 𝑁) | 
| 56 | 39, 54, 55 | 3jca 1129 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) | 
| 57 | 37, 56 | mpdan 687 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) | 
| 58 | 57 | expcom 413 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 ∈ ℕ → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) | 
| 59 | 58 | 3adant1 1131 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 ∈ ℕ → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) | 
| 60 | 26, 59 | sylbi 217 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀 ∈ ℕ → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) | 
| 61 | 60 | impcom 407 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) | 
| 62 |  | elfz2nn0 13658 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) | 
| 63 | 61, 62 | sylibr 234 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ (0...𝑁)) | 
| 64 | 63 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 ∈ (0...𝑁)) | 
| 65 |  | oveq2 7439 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑋) =
𝑁 →
(0...(♯‘𝑋)) =
(0...𝑁)) | 
| 66 | 65 | eleq2d 2827 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑋) =
𝑁 → (𝑀 ∈ (0...(♯‘𝑋)) ↔ 𝑀 ∈ (0...𝑁))) | 
| 67 | 66 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) → (𝑀 ∈ (0...(♯‘𝑋)) ↔ 𝑀 ∈ (0...𝑁))) | 
| 68 | 67 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑀 ∈
(0...(♯‘𝑋))
↔ 𝑀 ∈ (0...𝑁))) | 
| 69 | 64, 68 | mpbird 257 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 ∈
(0...(♯‘𝑋))) | 
| 70 | 69 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → 𝑀 ∈ (0...(♯‘𝑋))) | 
| 71 |  | eluz2 12884 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈
(ℤ≥‘(𝑀 − 1)) ↔ ((𝑀 − 1) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑀 − 1) ≤ 𝑀)) | 
| 72 | 12, 7, 14, 71 | syl3anbrc 1344 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
(ℤ≥‘(𝑀 − 1))) | 
| 73 |  | fzoss2 13727 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈
(ℤ≥‘(𝑀 − 1)) → (0..^(𝑀 − 1)) ⊆ (0..^𝑀)) | 
| 74 | 72, 73 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ →
(0..^(𝑀 − 1)) ⊆
(0..^𝑀)) | 
| 75 | 74 | sseld 3982 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → (𝑖 ∈ (0..^(𝑀 − 1)) → 𝑖 ∈ (0..^𝑀))) | 
| 76 | 75 | ad2antrl 728 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑖 ∈ (0..^(𝑀 − 1)) → 𝑖 ∈ (0..^𝑀))) | 
| 77 | 76 | imp 406 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → 𝑖 ∈ (0..^𝑀)) | 
| 78 |  | pfxfv 14720 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ Word (Vtx‘𝐺) ∧ 𝑀 ∈ (0...(♯‘𝑋)) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑋 prefix 𝑀)‘𝑖) = (𝑋‘𝑖)) | 
| 79 | 25, 70, 77, 78 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → ((𝑋 prefix 𝑀)‘𝑖) = (𝑋‘𝑖)) | 
| 80 | 79 | eqcomd 2743 | . . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → (𝑋‘𝑖) = ((𝑋 prefix 𝑀)‘𝑖)) | 
| 81 |  | fzonn0p1p1 13783 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^(𝑀 − 1)) → (𝑖 + 1) ∈ (0..^((𝑀 − 1) + 1))) | 
| 82 |  | nncn 12274 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) | 
| 83 |  | npcan1 11688 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀) | 
| 84 | 82, 83 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℕ → ((𝑀 − 1) + 1) = 𝑀) | 
| 85 | 84 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ →
(0..^((𝑀 − 1) + 1)) =
(0..^𝑀)) | 
| 86 | 85 | eleq2d 2827 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ → ((𝑖 + 1) ∈ (0..^((𝑀 − 1) + 1)) ↔ (𝑖 + 1) ∈ (0..^𝑀))) | 
| 87 | 81, 86 | imbitrid 244 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → (𝑖 ∈ (0..^(𝑀 − 1)) → (𝑖 + 1) ∈ (0..^𝑀))) | 
| 88 | 87 | ad2antrl 728 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑖 ∈ (0..^(𝑀 − 1)) → (𝑖 + 1) ∈ (0..^𝑀))) | 
| 89 | 88 | imp 406 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → (𝑖 + 1) ∈ (0..^𝑀)) | 
| 90 |  | pfxfv 14720 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ Word (Vtx‘𝐺) ∧ 𝑀 ∈ (0...(♯‘𝑋)) ∧ (𝑖 + 1) ∈ (0..^𝑀)) → ((𝑋 prefix 𝑀)‘(𝑖 + 1)) = (𝑋‘(𝑖 + 1))) | 
| 91 | 25, 70, 89, 90 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → ((𝑋 prefix 𝑀)‘(𝑖 + 1)) = (𝑋‘(𝑖 + 1))) | 
| 92 | 91 | eqcomd 2743 | . . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → (𝑋‘(𝑖 + 1)) = ((𝑋 prefix 𝑀)‘(𝑖 + 1))) | 
| 93 | 80, 92 | preq12d 4741 | . . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → {(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} = {((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))}) | 
| 94 | 93 | eleq1d 2826 | . . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → ({(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 95 | 94 | ralbidva 3176 | . . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (∀𝑖 ∈ (0..^(𝑀 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 96 | 23, 95 | sylibd 239 | . . . . . . . . . . 11
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 97 | 96 | impancom 451 | . . . . . . . . . 10
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 98 | 97 | imp 406 | . . . . . . . . 9
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) | 
| 99 | 24, 69 | jca 511 | . . . . . . . . . . . . 13
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑋 ∈ Word (Vtx‘𝐺) ∧ 𝑀 ∈ (0...(♯‘𝑋)))) | 
| 100 | 99 | adantlr 715 | . . . . . . . . . . . 12
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑋 ∈ Word (Vtx‘𝐺) ∧ 𝑀 ∈ (0...(♯‘𝑋)))) | 
| 101 |  | pfxlen 14721 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ Word (Vtx‘𝐺) ∧ 𝑀 ∈ (0...(♯‘𝑋))) → (♯‘(𝑋 prefix 𝑀)) = 𝑀) | 
| 102 | 100, 101 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) →
(♯‘(𝑋 prefix
𝑀)) = 𝑀) | 
| 103 | 102 | oveq1d 7446 | . . . . . . . . . 10
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) →
((♯‘(𝑋 prefix
𝑀)) − 1) = (𝑀 − 1)) | 
| 104 | 103 | oveq2d 7447 | . . . . . . . . 9
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) →
(0..^((♯‘(𝑋
prefix 𝑀)) − 1)) =
(0..^(𝑀 −
1))) | 
| 105 | 98, 104 | raleqtrrdv 3330 | . . . . . . . 8
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → ∀𝑖 ∈
(0..^((♯‘(𝑋
prefix 𝑀)) −
1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) | 
| 106 | 24, 69, 101 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) →
(♯‘(𝑋 prefix
𝑀)) = 𝑀) | 
| 107 | 84 | eqcomd 2743 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 = ((𝑀 − 1) + 1)) | 
| 108 | 107 | ad2antrl 728 | . . . . . . . . . 10
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 = ((𝑀 − 1) + 1)) | 
| 109 | 106, 108 | eqtrd 2777 | . . . . . . . . 9
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) →
(♯‘(𝑋 prefix
𝑀)) = ((𝑀 − 1) + 1)) | 
| 110 | 109 | adantlr 715 | . . . . . . . 8
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) →
(♯‘(𝑋 prefix
𝑀)) = ((𝑀 − 1) + 1)) | 
| 111 | 6, 105, 110 | 3jca 1129 | . . . . . . 7
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → ((𝑋 prefix 𝑀) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑋 prefix 𝑀)) − 1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (♯‘(𝑋 prefix 𝑀)) = ((𝑀 − 1) + 1))) | 
| 112 | 111 | ex 412 | . . . . . 6
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑋 prefix 𝑀) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑋 prefix 𝑀)) − 1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (♯‘(𝑋 prefix 𝑀)) = ((𝑀 − 1) + 1)))) | 
| 113 | 112 | 3adant3 1133 | . . . . 5
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑋), (𝑋‘0)} ∈ (Edg‘𝐺)) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑋 prefix 𝑀) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑋 prefix 𝑀)) − 1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (♯‘(𝑋 prefix 𝑀)) = ((𝑀 − 1) + 1)))) | 
| 114 | 3, 113 | syl 17 | . . . 4
⊢ (𝑋 ∈ (𝑁 ClWWalksN 𝐺) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑋 prefix 𝑀) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑋 prefix 𝑀)) − 1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (♯‘(𝑋 prefix 𝑀)) = ((𝑀 − 1) + 1)))) | 
| 115 | 114 | impcom 407 | . . 3
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ (𝑁 ClWWalksN 𝐺)) → ((𝑋 prefix 𝑀) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑋 prefix 𝑀)) − 1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (♯‘(𝑋 prefix 𝑀)) = ((𝑀 − 1) + 1))) | 
| 116 |  | nnm1nn0 12567 | . . . . 5
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ0) | 
| 117 | 116 | ad2antrr 726 | . . . 4
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ (𝑁 ClWWalksN 𝐺)) → (𝑀 − 1) ∈
ℕ0) | 
| 118 | 1, 2 | iswwlksnx 29860 | . . . 4
⊢ ((𝑀 − 1) ∈
ℕ0 → ((𝑋 prefix 𝑀) ∈ ((𝑀 − 1) WWalksN 𝐺) ↔ ((𝑋 prefix 𝑀) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑋 prefix 𝑀)) − 1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (♯‘(𝑋 prefix 𝑀)) = ((𝑀 − 1) + 1)))) | 
| 119 | 117, 118 | syl 17 | . . 3
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ (𝑁 ClWWalksN 𝐺)) → ((𝑋 prefix 𝑀) ∈ ((𝑀 − 1) WWalksN 𝐺) ↔ ((𝑋 prefix 𝑀) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑋 prefix 𝑀)) − 1)){((𝑋 prefix 𝑀)‘𝑖), ((𝑋 prefix 𝑀)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (♯‘(𝑋 prefix 𝑀)) = ((𝑀 − 1) + 1)))) | 
| 120 | 115, 119 | mpbird 257 | . 2
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ (𝑁 ClWWalksN 𝐺)) → (𝑋 prefix 𝑀) ∈ ((𝑀 − 1) WWalksN 𝐺)) | 
| 121 | 120 | ex 412 | 1
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑋 ∈ (𝑁 ClWWalksN 𝐺) → (𝑋 prefix 𝑀) ∈ ((𝑀 − 1) WWalksN 𝐺))) |