Step | Hyp | Ref
| Expression |
1 | | clwwlknimp 26304 |
. . . . 5
⊢ (𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑋), (𝑋‘0)} ∈ ran 𝐸)) |
2 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) → 𝑋 ∈ Word 𝑉) |
3 | 2 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑋 ∈ Word 𝑉) |
4 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℕ) |
5 | 4 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 ∈
ℕ) |
6 | | eluz2 11569 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) |
7 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
8 | 7 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ∈
ℝ) |
9 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
10 | 7, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℕ → (𝑀 + 1) ∈
ℝ) |
11 | 10 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑀 + 1) ∈
ℝ) |
12 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
13 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑁 ∈
ℝ) |
14 | 8, 11, 13 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑀 ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
15 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
16 | 7 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℕ → 𝑀 ≤ (𝑀 + 1)) |
17 | 16 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ (𝑀 + 1)) |
18 | 17 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁)) |
19 | | letr 10010 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁) → 𝑀 ≤ 𝑁)) |
20 | 15, 18, 19 | sylc 63 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑀 + 1) ≤ 𝑁) → 𝑀 ≤ 𝑁) |
21 | 20 | expcom 450 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 + 1) ≤ 𝑁 → ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ≤ 𝑁)) |
22 | 21 | expd 451 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 + 1) ≤ 𝑁 → (𝑁 ∈ ℤ → (𝑀 ∈ ℕ → 𝑀 ≤ 𝑁))) |
23 | 22 | impcom 445 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 ∈ ℕ → 𝑀 ≤ 𝑁)) |
24 | 23 | 3adant1 1072 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 ∈ ℕ → 𝑀 ≤ 𝑁)) |
25 | 6, 24 | sylbi 206 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀 ∈ ℕ → 𝑀 ≤ 𝑁)) |
26 | 25 | impcom 445 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 ≤ 𝑁) |
27 | 26 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 ≤ 𝑁) |
28 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑋) = 𝑁 → (𝑀 ≤ (#‘𝑋) ↔ 𝑀 ≤ 𝑁)) |
29 | 28 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) → (𝑀 ≤ (#‘𝑋) ↔ 𝑀 ≤ 𝑁)) |
30 | 29 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑀 ≤ (#‘𝑋) ↔ 𝑀 ≤ 𝑁)) |
31 | 27, 30 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 ≤ (#‘𝑋)) |
32 | | swrdn0 13282 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑀 ∈ ℕ ∧ 𝑀 ≤ (#‘𝑋)) → (𝑋 substr 〈0, 𝑀〉) ≠ ∅) |
33 | 3, 5, 31, 32 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑋 substr 〈0, 𝑀〉) ≠
∅) |
34 | 33 | adantlr 747 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑋 substr 〈0, 𝑀〉) ≠
∅) |
35 | | swrdcl 13271 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ Word 𝑉 → (𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉) |
36 | 35 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) → (𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉) |
37 | 36 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉) |
38 | 37 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉) |
39 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
40 | | eluzp1m1 11587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
41 | 40 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℤ → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
42 | 39, 41 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
43 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
44 | 39, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℤ) |
45 | 7 | lem1d 10836 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ≤ 𝑀) |
46 | | eluzuzle 11572 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 − 1) ∈ ℤ ∧
(𝑀 − 1) ≤ 𝑀) → ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)))) |
47 | 44, 45, 46 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)))) |
48 | 42, 47 | syld 46 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)))) |
49 | 48 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1))) |
50 | | fzoss2 12365 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)) → (0..^(𝑀 − 1)) ⊆ (0..^(𝑁 − 1))) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (0..^(𝑀 − 1)) ⊆ (0..^(𝑁 − 1))) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (0..^(𝑀 − 1)) ⊆ (0..^(𝑁 − 1))) |
53 | | ssralv 3629 |
. . . . . . . . . . . . . 14
⊢
((0..^(𝑀 − 1))
⊆ (0..^(𝑁 − 1))
→ (∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑀 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑀 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸)) |
55 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → 𝑋 ∈ Word 𝑉) |
56 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑀 ∈ ℝ) |
57 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → (𝑀 + 1) ∈ ℝ) |
58 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → 𝑁 ∈ ℝ) |
59 | 58 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑁 ∈ ℝ) |
60 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑀 ≤ (𝑀 + 1)) |
61 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 + 1) ≤ 𝑁) |
62 | 61 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → (𝑀 + 1) ≤ 𝑁) |
63 | 56, 57, 59, 60, 62 | letrd 10073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑀 ≤ 𝑁) |
64 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑀 ∈
ℕ0) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈
ℕ0) |
67 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℤ) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈ ℤ) |
69 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 0 ∈
ℝ) |
70 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈
ℝ) |
71 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℝ) |
72 | 69, 70, 71 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (0
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 𝑁
∈ ℝ)) |
73 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → (0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
74 | 64 | nn0ge0d 11231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑀 ∈ ℕ → 0 ≤
𝑀) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 0 ≤
𝑀) |
76 | 75 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) |
77 | | letr 10010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 𝑁
∈ ℝ) → ((0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁) → 0 ≤ 𝑁)) |
78 | 73, 76, 77 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 0 ≤ 𝑁) |
79 | 68, 78 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁)) |
80 | | elnn0z 11267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℤ
∧ 0 ≤ 𝑁)) |
81 | 79, 80 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈
ℕ0) |
82 | 81 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 → 𝑁 ∈
ℕ0)) |
83 | 82 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈ ℤ → (𝑀 ∈ ℕ → (𝑀 ≤ 𝑁 → 𝑁 ∈
ℕ0))) |
84 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 ∈ ℕ → (𝑀 ≤ 𝑁 → 𝑁 ∈
ℕ0))) |
85 | 84 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → (𝑀 ≤ 𝑁 → 𝑁 ∈
ℕ0)) |
86 | 85 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈
ℕ0) |
87 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ 𝑁) |
88 | 66, 86, 87 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
89 | 63, 88 | mpdan 699 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
90 | 89 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 ∈ ℕ → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
91 | 90 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 ∈ ℕ → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
92 | 6, 91 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀 ∈ ℕ → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
93 | 92 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
94 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
95 | 93, 94 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ (0...𝑁)) |
96 | 95 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 ∈ (0...𝑁)) |
97 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑋) = 𝑁 → (0...(#‘𝑋)) = (0...𝑁)) |
98 | 97 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑋) = 𝑁 → (𝑀 ∈ (0...(#‘𝑋)) ↔ 𝑀 ∈ (0...𝑁))) |
99 | 98 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) → (𝑀 ∈ (0...(#‘𝑋)) ↔ 𝑀 ∈ (0...𝑁))) |
100 | 99 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑀 ∈ (0...(#‘𝑋)) ↔ 𝑀 ∈ (0...𝑁))) |
101 | 96, 100 | mpbird 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 ∈ (0...(#‘𝑋))) |
102 | 101 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → 𝑀 ∈ (0...(#‘𝑋))) |
103 | 44, 39, 45 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑀 ∈ ℕ → ((𝑀 − 1) ∈ ℤ ∧
𝑀 ∈ ℤ ∧
(𝑀 − 1) ≤ 𝑀)) |
104 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑀 ∈
(ℤ≥‘(𝑀 − 1)) ↔ ((𝑀 − 1) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑀 − 1) ≤ 𝑀)) |
105 | 103, 104 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
(ℤ≥‘(𝑀 − 1))) |
106 | | fzoss2 12365 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈
(ℤ≥‘(𝑀 − 1)) → (0..^(𝑀 − 1)) ⊆ (0..^𝑀)) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℕ →
(0..^(𝑀 − 1)) ⊆
(0..^𝑀)) |
108 | 107 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ → (𝑖 ∈ (0..^(𝑀 − 1)) → 𝑖 ∈ (0..^𝑀))) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑖 ∈ (0..^(𝑀 − 1)) → 𝑖 ∈ (0..^𝑀))) |
110 | 109 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑖 ∈ (0..^(𝑀 − 1)) → 𝑖 ∈ (0..^𝑀))) |
111 | 110 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → 𝑖 ∈ (0..^𝑀)) |
112 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑋)) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑋 substr 〈0, 𝑀〉)‘𝑖) = (𝑋‘𝑖)) |
113 | 55, 102, 111, 112 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → ((𝑋 substr 〈0, 𝑀〉)‘𝑖) = (𝑋‘𝑖)) |
114 | 113 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → (𝑋‘𝑖) = ((𝑋 substr 〈0, 𝑀〉)‘𝑖)) |
115 | | fzonn0p1p1 12413 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (0..^(𝑀 − 1)) → (𝑖 + 1) ∈ (0..^((𝑀 − 1) + 1))) |
116 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
117 | | npcan1 10334 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑀 ∈ ℕ → ((𝑀 − 1) + 1) = 𝑀) |
119 | 118 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℕ →
(0..^((𝑀 − 1) + 1)) =
(0..^𝑀)) |
120 | 119 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℕ → ((𝑖 + 1) ∈ (0..^((𝑀 − 1) + 1)) ↔ (𝑖 + 1) ∈ (0..^𝑀))) |
121 | 115, 120 | syl5ib 233 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ → (𝑖 ∈ (0..^(𝑀 − 1)) → (𝑖 + 1) ∈ (0..^𝑀))) |
122 | 121 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑖 ∈ (0..^(𝑀 − 1)) → (𝑖 + 1) ∈ (0..^𝑀))) |
123 | 122 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑖 ∈ (0..^(𝑀 − 1)) → (𝑖 + 1) ∈ (0..^𝑀))) |
124 | 123 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → (𝑖 + 1) ∈ (0..^𝑀)) |
125 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑋)) ∧ (𝑖 + 1) ∈ (0..^𝑀)) → ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1)) = (𝑋‘(𝑖 + 1))) |
126 | 55, 102, 124, 125 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1)) = (𝑋‘(𝑖 + 1))) |
127 | 126 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → (𝑋‘(𝑖 + 1)) = ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))) |
128 | 114, 127 | preq12d 4220 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → {(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} = {((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))}) |
129 | 128 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → ({(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
130 | 129 | ralbidva 2968 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (∀𝑖 ∈ (0..^(𝑀 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
131 | 54, 130 | sylibd 228 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
132 | 131 | impancom 455 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
133 | 132 | imp 444 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
134 | 3, 101 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑋 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑋)))) |
135 | 134 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑋 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑋)))) |
136 | | swrd0len 13274 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑋))) → (#‘(𝑋 substr 〈0, 𝑀〉)) = 𝑀) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (#‘(𝑋 substr 〈0, 𝑀〉)) = 𝑀) |
138 | 137 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → ((#‘(𝑋 substr 〈0, 𝑀〉)) − 1) = (𝑀 − 1)) |
139 | 138 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) →
(0..^((#‘(𝑋 substr
〈0, 𝑀〉)) −
1)) = (0..^(𝑀 −
1))) |
140 | 139 | raleqdv 3121 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
141 | 133, 140 | mpbird 246 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
142 | 34, 38, 141 | 3jca 1235 |
. . . . . . . 8
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → ((𝑋 substr 〈0, 𝑀〉) ≠ ∅ ∧
(𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
143 | 3, 101, 136 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (#‘(𝑋 substr 〈0, 𝑀〉)) = 𝑀) |
144 | 118 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑀 = ((𝑀 − 1) + 1)) |
145 | 144 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 = ((𝑀 − 1) + 1)) |
146 | 145 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 = ((𝑀 − 1) + 1)) |
147 | 143, 146 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)) |
148 | 147 | adantlr 747 |
. . . . . . . 8
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)) |
149 | 142, 148 | jca 553 |
. . . . . . 7
⊢ ((((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (((𝑋 substr 〈0, 𝑀〉) ≠ ∅ ∧
(𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1))) |
150 | 149 | ex 449 |
. . . . . 6
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (((𝑋 substr 〈0, 𝑀〉) ≠ ∅ ∧
(𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
151 | 150 | 3adant3 1074 |
. . . . 5
⊢ (((𝑋 ∈ Word 𝑉 ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑋), (𝑋‘0)} ∈ ran 𝐸) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (((𝑋 substr 〈0, 𝑀〉) ≠ ∅ ∧
(𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
152 | 1, 151 | syl 17 |
. . . 4
⊢ (𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (((𝑋 substr 〈0, 𝑀〉) ≠ ∅ ∧
(𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
153 | 152 | impcom 445 |
. . 3
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (((𝑋 substr 〈0, 𝑀〉) ≠ ∅ ∧ (𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1))) |
154 | | nnm1nn0 11211 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ0) |
155 | 154 | adantr 480 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑀 − 1) ∈
ℕ0) |
156 | | clwwlknprop 26300 |
. . . . . . . 8
⊢ (𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑋 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑋) = 𝑁))) |
157 | 156 | simp1d 1066 |
. . . . . . 7
⊢ (𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
158 | 155, 157 | anim12ci 589 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑀 − 1) ∈
ℕ0)) |
159 | | df-3an 1033 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑀 − 1) ∈
ℕ0) ↔ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑀 − 1) ∈
ℕ0)) |
160 | 158, 159 | sylibr 223 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑀 − 1) ∈
ℕ0)) |
161 | | iswwlkn 26212 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑀 − 1) ∈
ℕ0) → ((𝑋 substr 〈0, 𝑀〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑀 − 1)) ↔ ((𝑋 substr 〈0, 𝑀〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
162 | 160, 161 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ((𝑋 substr 〈0, 𝑀〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑀 − 1)) ↔ ((𝑋 substr 〈0, 𝑀〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
163 | | iswwlk 26211 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑋 substr 〈0, 𝑀〉) ∈ (𝑉 WWalks 𝐸) ↔ ((𝑋 substr 〈0, 𝑀〉) ≠ ∅ ∧ (𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
164 | 157, 163 | syl 17 |
. . . . . 6
⊢ (𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑋 substr 〈0, 𝑀〉) ∈ (𝑉 WWalks 𝐸) ↔ ((𝑋 substr 〈0, 𝑀〉) ≠ ∅ ∧ (𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
165 | 164 | adantl 481 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ((𝑋 substr 〈0, 𝑀〉) ∈ (𝑉 WWalks 𝐸) ↔ ((𝑋 substr 〈0, 𝑀〉) ≠ ∅ ∧ (𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
166 | 165 | anbi1d 737 |
. . . 4
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (((𝑋 substr 〈0, 𝑀〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)) ↔ (((𝑋 substr 〈0, 𝑀〉) ≠ ∅ ∧
(𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
167 | 162, 166 | bitrd 267 |
. . 3
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ((𝑋 substr 〈0, 𝑀〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑀 − 1)) ↔ (((𝑋 substr 〈0, 𝑀〉) ≠ ∅ ∧ (𝑋 substr 〈0, 𝑀〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
168 | 153, 167 | mpbird 246 |
. 2
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑋 substr 〈0, 𝑀〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑀 − 1))) |
169 | 168 | ex 449 |
1
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑋 substr 〈0, 𝑀〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑀 − 1)))) |