Proof of Theorem swrdsbslen
Step | Hyp | Ref
| Expression |
1 | | simpr1 1060 |
. . . 4
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈)))) → (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉)) |
2 | | simpr2 1061 |
. . . 4
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈)))) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
3 | | simpl 472 |
. . . 4
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈)))) → 𝑁 ≤ 𝑀) |
4 | | swrdsb0eq 13299 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝑁 ≤ 𝑀) → (𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉)) |
5 | 1, 2, 3, 4 | syl3anc 1318 |
. . 3
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈)))) → (𝑊 substr 〈𝑀, 𝑁〉) = (𝑈 substr 〈𝑀, 𝑁〉)) |
6 | 5 | fveq2d 6107 |
. 2
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈)))) → (#‘(𝑊 substr 〈𝑀, 𝑁〉)) = (#‘(𝑈 substr 〈𝑀, 𝑁〉))) |
7 | | nn0re 11178 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
8 | | nn0re 11178 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
9 | | ltnle 9996 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀)) |
10 | | ltle 10005 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁)) |
11 | 9, 10 | sylbird 249 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬
𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁)) |
12 | 7, 8, 11 | syl2an 493 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁)) |
13 | 12 | 3ad2ant2 1076 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁)) |
14 | | simpl1l 1105 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑊 ∈ Word 𝑉) |
15 | | simpl2l 1107 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈
ℕ0) |
16 | | nn0z 11277 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℤ) |
17 | | nn0z 11277 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
18 | 16, 17 | anim12i 588 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
19 | 18 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
20 | 19 | anim1i 590 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 ≤ 𝑁) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁)) |
21 | | df-3an 1033 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁)) |
22 | 20, 21 | sylibr 223 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
23 | | eluz2 11569 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
24 | 22, 23 | sylibr 223 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈ (ℤ≥‘𝑀)) |
25 | | simpl3l 1109 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ≤ (#‘𝑊)) |
26 | | swrdlen2 13297 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ 𝑁 ≤ (#‘𝑊)) → (#‘(𝑊 substr 〈𝑀, 𝑁〉)) = (𝑁 − 𝑀)) |
27 | 14, 15, 24, 25, 26 | syl121anc 1323 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (#‘(𝑊 substr 〈𝑀, 𝑁〉)) = (𝑁 − 𝑀)) |
28 | | simpl1r 1106 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑈 ∈ Word 𝑉) |
29 | | simpl3r 1110 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ≤ (#‘𝑈)) |
30 | | swrdlen2 13297 |
. . . . . . 7
⊢ ((𝑈 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ 𝑁 ≤ (#‘𝑈)) → (#‘(𝑈 substr 〈𝑀, 𝑁〉)) = (𝑁 − 𝑀)) |
31 | 28, 15, 24, 29, 30 | syl121anc 1323 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (#‘(𝑈 substr 〈𝑀, 𝑁〉)) = (𝑁 − 𝑀)) |
32 | 27, 31 | eqtr4d 2647 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (#‘(𝑊 substr 〈𝑀, 𝑁〉)) = (#‘(𝑈 substr 〈𝑀, 𝑁〉))) |
33 | 32 | ex 449 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (𝑀 ≤ 𝑁 → (#‘(𝑊 substr 〈𝑀, 𝑁〉)) = (#‘(𝑈 substr 〈𝑀, 𝑁〉)))) |
34 | 13, 33 | syld 46 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (¬ 𝑁 ≤ 𝑀 → (#‘(𝑊 substr 〈𝑀, 𝑁〉)) = (#‘(𝑈 substr 〈𝑀, 𝑁〉)))) |
35 | 34 | impcom 445 |
. 2
⊢ ((¬
𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈)))) → (#‘(𝑊 substr 〈𝑀, 𝑁〉)) = (#‘(𝑈 substr 〈𝑀, 𝑁〉))) |
36 | 6, 35 | pm2.61ian 827 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑁 ≤
(#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (#‘(𝑊 substr 〈𝑀, 𝑁〉)) = (#‘(𝑈 substr 〈𝑀, 𝑁〉))) |