Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . . 7
⊢
((#‘𝐴) = 0
→ (0...(#‘𝐴)) =
(0...0)) |
2 | 1 | eleq2d 2687 |
. . . . . 6
⊢
((#‘𝐴) = 0
→ (𝑁 ∈
(0...(#‘𝐴)) ↔
𝑁 ∈
(0...0))) |
3 | | elfz1eq 12352 |
. . . . . . 7
⊢ (𝑁 ∈ (0...0) → 𝑁 = 0) |
4 | | elfz1eq 12352 |
. . . . . . . . 9
⊢ (𝑀 ∈ (0...0) → 𝑀 = 0) |
5 | | swrd00 13418 |
. . . . . . . . . . 11
⊢ ((𝐴 ++ 𝐵) substr 〈0, 0〉) =
∅ |
6 | | swrd00 13418 |
. . . . . . . . . . 11
⊢ (𝐴 substr 〈0, 0〉) =
∅ |
7 | 5, 6 | eqtr4i 2647 |
. . . . . . . . . 10
⊢ ((𝐴 ++ 𝐵) substr 〈0, 0〉) = (𝐴 substr 〈0,
0〉) |
8 | | opeq1 4402 |
. . . . . . . . . . 11
⊢ (𝑀 = 0 → 〈𝑀, 0〉 = 〈0,
0〉) |
9 | 8 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑀 = 0 → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = ((𝐴 ++ 𝐵) substr 〈0, 0〉)) |
10 | 8 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑀 = 0 → (𝐴 substr 〈𝑀, 0〉) = (𝐴 substr 〈0, 0〉)) |
11 | 7, 9, 10 | 3eqtr4a 2682 |
. . . . . . . . 9
⊢ (𝑀 = 0 → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉)) |
12 | 4, 11 | syl 17 |
. . . . . . . 8
⊢ (𝑀 ∈ (0...0) → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉)) |
13 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑁 = 0 → (0...𝑁) = (0...0)) |
14 | 13 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝑁 = 0 → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ∈ (0...0))) |
15 | | opeq2 4403 |
. . . . . . . . . . 11
⊢ (𝑁 = 0 → 〈𝑀, 𝑁〉 = 〈𝑀, 0〉) |
16 | 15 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑁 = 0 → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉)) |
17 | 15 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑁 = 0 → (𝐴 substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 0〉)) |
18 | 16, 17 | eqeq12d 2637 |
. . . . . . . . 9
⊢ (𝑁 = 0 → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉) ↔ ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉))) |
19 | 14, 18 | imbi12d 334 |
. . . . . . . 8
⊢ (𝑁 = 0 → ((𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)) ↔ (𝑀 ∈ (0...0) → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉)))) |
20 | 12, 19 | mpbiri 248 |
. . . . . . 7
⊢ (𝑁 = 0 → (𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
21 | 3, 20 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ (0...0) → (𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
22 | 2, 21 | syl6bi 243 |
. . . . 5
⊢
((#‘𝐴) = 0
→ (𝑁 ∈
(0...(#‘𝐴)) →
(𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)))) |
23 | 22 | com23 86 |
. . . 4
⊢
((#‘𝐴) = 0
→ (𝑀 ∈ (0...𝑁) → (𝑁 ∈ (0...(#‘𝐴)) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)))) |
24 | 23 | impd 447 |
. . 3
⊢
((#‘𝐴) = 0
→ ((𝑀 ∈
(0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
25 | 24 | a1d 25 |
. 2
⊢
((#‘𝐴) = 0
→ ((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)))) |
26 | | ccatcl 13359 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
27 | 26 | adantl 482 |
. . . . . . 7
⊢ ((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
28 | 27 | adantr 481 |
. . . . . 6
⊢ (((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
29 | | simprl 794 |
. . . . . 6
⊢ (((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → 𝑀 ∈ (0...𝑁)) |
30 | | elfzelfzccat 13364 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(#‘𝐴)) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))))) |
31 | 30 | adantl 482 |
. . . . . . . . 9
⊢ ((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → (𝑁 ∈ (0...(#‘𝐴)) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))))) |
32 | 31 | com12 32 |
. . . . . . . 8
⊢ (𝑁 ∈ (0...(#‘𝐴)) → ((¬ (#‘𝐴) = 0 ∧ (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))))) |
33 | 32 | adantl 482 |
. . . . . . 7
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) → ((¬ (#‘𝐴) = 0 ∧ (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))))) |
34 | 33 | impcom 446 |
. . . . . 6
⊢ (((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵)))) |
35 | | swrdvalfn 13426 |
. . . . . 6
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
36 | 28, 29, 34, 35 | syl3anc 1326 |
. . . . 5
⊢ (((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
37 | | 3anass 1042 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) ↔ (𝐴 ∈ Word 𝑉 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))))) |
38 | 37 | simplbi2 655 |
. . . . . . . 8
⊢ (𝐴 ∈ Word 𝑉 → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))))) |
39 | 38 | ad2antrl 764 |
. . . . . . 7
⊢ ((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))))) |
40 | 39 | imp 445 |
. . . . . 6
⊢ (((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) |
41 | | swrdvalfn 13426 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) → (𝐴 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
42 | 40, 41 | syl 17 |
. . . . 5
⊢ (((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → (𝐴 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
43 | | simprl 794 |
. . . . . . . 8
⊢ ((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → 𝐴 ∈ Word 𝑉) |
44 | 43 | ad2antrr 762 |
. . . . . . 7
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝐴 ∈ Word 𝑉) |
45 | | simprr 796 |
. . . . . . . 8
⊢ ((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → 𝐵 ∈ Word 𝑉) |
46 | 45 | ad2antrr 762 |
. . . . . . 7
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝐵 ∈ Word 𝑉) |
47 | | elfzo0 12508 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0..^(𝑁 − 𝑀)) ↔ (𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀))) |
48 | | elfz2nn0 12431 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
49 | | nn0addcl 11328 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑘 + 𝑀) ∈
ℕ0) |
50 | 49 | expcom 451 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ0
→ (𝑘 ∈
ℕ0 → (𝑘 + 𝑀) ∈
ℕ0)) |
51 | 50 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑀
≤ 𝑁) → (𝑘 ∈ ℕ0
→ (𝑘 + 𝑀) ∈
ℕ0)) |
52 | 48, 51 | sylbi 207 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (0...𝑁) → (𝑘 ∈ ℕ0 → (𝑘 + 𝑀) ∈
ℕ0)) |
53 | 52 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ (((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → (𝑘 ∈ ℕ0 → (𝑘 + 𝑀) ∈
ℕ0)) |
54 | 53 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (((¬ (#‘𝐴)
= 0 ∧ (𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → (𝑘 + 𝑀) ∈
ℕ0)) |
55 | 54 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (((¬ (#‘𝐴) = 0 ∧ (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → (𝑘 + 𝑀) ∈
ℕ0)) |
56 | 47, 55 | sylbi 207 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0..^(𝑁 − 𝑀)) → (((¬ (#‘𝐴) = 0 ∧ (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → (𝑘 + 𝑀) ∈
ℕ0)) |
57 | 56 | impcom 446 |
. . . . . . . 8
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝑘 + 𝑀) ∈
ℕ0) |
58 | | lencl 13324 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈
ℕ0) |
59 | | df-ne 2795 |
. . . . . . . . . . . . 13
⊢
((#‘𝐴) ≠ 0
↔ ¬ (#‘𝐴) =
0) |
60 | | elnnne0 11306 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐴) ∈
ℕ ↔ ((#‘𝐴)
∈ ℕ0 ∧ (#‘𝐴) ≠ 0)) |
61 | 60 | simplbi2 655 |
. . . . . . . . . . . . 13
⊢
((#‘𝐴) ∈
ℕ0 → ((#‘𝐴) ≠ 0 → (#‘𝐴) ∈ ℕ)) |
62 | 59, 61 | syl5bir 233 |
. . . . . . . . . . . 12
⊢
((#‘𝐴) ∈
ℕ0 → (¬ (#‘𝐴) = 0 → (#‘𝐴) ∈ ℕ)) |
63 | 58, 62 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (¬ (#‘𝐴) = 0 → (#‘𝐴) ∈ ℕ)) |
64 | 63 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (¬ (#‘𝐴) = 0 → (#‘𝐴) ∈ ℕ)) |
65 | 64 | impcom 446 |
. . . . . . . . 9
⊢ ((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → (#‘𝐴) ∈ ℕ) |
66 | 65 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (#‘𝐴) ∈ ℕ) |
67 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (0...(#‘𝐴)) ↔ (𝑁 ∈ ℕ0 ∧
(#‘𝐴) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝐴))) |
68 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
69 | 68 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ 𝑘 ∈
ℝ) |
70 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
71 | 70 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → 𝑀 ∈ ℝ) |
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ 𝑀 ∈
ℝ) |
73 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
74 | 73 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ 𝑁 ∈
ℝ) |
75 | 69, 72, 74 | ltaddsubd 10627 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ ((𝑘 + 𝑀) < 𝑁 ↔ 𝑘 < (𝑁 − 𝑀))) |
76 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑘 + 𝑀) ∈ ℕ0 → (𝑘 + 𝑀) ∈ ℝ) |
77 | 49, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑘 + 𝑀) ∈ ℝ) |
78 | 77 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (𝑘 + 𝑀) ∈
ℝ) |
79 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐴) ∈
ℕ0 → (#‘𝐴) ∈ ℝ) |
80 | 79 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) → (#‘𝐴) ∈ ℝ) |
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (#‘𝐴) ∈
ℝ) |
82 | | ltletr 10129 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑘 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (#‘𝐴) ∈ ℝ) →
(((𝑘 + 𝑀) < 𝑁 ∧ 𝑁 ≤ (#‘𝐴)) → (𝑘 + 𝑀) < (#‘𝐴))) |
83 | 78, 74, 81, 82 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (((𝑘 + 𝑀) < 𝑁 ∧ 𝑁 ≤ (#‘𝐴)) → (𝑘 + 𝑀) < (#‘𝐴))) |
84 | 83 | expd 452 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ ((𝑘 + 𝑀) < 𝑁 → (𝑁 ≤ (#‘𝐴) → (𝑘 + 𝑀) < (#‘𝐴)))) |
85 | 75, 84 | sylbird 250 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (𝑘 < (𝑁 − 𝑀) → (𝑁 ≤ (#‘𝐴) → (𝑘 + 𝑀) < (#‘𝐴)))) |
86 | 85 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) → ((𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑘 < (𝑁 − 𝑀) → (𝑁 ≤ (#‘𝐴) → (𝑘 + 𝑀) < (#‘𝐴))))) |
87 | 86 | com24 95 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) → (𝑁 ≤ (#‘𝐴) → (𝑘 < (𝑁 − 𝑀) → ((𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + 𝑀) < (#‘𝐴))))) |
88 | 87 | 3impia 1261 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝐴)) →
(𝑘 < (𝑁 − 𝑀) → ((𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + 𝑀) < (#‘𝐴)))) |
89 | 88 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑘 < (𝑁 − 𝑀) → ((𝑁 ∈ ℕ0 ∧
(#‘𝐴) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝐴)) →
(𝑘 + 𝑀) < (#‘𝐴)))) |
90 | 89 | impancom 456 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑘 < (𝑁 − 𝑀)) → (𝑀 ∈ ℕ0 → ((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝐴)) →
(𝑘 + 𝑀) < (#‘𝐴)))) |
91 | 90 | 3adant2 1080 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑀 ∈ ℕ0 → ((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝐴)) →
(𝑘 + 𝑀) < (#‘𝐴)))) |
92 | 91 | com13 88 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝐴)) →
(𝑀 ∈
ℕ0 → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (#‘𝐴)))) |
93 | 67, 92 | sylbi 207 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (0...(#‘𝐴)) → (𝑀 ∈ ℕ0 → ((𝑘 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (#‘𝐴)))) |
94 | 93 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ0
→ (𝑁 ∈
(0...(#‘𝐴)) →
((𝑘 ∈
ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (#‘𝐴)))) |
95 | 94 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑀
≤ 𝑁) → (𝑁 ∈ (0...(#‘𝐴)) → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (#‘𝐴)))) |
96 | 48, 95 | sylbi 207 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ (0...𝑁) → (𝑁 ∈ (0...(#‘𝐴)) → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (#‘𝐴)))) |
97 | 96 | a1i 11 |
. . . . . . . . . . 11
⊢ ((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → (𝑀 ∈ (0...𝑁) → (𝑁 ∈ (0...(#‘𝐴)) → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (#‘𝐴))))) |
98 | 97 | imp32 449 |
. . . . . . . . . 10
⊢ (((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (#‘𝐴))) |
99 | 47, 98 | syl5bi 232 |
. . . . . . . . 9
⊢ (((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → (𝑘 ∈ (0..^(𝑁 − 𝑀)) → (𝑘 + 𝑀) < (#‘𝐴))) |
100 | 99 | imp 445 |
. . . . . . . 8
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝑘 + 𝑀) < (#‘𝐴)) |
101 | | elfzo0 12508 |
. . . . . . . 8
⊢ ((𝑘 + 𝑀) ∈ (0..^(#‘𝐴)) ↔ ((𝑘 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝑘 + 𝑀) < (#‘𝐴))) |
102 | 57, 66, 100, 101 | syl3anbrc 1246 |
. . . . . . 7
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝑘 + 𝑀) ∈ (0..^(#‘𝐴))) |
103 | | ccatval1 13361 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝑘 + 𝑀) ∈ (0..^(#‘𝐴))) → ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀)) = (𝐴‘(𝑘 + 𝑀))) |
104 | 44, 46, 102, 103 | syl3anc 1326 |
. . . . . 6
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀)) = (𝐴‘(𝑘 + 𝑀))) |
105 | 27 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
106 | 29 | adantr 481 |
. . . . . . . 8
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝑀 ∈ (0...𝑁)) |
107 | 34 | adantr 481 |
. . . . . . . 8
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵)))) |
108 | 105, 106,
107 | 3jca 1242 |
. . . . . . 7
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))))) |
109 | | swrdfv 13424 |
. . . . . . 7
⊢ ((((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀))) |
110 | 108, 109 | sylancom 701 |
. . . . . 6
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀))) |
111 | | swrdfv 13424 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → ((𝐴 substr 〈𝑀, 𝑁〉)‘𝑘) = (𝐴‘(𝑘 + 𝑀))) |
112 | 40, 111 | sylan 488 |
. . . . . 6
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → ((𝐴 substr 〈𝑀, 𝑁〉)‘𝑘) = (𝐴‘(𝑘 + 𝑀))) |
113 | 104, 110,
112 | 3eqtr4d 2666 |
. . . . 5
⊢ ((((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐴 substr 〈𝑀, 𝑁〉)‘𝑘)) |
114 | 36, 42, 113 | eqfnfvd 6314 |
. . . 4
⊢ (((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)) |
115 | 114 | ex 450 |
. . 3
⊢ ((¬
(#‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
116 | 115 | ex 450 |
. 2
⊢ (¬
(#‘𝐴) = 0 →
((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)))) |
117 | 25, 116 | pm2.61i 176 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |