Step | Hyp | Ref
| Expression |
1 | | oveq2 6918 |
. . . . . . 7
⊢
((♯‘𝐴) =
0 → (0...(♯‘𝐴)) = (0...0)) |
2 | 1 | eleq2d 2892 |
. . . . . 6
⊢
((♯‘𝐴) =
0 → (𝑁 ∈
(0...(♯‘𝐴))
↔ 𝑁 ∈
(0...0))) |
3 | | elfz1eq 12652 |
. . . . . . 7
⊢ (𝑁 ∈ (0...0) → 𝑁 = 0) |
4 | | elfz1eq 12652 |
. . . . . . . . 9
⊢ (𝑀 ∈ (0...0) → 𝑀 = 0) |
5 | | swrd00 13711 |
. . . . . . . . . . 11
⊢ ((𝐴 ++ 𝐵) substr 〈0, 0〉) =
∅ |
6 | | swrd00 13711 |
. . . . . . . . . . 11
⊢ (𝐴 substr 〈0, 0〉) =
∅ |
7 | 5, 6 | eqtr4i 2852 |
. . . . . . . . . 10
⊢ ((𝐴 ++ 𝐵) substr 〈0, 0〉) = (𝐴 substr 〈0,
0〉) |
8 | | opeq1 4625 |
. . . . . . . . . . 11
⊢ (𝑀 = 0 → 〈𝑀, 0〉 = 〈0,
0〉) |
9 | 8 | oveq2d 6926 |
. . . . . . . . . 10
⊢ (𝑀 = 0 → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = ((𝐴 ++ 𝐵) substr 〈0, 0〉)) |
10 | 8 | oveq2d 6926 |
. . . . . . . . . 10
⊢ (𝑀 = 0 → (𝐴 substr 〈𝑀, 0〉) = (𝐴 substr 〈0, 0〉)) |
11 | 7, 9, 10 | 3eqtr4a 2887 |
. . . . . . . . 9
⊢ (𝑀 = 0 → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉)) |
12 | 4, 11 | syl 17 |
. . . . . . . 8
⊢ (𝑀 ∈ (0...0) → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉)) |
13 | | oveq2 6918 |
. . . . . . . . . 10
⊢ (𝑁 = 0 → (0...𝑁) = (0...0)) |
14 | 13 | eleq2d 2892 |
. . . . . . . . 9
⊢ (𝑁 = 0 → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ∈ (0...0))) |
15 | | opeq2 4626 |
. . . . . . . . . . 11
⊢ (𝑁 = 0 → 〈𝑀, 𝑁〉 = 〈𝑀, 0〉) |
16 | 15 | oveq2d 6926 |
. . . . . . . . . 10
⊢ (𝑁 = 0 → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉)) |
17 | 15 | oveq2d 6926 |
. . . . . . . . . 10
⊢ (𝑁 = 0 → (𝐴 substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 0〉)) |
18 | 16, 17 | eqeq12d 2840 |
. . . . . . . . 9
⊢ (𝑁 = 0 → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉) ↔ ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉))) |
19 | 14, 18 | imbi12d 336 |
. . . . . . . 8
⊢ (𝑁 = 0 → ((𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)) ↔ (𝑀 ∈ (0...0) → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉)))) |
20 | 12, 19 | mpbiri 250 |
. . . . . . 7
⊢ (𝑁 = 0 → (𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
21 | 3, 20 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ (0...0) → (𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
22 | 2, 21 | syl6bi 245 |
. . . . 5
⊢
((♯‘𝐴) =
0 → (𝑁 ∈
(0...(♯‘𝐴))
→ (𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)))) |
23 | 22 | com23 86 |
. . . 4
⊢
((♯‘𝐴) =
0 → (𝑀 ∈
(0...𝑁) → (𝑁 ∈
(0...(♯‘𝐴))
→ ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)))) |
24 | 23 | impd 400 |
. . 3
⊢
((♯‘𝐴) =
0 → ((𝑀 ∈
(0...𝑁) ∧ 𝑁 ∈
(0...(♯‘𝐴)))
→ ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
25 | 24 | a1d 25 |
. 2
⊢
((♯‘𝐴) =
0 → ((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)))) |
26 | | ccatcl 13641 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
27 | 26 | adantl 475 |
. . . . . . 7
⊢ ((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
28 | 27 | adantr 474 |
. . . . . 6
⊢ (((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
29 | | simprl 787 |
. . . . . 6
⊢ (((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → 𝑀 ∈ (0...𝑁)) |
30 | | elfzelfzccat 13647 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(♯‘𝐴)) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵))))) |
31 | 30 | adantl 475 |
. . . . . . . . 9
⊢ ((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → (𝑁 ∈ (0...(♯‘𝐴)) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵))))) |
32 | 31 | com12 32 |
. . . . . . . 8
⊢ (𝑁 ∈
(0...(♯‘𝐴))
→ ((¬ (♯‘𝐴) = 0 ∧ (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵))))) |
33 | 32 | adantl 475 |
. . . . . . 7
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → ((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵))))) |
34 | 33 | impcom 398 |
. . . . . 6
⊢ (((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) |
35 | | swrdvalfn 13720 |
. . . . . 6
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
36 | 28, 29, 34, 35 | syl3anc 1494 |
. . . . 5
⊢ (((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
37 | | 3anass 1120 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) ↔ (𝐴 ∈ Word 𝑉 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))))) |
38 | 37 | simplbi2 496 |
. . . . . . . 8
⊢ (𝐴 ∈ Word 𝑉 → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))))) |
39 | 38 | ad2antrl 719 |
. . . . . . 7
⊢ ((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))))) |
40 | 39 | imp 397 |
. . . . . 6
⊢ (((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) |
41 | | swrdvalfn 13720 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → (𝐴 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
42 | 40, 41 | syl 17 |
. . . . 5
⊢ (((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝐴 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
43 | | simprl 787 |
. . . . . . . 8
⊢ ((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → 𝐴 ∈ Word 𝑉) |
44 | 43 | ad2antrr 717 |
. . . . . . 7
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝐴 ∈ Word 𝑉) |
45 | | simprr 789 |
. . . . . . . 8
⊢ ((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → 𝐵 ∈ Word 𝑉) |
46 | 45 | ad2antrr 717 |
. . . . . . 7
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝐵 ∈ Word 𝑉) |
47 | | elfzo0 12811 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0..^(𝑁 − 𝑀)) ↔ (𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀))) |
48 | | elfz2nn0 12732 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
49 | | nn0addcl 11662 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑘 + 𝑀) ∈
ℕ0) |
50 | 49 | expcom 404 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ0
→ (𝑘 ∈
ℕ0 → (𝑘 + 𝑀) ∈
ℕ0)) |
51 | 50 | 3ad2ant1 1167 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑀
≤ 𝑁) → (𝑘 ∈ ℕ0
→ (𝑘 + 𝑀) ∈
ℕ0)) |
52 | 48, 51 | sylbi 209 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (0...𝑁) → (𝑘 ∈ ℕ0 → (𝑘 + 𝑀) ∈
ℕ0)) |
53 | 52 | ad2antrl 719 |
. . . . . . . . . . . 12
⊢ (((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝑘 ∈ ℕ0 → (𝑘 + 𝑀) ∈
ℕ0)) |
54 | 53 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (((¬ (♯‘𝐴) = 0 ∧ (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝑘 + 𝑀) ∈
ℕ0)) |
55 | 54 | 3ad2ant1 1167 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (((¬ (♯‘𝐴) = 0 ∧ (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝑘 + 𝑀) ∈
ℕ0)) |
56 | 47, 55 | sylbi 209 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0..^(𝑁 − 𝑀)) → (((¬ (♯‘𝐴) = 0 ∧ (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝑘 + 𝑀) ∈
ℕ0)) |
57 | 56 | impcom 398 |
. . . . . . . 8
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝑘 + 𝑀) ∈
ℕ0) |
58 | | lencl 13600 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈
ℕ0) |
59 | | df-ne 3000 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐴)
≠ 0 ↔ ¬ (♯‘𝐴) = 0) |
60 | | elnnne0 11641 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐴)
∈ ℕ ↔ ((♯‘𝐴) ∈ ℕ0 ∧
(♯‘𝐴) ≠
0)) |
61 | 60 | simplbi2 496 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐴)
∈ ℕ0 → ((♯‘𝐴) ≠ 0 → (♯‘𝐴) ∈
ℕ)) |
62 | 59, 61 | syl5bir 235 |
. . . . . . . . . . . 12
⊢
((♯‘𝐴)
∈ ℕ0 → (¬ (♯‘𝐴) = 0 → (♯‘𝐴) ∈
ℕ)) |
63 | 58, 62 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (¬ (♯‘𝐴) = 0 →
(♯‘𝐴) ∈
ℕ)) |
64 | 63 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (¬ (♯‘𝐴) = 0 →
(♯‘𝐴) ∈
ℕ)) |
65 | 64 | impcom 398 |
. . . . . . . . 9
⊢ ((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → (♯‘𝐴) ∈ ℕ) |
66 | 65 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (♯‘𝐴) ∈ ℕ) |
67 | | elfz2nn0 12732 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(0...(♯‘𝐴))
↔ (𝑁 ∈
ℕ0 ∧ (♯‘𝐴) ∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝐴))) |
68 | | nn0re 11635 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
69 | 68 | ad2antrl 719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ 𝑘 ∈
ℝ) |
70 | | nn0re 11635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
71 | 70 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → 𝑀 ∈ ℝ) |
72 | 71 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ 𝑀 ∈
ℝ) |
73 | | nn0re 11635 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
74 | 73 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ 𝑁 ∈
ℝ) |
75 | 69, 72, 74 | ltaddsubd 10959 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ ((𝑘 + 𝑀) < 𝑁 ↔ 𝑘 < (𝑁 − 𝑀))) |
76 | | nn0re 11635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑘 + 𝑀) ∈ ℕ0 → (𝑘 + 𝑀) ∈ ℝ) |
77 | 49, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑘 + 𝑀) ∈ ℝ) |
78 | 77 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (𝑘 + 𝑀) ∈
ℝ) |
79 | | nn0re 11635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝐴)
∈ ℕ0 → (♯‘𝐴) ∈ ℝ) |
80 | 79 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) → (♯‘𝐴) ∈ ℝ) |
81 | 80 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (♯‘𝐴)
∈ ℝ) |
82 | | ltletr 10455 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑘 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ) →
(((𝑘 + 𝑀) < 𝑁 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑘 + 𝑀) < (♯‘𝐴))) |
83 | 78, 74, 81, 82 | syl3anc 1494 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (((𝑘 + 𝑀) < 𝑁 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑘 + 𝑀) < (♯‘𝐴))) |
84 | 83 | expd 406 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ ((𝑘 + 𝑀) < 𝑁 → (𝑁 ≤ (♯‘𝐴) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
85 | 75, 84 | sylbird 252 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (𝑘 < (𝑁 − 𝑀) → (𝑁 ≤ (♯‘𝐴) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
86 | 85 | ex 403 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) → ((𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑘 < (𝑁 − 𝑀) → (𝑁 ≤ (♯‘𝐴) → (𝑘 + 𝑀) < (♯‘𝐴))))) |
87 | 86 | com24 95 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) → (𝑁 ≤ (♯‘𝐴) → (𝑘 < (𝑁 − 𝑀) → ((𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + 𝑀) < (♯‘𝐴))))) |
88 | 87 | 3impia 1149 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑘 < (𝑁 − 𝑀) → ((𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + 𝑀) < (♯‘𝐴)))) |
89 | 88 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑘 < (𝑁 − 𝑀) → ((𝑁 ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ0 ∧ 𝑁
≤ (♯‘𝐴))
→ (𝑘 + 𝑀) < (♯‘𝐴)))) |
90 | 89 | impancom 445 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ 𝑘 < (𝑁 − 𝑀)) → (𝑀 ∈ ℕ0 → ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
91 | 90 | 3adant2 1165 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑀 ∈ ℕ0 → ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
92 | 91 | com13 88 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑀 ∈ ℕ0 → ((𝑘 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
93 | 67, 92 | sylbi 209 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(0...(♯‘𝐴))
→ (𝑀 ∈
ℕ0 → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
94 | 93 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ0
→ (𝑁 ∈
(0...(♯‘𝐴))
→ ((𝑘 ∈
ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
95 | 94 | 3ad2ant1 1167 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑀
≤ 𝑁) → (𝑁 ∈
(0...(♯‘𝐴))
→ ((𝑘 ∈
ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
96 | 48, 95 | sylbi 209 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ (0...𝑁) → (𝑁 ∈ (0...(♯‘𝐴)) → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
97 | 96 | a1i 11 |
. . . . . . . . . . 11
⊢ ((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → (𝑀 ∈ (0...𝑁) → (𝑁 ∈ (0...(♯‘𝐴)) → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴))))) |
98 | 97 | imp32 411 |
. . . . . . . . . 10
⊢ (((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴))) |
99 | 47, 98 | syl5bi 234 |
. . . . . . . . 9
⊢ (((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝑘 ∈ (0..^(𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴))) |
100 | 99 | imp 397 |
. . . . . . . 8
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝑘 + 𝑀) < (♯‘𝐴)) |
101 | | elfzo0 12811 |
. . . . . . . 8
⊢ ((𝑘 + 𝑀) ∈ (0..^(♯‘𝐴)) ↔ ((𝑘 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝑘 + 𝑀) < (♯‘𝐴))) |
102 | 57, 66, 100, 101 | syl3anbrc 1447 |
. . . . . . 7
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝑘 + 𝑀) ∈ (0..^(♯‘𝐴))) |
103 | | ccatval1 13644 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝑘 + 𝑀) ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀)) = (𝐴‘(𝑘 + 𝑀))) |
104 | 44, 46, 102, 103 | syl3anc 1494 |
. . . . . 6
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀)) = (𝐴‘(𝑘 + 𝑀))) |
105 | 27 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
106 | 29 | adantr 474 |
. . . . . . . 8
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝑀 ∈ (0...𝑁)) |
107 | 34 | adantr 474 |
. . . . . . . 8
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) |
108 | 105, 106,
107 | 3jca 1162 |
. . . . . . 7
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵))))) |
109 | | swrdfv 13717 |
. . . . . . 7
⊢ ((((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀))) |
110 | 108, 109 | sylancom 582 |
. . . . . 6
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀))) |
111 | | swrdfv 13717 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → ((𝐴 substr 〈𝑀, 𝑁〉)‘𝑘) = (𝐴‘(𝑘 + 𝑀))) |
112 | 40, 111 | sylan 575 |
. . . . . 6
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → ((𝐴 substr 〈𝑀, 𝑁〉)‘𝑘) = (𝐴‘(𝑘 + 𝑀))) |
113 | 104, 110,
112 | 3eqtr4d 2871 |
. . . . 5
⊢ ((((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐴 substr 〈𝑀, 𝑁〉)‘𝑘)) |
114 | 36, 42, 113 | eqfnfvd 6568 |
. . . 4
⊢ (((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)) |
115 | 114 | ex 403 |
. . 3
⊢ ((¬
(♯‘𝐴) = 0 ∧
(𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
116 | 115 | ex 403 |
. 2
⊢ (¬
(♯‘𝐴) = 0
→ ((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)))) |
117 | 25, 116 | pm2.61i 177 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |