Proof of Theorem lswccatn0lsw
Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . 4
⊢ (𝐴 ++ 𝐵) ∈ V |
2 | | lsw 13204 |
. . . 4
⊢ ((𝐴 ++ 𝐵) ∈ V → ( lastS ‘(𝐴 ++ 𝐵)) = ((𝐴 ++ 𝐵)‘((#‘(𝐴 ++ 𝐵)) − 1))) |
3 | 1, 2 | mp1i 13 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ( lastS ‘(𝐴 ++ 𝐵)) = ((𝐴 ++ 𝐵)‘((#‘(𝐴 ++ 𝐵)) − 1))) |
4 | | ccatlen 13213 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (#‘(𝐴 ++ 𝐵)) = ((#‘𝐴) + (#‘𝐵))) |
5 | 4 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((#‘(𝐴 ++ 𝐵)) − 1) = (((#‘𝐴) + (#‘𝐵)) − 1)) |
6 | 5 | 3adant3 1074 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((#‘(𝐴 ++ 𝐵)) − 1) = (((#‘𝐴) + (#‘𝐵)) − 1)) |
7 | | lencl 13179 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈
ℕ0) |
8 | 7 | nn0zd 11356 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈ ℤ) |
9 | 8 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (#‘𝐴) ∈
ℤ) |
10 | | lennncl 13180 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (#‘𝐵) ∈
ℕ) |
11 | 10 | 3adant1 1072 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (#‘𝐵) ∈
ℕ) |
12 | | simpl 472 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℤ ∧ (#‘𝐵)
∈ ℕ) → (#‘𝐴) ∈ ℤ) |
13 | | nnz 11276 |
. . . . . . . . . . . 12
⊢
((#‘𝐵) ∈
ℕ → (#‘𝐵)
∈ ℤ) |
14 | 13 | adantl 481 |
. . . . . . . . . . 11
⊢
(((#‘𝐴) ∈
ℤ ∧ (#‘𝐵)
∈ ℕ) → (#‘𝐵) ∈ ℤ) |
15 | 12, 14 | zaddcld 11362 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℤ ∧ (#‘𝐵)
∈ ℕ) → ((#‘𝐴) + (#‘𝐵)) ∈ ℤ) |
16 | | zre 11258 |
. . . . . . . . . . 11
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
∈ ℝ) |
17 | | nnrp 11718 |
. . . . . . . . . . 11
⊢
((#‘𝐵) ∈
ℕ → (#‘𝐵)
∈ ℝ+) |
18 | | ltaddrp 11743 |
. . . . . . . . . . 11
⊢
(((#‘𝐴) ∈
ℝ ∧ (#‘𝐵)
∈ ℝ+) → (#‘𝐴) < ((#‘𝐴) + (#‘𝐵))) |
19 | 16, 17, 18 | syl2an 493 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℤ ∧ (#‘𝐵)
∈ ℕ) → (#‘𝐴) < ((#‘𝐴) + (#‘𝐵))) |
20 | 12, 15, 19 | 3jca 1235 |
. . . . . . . . 9
⊢
(((#‘𝐴) ∈
ℤ ∧ (#‘𝐵)
∈ ℕ) → ((#‘𝐴) ∈ ℤ ∧ ((#‘𝐴) + (#‘𝐵)) ∈ ℤ ∧ (#‘𝐴) < ((#‘𝐴) + (#‘𝐵)))) |
21 | 9, 11, 20 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((#‘𝐴) ∈ ℤ ∧
((#‘𝐴) +
(#‘𝐵)) ∈ ℤ
∧ (#‘𝐴) <
((#‘𝐴) +
(#‘𝐵)))) |
22 | | fzolb 12345 |
. . . . . . . 8
⊢
((#‘𝐴) ∈
((#‘𝐴)..^((#‘𝐴) + (#‘𝐵))) ↔ ((#‘𝐴) ∈ ℤ ∧ ((#‘𝐴) + (#‘𝐵)) ∈ ℤ ∧ (#‘𝐴) < ((#‘𝐴) + (#‘𝐵)))) |
23 | 21, 22 | sylibr 223 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (#‘𝐴) ∈ ((#‘𝐴)..^((#‘𝐴) + (#‘𝐵)))) |
24 | | fzoend 12425 |
. . . . . . 7
⊢
((#‘𝐴) ∈
((#‘𝐴)..^((#‘𝐴) + (#‘𝐵))) → (((#‘𝐴) + (#‘𝐵)) − 1) ∈ ((#‘𝐴)..^((#‘𝐴) + (#‘𝐵)))) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (((#‘𝐴) + (#‘𝐵)) − 1) ∈ ((#‘𝐴)..^((#‘𝐴) + (#‘𝐵)))) |
26 | 6, 25 | eqeltrd 2688 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((#‘(𝐴 ++ 𝐵)) − 1) ∈ ((#‘𝐴)..^((#‘𝐴) + (#‘𝐵)))) |
27 | | ccatval2 13215 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ ((#‘(𝐴 ++ 𝐵)) − 1) ∈ ((#‘𝐴)..^((#‘𝐴) + (#‘𝐵)))) → ((𝐴 ++ 𝐵)‘((#‘(𝐴 ++ 𝐵)) − 1)) = (𝐵‘(((#‘(𝐴 ++ 𝐵)) − 1) − (#‘𝐴)))) |
28 | 26, 27 | syld3an3 1363 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘((#‘(𝐴 ++ 𝐵)) − 1)) = (𝐵‘(((#‘(𝐴 ++ 𝐵)) − 1) − (#‘𝐴)))) |
29 | 5 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (((#‘(𝐴 ++ 𝐵)) − 1) − (#‘𝐴)) = ((((#‘𝐴) + (#‘𝐵)) − 1) − (#‘𝐴))) |
30 | 7 | nn0cnd 11230 |
. . . . . . . 8
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈ ℂ) |
31 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝐵 ∈ Word 𝑉 → (#‘𝐵) ∈
ℕ0) |
32 | 31 | nn0cnd 11230 |
. . . . . . . 8
⊢ (𝐵 ∈ Word 𝑉 → (#‘𝐵) ∈ ℂ) |
33 | | addcl 9897 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℂ ∧ (#‘𝐵)
∈ ℂ) → ((#‘𝐴) + (#‘𝐵)) ∈ ℂ) |
34 | | 1cnd 9935 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℂ ∧ (#‘𝐵)
∈ ℂ) → 1 ∈ ℂ) |
35 | | simpl 472 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℂ ∧ (#‘𝐵)
∈ ℂ) → (#‘𝐴) ∈ ℂ) |
36 | 33, 34, 35 | sub32d 10303 |
. . . . . . . . 9
⊢
(((#‘𝐴) ∈
ℂ ∧ (#‘𝐵)
∈ ℂ) → ((((#‘𝐴) + (#‘𝐵)) − 1) − (#‘𝐴)) = ((((#‘𝐴) + (#‘𝐵)) − (#‘𝐴)) − 1)) |
37 | | pncan2 10167 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℂ ∧ (#‘𝐵)
∈ ℂ) → (((#‘𝐴) + (#‘𝐵)) − (#‘𝐴)) = (#‘𝐵)) |
38 | 37 | oveq1d 6564 |
. . . . . . . . 9
⊢
(((#‘𝐴) ∈
ℂ ∧ (#‘𝐵)
∈ ℂ) → ((((#‘𝐴) + (#‘𝐵)) − (#‘𝐴)) − 1) = ((#‘𝐵) − 1)) |
39 | 36, 38 | eqtrd 2644 |
. . . . . . . 8
⊢
(((#‘𝐴) ∈
ℂ ∧ (#‘𝐵)
∈ ℂ) → ((((#‘𝐴) + (#‘𝐵)) − 1) − (#‘𝐴)) = ((#‘𝐵) − 1)) |
40 | 30, 32, 39 | syl2an 493 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((((#‘𝐴) + (#‘𝐵)) − 1) − (#‘𝐴)) = ((#‘𝐵) − 1)) |
41 | 29, 40 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (((#‘(𝐴 ++ 𝐵)) − 1) − (#‘𝐴)) = ((#‘𝐵) − 1)) |
42 | 41 | 3adant3 1074 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (((#‘(𝐴 ++ 𝐵)) − 1) − (#‘𝐴)) = ((#‘𝐵) − 1)) |
43 | 42 | fveq2d 6107 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (𝐵‘(((#‘(𝐴 ++ 𝐵)) − 1) − (#‘𝐴))) = (𝐵‘((#‘𝐵) − 1))) |
44 | 28, 43 | eqtrd 2644 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘((#‘(𝐴 ++ 𝐵)) − 1)) = (𝐵‘((#‘𝐵) − 1))) |
45 | 3, 44 | eqtrd 2644 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ( lastS ‘(𝐴 ++ 𝐵)) = (𝐵‘((#‘𝐵) − 1))) |
46 | | lsw 13204 |
. . . 4
⊢ (𝐵 ∈ Word 𝑉 → ( lastS ‘𝐵) = (𝐵‘((#‘𝐵) − 1))) |
47 | 46 | eqcomd 2616 |
. . 3
⊢ (𝐵 ∈ Word 𝑉 → (𝐵‘((#‘𝐵) − 1)) = ( lastS ‘𝐵)) |
48 | 47 | 3ad2ant2 1076 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (𝐵‘((#‘𝐵) − 1)) = ( lastS ‘𝐵)) |
49 | 45, 48 | eqtrd 2644 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ( lastS ‘(𝐴 ++ 𝐵)) = ( lastS ‘𝐵)) |