Proof of Theorem swrdccatid
Step | Hyp | Ref
| Expression |
1 | | 3simpa 1058 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
2 | | lencl 13324 |
. . . . 5
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈
ℕ0) |
3 | | lencl 13324 |
. . . . . 6
⊢ (𝐵 ∈ Word 𝑉 → (#‘𝐵) ∈
ℕ0) |
4 | | simplr 792 |
. . . . . . . . 9
⊢
((((#‘𝐵)
∈ ℕ0 ∧ (#‘𝐴) ∈ ℕ0) ∧ 𝑁 = (#‘𝐴)) → (#‘𝐴) ∈
ℕ0) |
5 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝑁 = (#‘𝐴) → (𝑁 ∈ ℕ0 ↔
(#‘𝐴) ∈
ℕ0)) |
6 | 5 | adantl 482 |
. . . . . . . . 9
⊢
((((#‘𝐵)
∈ ℕ0 ∧ (#‘𝐴) ∈ ℕ0) ∧ 𝑁 = (#‘𝐴)) → (𝑁 ∈ ℕ0 ↔
(#‘𝐴) ∈
ℕ0)) |
7 | 4, 6 | mpbird 247 |
. . . . . . . 8
⊢
((((#‘𝐵)
∈ ℕ0 ∧ (#‘𝐴) ∈ ℕ0) ∧ 𝑁 = (#‘𝐴)) → 𝑁 ∈
ℕ0) |
8 | | nn0addcl 11328 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
((#‘𝐴) +
(#‘𝐵)) ∈
ℕ0) |
9 | 8 | ancoms 469 |
. . . . . . . . 9
⊢
(((#‘𝐵) ∈
ℕ0 ∧ (#‘𝐴) ∈ ℕ0) →
((#‘𝐴) +
(#‘𝐵)) ∈
ℕ0) |
10 | 9 | adantr 481 |
. . . . . . . 8
⊢
((((#‘𝐵)
∈ ℕ0 ∧ (#‘𝐴) ∈ ℕ0) ∧ 𝑁 = (#‘𝐴)) → ((#‘𝐴) + (#‘𝐵)) ∈
ℕ0) |
11 | | nn0re 11301 |
. . . . . . . . . . . . 13
⊢
((#‘𝐴) ∈
ℕ0 → (#‘𝐴) ∈ ℝ) |
12 | 11 | anim1i 592 |
. . . . . . . . . . . 12
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
((#‘𝐴) ∈ ℝ
∧ (#‘𝐵) ∈
ℕ0)) |
13 | 12 | ancoms 469 |
. . . . . . . . . . 11
⊢
(((#‘𝐵) ∈
ℕ0 ∧ (#‘𝐴) ∈ ℕ0) →
((#‘𝐴) ∈ ℝ
∧ (#‘𝐵) ∈
ℕ0)) |
14 | | nn0addge1 11339 |
. . . . . . . . . . 11
⊢
(((#‘𝐴) ∈
ℝ ∧ (#‘𝐵)
∈ ℕ0) → (#‘𝐴) ≤ ((#‘𝐴) + (#‘𝐵))) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
⊢
(((#‘𝐵) ∈
ℕ0 ∧ (#‘𝐴) ∈ ℕ0) →
(#‘𝐴) ≤
((#‘𝐴) +
(#‘𝐵))) |
16 | 15 | adantr 481 |
. . . . . . . . 9
⊢
((((#‘𝐵)
∈ ℕ0 ∧ (#‘𝐴) ∈ ℕ0) ∧ 𝑁 = (#‘𝐴)) → (#‘𝐴) ≤ ((#‘𝐴) + (#‘𝐵))) |
17 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑁 = (#‘𝐴) → (𝑁 ≤ ((#‘𝐴) + (#‘𝐵)) ↔ (#‘𝐴) ≤ ((#‘𝐴) + (#‘𝐵)))) |
18 | 17 | adantl 482 |
. . . . . . . . 9
⊢
((((#‘𝐵)
∈ ℕ0 ∧ (#‘𝐴) ∈ ℕ0) ∧ 𝑁 = (#‘𝐴)) → (𝑁 ≤ ((#‘𝐴) + (#‘𝐵)) ↔ (#‘𝐴) ≤ ((#‘𝐴) + (#‘𝐵)))) |
19 | 16, 18 | mpbird 247 |
. . . . . . . 8
⊢
((((#‘𝐵)
∈ ℕ0 ∧ (#‘𝐴) ∈ ℕ0) ∧ 𝑁 = (#‘𝐴)) → 𝑁 ≤ ((#‘𝐴) + (#‘𝐵))) |
20 | | elfz2nn0 12431 |
. . . . . . . 8
⊢ (𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵))) ↔ (𝑁 ∈ ℕ0 ∧
((#‘𝐴) +
(#‘𝐵)) ∈
ℕ0 ∧ 𝑁
≤ ((#‘𝐴) +
(#‘𝐵)))) |
21 | 7, 10, 19, 20 | syl3anbrc 1246 |
. . . . . . 7
⊢
((((#‘𝐵)
∈ ℕ0 ∧ (#‘𝐴) ∈ ℕ0) ∧ 𝑁 = (#‘𝐴)) → 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵)))) |
22 | 21 | exp31 630 |
. . . . . 6
⊢
((#‘𝐵) ∈
ℕ0 → ((#‘𝐴) ∈ ℕ0 → (𝑁 = (#‘𝐴) → 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵)))))) |
23 | 3, 22 | syl 17 |
. . . . 5
⊢ (𝐵 ∈ Word 𝑉 → ((#‘𝐴) ∈ ℕ0 → (𝑁 = (#‘𝐴) → 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵)))))) |
24 | 2, 23 | syl5com 31 |
. . . 4
⊢ (𝐴 ∈ Word 𝑉 → (𝐵 ∈ Word 𝑉 → (𝑁 = (#‘𝐴) → 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵)))))) |
25 | 24 | 3imp 1256 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵)))) |
26 | | eqid 2622 |
. . . 4
⊢
(#‘𝐴) =
(#‘𝐴) |
27 | 26 | swrdccat3a 13494 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = if(𝑁 ≤ (#‘𝐴), (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − (#‘𝐴))〉))))) |
28 | 1, 25, 27 | sylc 65 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = if(𝑁 ≤ (#‘𝐴), (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − (#‘𝐴))〉)))) |
29 | 2, 11 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈ ℝ) |
30 | 29 | leidd 10594 |
. . . . 5
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ≤ (#‘𝐴)) |
31 | 30 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → (#‘𝐴) ≤ (#‘𝐴)) |
32 | | breq1 4656 |
. . . . 5
⊢ (𝑁 = (#‘𝐴) → (𝑁 ≤ (#‘𝐴) ↔ (#‘𝐴) ≤ (#‘𝐴))) |
33 | 32 | 3ad2ant3 1084 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → (𝑁 ≤ (#‘𝐴) ↔ (#‘𝐴) ≤ (#‘𝐴))) |
34 | 31, 33 | mpbird 247 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → 𝑁 ≤ (#‘𝐴)) |
35 | 34 | iftrued 4094 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → if(𝑁 ≤ (#‘𝐴), (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − (#‘𝐴))〉))) = (𝐴 substr 〈0, 𝑁〉)) |
36 | | swrdid 13428 |
. . . 4
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr 〈0, (#‘𝐴)〉) = 𝐴) |
37 | 36 | 3ad2ant1 1082 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → (𝐴 substr 〈0, (#‘𝐴)〉) = 𝐴) |
38 | | opeq2 4403 |
. . . . . 6
⊢ (𝑁 = (#‘𝐴) → 〈0, 𝑁〉 = 〈0, (#‘𝐴)〉) |
39 | 38 | oveq2d 6666 |
. . . . 5
⊢ (𝑁 = (#‘𝐴) → (𝐴 substr 〈0, 𝑁〉) = (𝐴 substr 〈0, (#‘𝐴)〉)) |
40 | 39 | eqeq1d 2624 |
. . . 4
⊢ (𝑁 = (#‘𝐴) → ((𝐴 substr 〈0, 𝑁〉) = 𝐴 ↔ (𝐴 substr 〈0, (#‘𝐴)〉) = 𝐴)) |
41 | 40 | 3ad2ant3 1084 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → ((𝐴 substr 〈0, 𝑁〉) = 𝐴 ↔ (𝐴 substr 〈0, (#‘𝐴)〉) = 𝐴)) |
42 | 37, 41 | mpbird 247 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → (𝐴 substr 〈0, 𝑁〉) = 𝐴) |
43 | 28, 35, 42 | 3eqtrd 2660 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝐴)) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = 𝐴) |