Step | Hyp | Ref
| Expression |
1 | | simpr1 1174 |
. . . 4
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈)))) → (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉)) |
2 | | simpr2 1175 |
. . . 4
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈)))) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
3 | | simpl 475 |
. . . 4
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈)))) → 𝑁 ≤ 𝑀) |
4 | | swrdsb0eq 13838 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝑁 ≤ 𝑀) → (𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉)) |
5 | 1, 2, 3, 4 | syl3anc 1351 |
. . 3
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈)))) → (𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉)) |
6 | | ral0 4333 |
. . . . . . 7
⊢
∀𝑖 ∈
∅ (𝑊‘𝑖) = (𝑈‘𝑖) |
7 | | nn0z 11816 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℤ) |
8 | | nn0z 11816 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
9 | | fzon 12871 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅)) |
10 | 7, 8, 9 | syl2an 586 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅)) |
11 | 10 | biimpa 469 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝑀) → (𝑀..^𝑁) = ∅) |
12 | 11 | raleqdv 3349 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝑀) → (∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖) ↔ ∀𝑖 ∈ ∅ (𝑊‘𝑖) = (𝑈‘𝑖))) |
13 | 6, 12 | mpbiri 250 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝑀) → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)) |
14 | 13 | ex 405 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ 𝑀 → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))) |
15 | 14 | 3ad2ant2 1114 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (𝑁 ≤ 𝑀 → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))) |
16 | 15 | impcom 399 |
. . 3
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈)))) → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)) |
17 | 5, 16 | 2thd 257 |
. 2
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈)))) → ((𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))) |
18 | | swrdcl 13806 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉) |
19 | | swrdcl 13806 |
. . . . . 6
⊢ (𝑈 ∈ Word 𝑉 → (𝑈 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉) |
20 | | eqwrd 13718 |
. . . . . 6
⊢ (((𝑊 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉 ∧ (𝑈 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉) → ((𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉) ↔ ((♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (♯‘(𝑈 substr 〈𝑀, 𝑁〉)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr 〈𝑀, 𝑁〉)))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗)))) |
21 | 18, 19, 20 | syl2an 586 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → ((𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉) ↔ ((♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (♯‘(𝑈 substr 〈𝑀, 𝑁〉)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr 〈𝑀, 𝑁〉)))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗)))) |
22 | 21 | 3ad2ant1 1113 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → ((𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉) ↔ ((♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (♯‘(𝑈 substr 〈𝑀, 𝑁〉)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr 〈𝑀, 𝑁〉)))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗)))) |
23 | 22 | adantl 474 |
. . 3
⊢ ((¬
𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈)))) → ((𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉) ↔ ((♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (♯‘(𝑈 substr 〈𝑀, 𝑁〉)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr 〈𝑀, 𝑁〉)))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗)))) |
24 | | swrdsbslen 13839 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (♯‘(𝑈 substr 〈𝑀, 𝑁〉))) |
25 | 24 | adantl 474 |
. . . 4
⊢ ((¬
𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈)))) →
(♯‘(𝑊 substr
〈𝑀, 𝑁〉)) = (♯‘(𝑈 substr 〈𝑀, 𝑁〉))) |
26 | 25 | biantrurd 525 |
. . 3
⊢ ((¬
𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈)))) → (∀𝑗 ∈
(0..^(♯‘(𝑊
substr 〈𝑀, 𝑁〉)))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ((♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (♯‘(𝑈 substr 〈𝑀, 𝑁〉)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr 〈𝑀, 𝑁〉)))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗)))) |
27 | | nn0re 11715 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
28 | | nn0re 11715 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
29 | | ltnle 10518 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀)) |
30 | | ltle 10527 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁)) |
31 | 29, 30 | sylbird 252 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬
𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁)) |
32 | 27, 28, 31 | syl2an 586 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁)) |
33 | 32 | 3ad2ant2 1114 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁)) |
34 | | simpl1l 1204 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑊 ∈ Word 𝑉) |
35 | | simpl2l 1206 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈
ℕ0) |
36 | 7, 8 | anim12i 603 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
37 | 36 | 3ad2ant2 1114 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
38 | 37 | anim1i 605 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁)) |
39 | | df-3an 1070 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁)) |
40 | 38, 39 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
41 | | eluz2 12062 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
42 | 40, 41 | sylibr 226 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈ (ℤ≥‘𝑀)) |
43 | 35, 42 | jca 504 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀))) |
44 | | simpl3l 1208 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ≤ (♯‘𝑊)) |
45 | 34, 43, 44 | 3jca 1108 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑊))) |
46 | | swrdlen2 13835 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑊)) → (♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (𝑁 − 𝑀)) |
47 | 45, 46 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (𝑁 − 𝑀)) |
48 | 47 | oveq2d 6990 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (0..^(♯‘(𝑊 substr 〈𝑀, 𝑁〉))) = (0..^(𝑁 − 𝑀))) |
49 | 48 | raleqdv 3349 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr 〈𝑀, 𝑁〉)))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗))) |
50 | | 0zd 11803 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → 0 ∈
ℤ) |
51 | | zsubcl 11835 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 − 𝑀) ∈ ℤ) |
52 | 8, 7, 51 | syl2anr 587 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 − 𝑀) ∈ ℤ) |
53 | 52 | 3ad2ant2 1114 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (𝑁 − 𝑀) ∈ ℤ) |
54 | 7 | adantr 473 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑀 ∈ ℤ) |
55 | 54 | 3ad2ant2 1114 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → 𝑀 ∈ ℤ) |
56 | | fzoshftral 12967 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ (𝑁
− 𝑀) ∈ ℤ
∧ 𝑀 ∈ ℤ)
→ (∀𝑗 ∈
(0..^(𝑁 − 𝑀))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗))) |
57 | 50, 53, 55, 56 | syl3anc 1351 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗))) |
58 | 57 | adantr 473 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗))) |
59 | | nn0cn 11716 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
60 | | nn0cn 11716 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) |
61 | | addid2 10621 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℂ → (0 +
𝑀) = 𝑀) |
62 | 61 | adantl 474 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (0 +
𝑀) = 𝑀) |
63 | | npcan 10694 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑁 − 𝑀) + 𝑀) = 𝑁) |
64 | 62, 63 | oveq12d 6992 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((0 +
𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁)) |
65 | 59, 60, 64 | syl2anr 587 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁)) |
66 | 65 | 3ad2ant2 1114 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁)) |
67 | 66 | adantr 473 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁)) |
68 | 67 | raleqdv 3349 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)[(𝑖 − 𝑀) / 𝑗]((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗))) |
69 | | ovex 7006 |
. . . . . . . . . . . 12
⊢ (𝑖 − 𝑀) ∈ V |
70 | | sbceqg 4241 |
. . . . . . . . . . . . 13
⊢ ((𝑖 − 𝑀) ∈ V → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗))) |
71 | | csbfv2g 6541 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑊 substr 〈𝑀, 𝑁〉)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗)) |
72 | | csbvarg 4261 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌𝑗 = (𝑖 − 𝑀)) |
73 | 72 | fveq2d 6500 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 − 𝑀) ∈ V → ((𝑊 substr 〈𝑀, 𝑁〉)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗) = ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀))) |
74 | 71, 73 | eqtrd 2808 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀))) |
75 | | csbfv2g 6541 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗)) |
76 | 72 | fveq2d 6500 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 − 𝑀) ∈ V → ((𝑈 substr 〈𝑀, 𝑁〉)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀))) |
77 | 75, 76 | eqtrd 2808 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀))) |
78 | 74, 77 | eqeq12d 2787 |
. . . . . . . . . . . . 13
⊢ ((𝑖 − 𝑀) ∈ V → (⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)) = ((𝑈 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)))) |
79 | 70, 78 | bitrd 271 |
. . . . . . . . . . . 12
⊢ ((𝑖 − 𝑀) ∈ V → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)) = ((𝑈 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)))) |
80 | 69, 79 | mp1i 13 |
. . . . . . . . . . 11
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)) = ((𝑈 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)))) |
81 | | swrdfv2 13836 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑊)) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)) = (𝑊‘𝑖)) |
82 | 45, 81 | sylan 572 |
. . . . . . . . . . . 12
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)) = (𝑊‘𝑖)) |
83 | | simpl1r 1205 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑈 ∈ Word 𝑉) |
84 | | simpl3r 1209 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ≤ (♯‘𝑈)) |
85 | 83, 43, 84 | 3jca 1108 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑈 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑈))) |
86 | | swrdfv2 13836 |
. . . . . . . . . . . . 13
⊢ (((𝑈 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑈)) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑈 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)) = (𝑈‘𝑖)) |
87 | 85, 86 | sylan 572 |
. . . . . . . . . . . 12
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑈 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)) = (𝑈‘𝑖)) |
88 | 82, 87 | eqeq12d 2787 |
. . . . . . . . . . 11
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → (((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)) = ((𝑈 substr 〈𝑀, 𝑁〉)‘(𝑖 − 𝑀)) ↔ (𝑊‘𝑖) = (𝑈‘𝑖))) |
89 | 80, 88 | bitrd 271 |
. . . . . . . . . 10
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ (𝑊‘𝑖) = (𝑈‘𝑖))) |
90 | 89 | ralbidva 3140 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑖 ∈ (𝑀..^𝑁)[(𝑖 − 𝑀) / 𝑗]((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))) |
91 | 68, 90 | bitrd 271 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))) |
92 | 58, 91 | bitrd 271 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))) |
93 | 49, 92 | bitrd 271 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr 〈𝑀, 𝑁〉)))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))) |
94 | 93 | ex 405 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (𝑀 ≤ 𝑁 → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr 〈𝑀, 𝑁〉)))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))) |
95 | 33, 94 | syld 47 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → (¬ 𝑁 ≤ 𝑀 → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr 〈𝑀, 𝑁〉)))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))) |
96 | 95 | impcom 399 |
. . 3
⊢ ((¬
𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈)))) → (∀𝑗 ∈
(0..^(♯‘(𝑊
substr 〈𝑀, 𝑁〉)))((𝑊 substr 〈𝑀, 𝑁〉)‘𝑗) = ((𝑈 substr 〈𝑀, 𝑁〉)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))) |
97 | 23, 26, 96 | 3bitr2d 299 |
. 2
⊢ ((¬
𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈)))) → ((𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))) |
98 | 17, 97 | pm2.61ian 799 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → ((𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))) |