Proof of Theorem lswccatn0lsw
| Step | Hyp | Ref
| Expression |
| 1 | | ccatlen 14613 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) |
| 2 | 1 | oveq1d 7446 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘(𝐴 ++ 𝐵)) − 1) = (((♯‘𝐴) + (♯‘𝐵)) − 1)) |
| 3 | 2 | 3adant3 1133 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((♯‘(𝐴 ++ 𝐵)) − 1) = (((♯‘𝐴) + (♯‘𝐵)) − 1)) |
| 4 | | lencl 14571 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈
ℕ0) |
| 5 | 4 | nn0zd 12639 |
. . . . . . . . 9
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℤ) |
| 6 | | lennncl 14572 |
. . . . . . . . 9
⊢ ((𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (♯‘𝐵) ∈
ℕ) |
| 7 | | simpl 482 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) →
(♯‘𝐴) ∈
ℤ) |
| 8 | | nnz 12634 |
. . . . . . . . . . 11
⊢
((♯‘𝐵)
∈ ℕ → (♯‘𝐵) ∈ ℤ) |
| 9 | | zaddcl 12657 |
. . . . . . . . . . 11
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ) |
| 10 | 8, 9 | sylan2 593 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ) |
| 11 | | zre 12617 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℤ → (♯‘𝐴) ∈ ℝ) |
| 12 | | nnrp 13046 |
. . . . . . . . . . 11
⊢
((♯‘𝐵)
∈ ℕ → (♯‘𝐵) ∈
ℝ+) |
| 13 | | ltaddrp 13072 |
. . . . . . . . . . 11
⊢
(((♯‘𝐴)
∈ ℝ ∧ (♯‘𝐵) ∈ ℝ+) →
(♯‘𝐴) <
((♯‘𝐴) +
(♯‘𝐵))) |
| 14 | 11, 12, 13 | syl2an 596 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) →
(♯‘𝐴) <
((♯‘𝐴) +
(♯‘𝐵))) |
| 15 | 7, 10, 14 | 3jca 1129 |
. . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) →
((♯‘𝐴) ∈
ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ ∧ (♯‘𝐴) < ((♯‘𝐴) + (♯‘𝐵)))) |
| 16 | 5, 6, 15 | syl2an 596 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ (𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) ∈ ℤ ∧
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ ∧ (♯‘𝐴) < ((♯‘𝐴) + (♯‘𝐵)))) |
| 17 | 16 | 3impb 1115 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((♯‘𝐴) ∈ ℤ ∧
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ ∧ (♯‘𝐴) < ((♯‘𝐴) + (♯‘𝐵)))) |
| 18 | | fzolb 13705 |
. . . . . . 7
⊢
((♯‘𝐴)
∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ ((♯‘𝐴) ∈ ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ ∧
(♯‘𝐴) <
((♯‘𝐴) +
(♯‘𝐵)))) |
| 19 | 17, 18 | sylibr 234 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (♯‘𝐴) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
| 20 | | fzoend 13796 |
. . . . . 6
⊢
((♯‘𝐴)
∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) → (((♯‘𝐴) + (♯‘𝐵)) − 1) ∈
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
| 21 | 19, 20 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (((♯‘𝐴) + (♯‘𝐵)) − 1) ∈
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
| 22 | 3, 21 | eqeltrd 2841 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((♯‘(𝐴 ++ 𝐵)) − 1) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
| 23 | | ccatval2 14616 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ ((♯‘(𝐴 ++ 𝐵)) − 1) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘((♯‘(𝐴 ++ 𝐵)) − 1)) = (𝐵‘(((♯‘(𝐴 ++ 𝐵)) − 1) − (♯‘𝐴)))) |
| 24 | 22, 23 | syld3an3 1411 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘((♯‘(𝐴 ++ 𝐵)) − 1)) = (𝐵‘(((♯‘(𝐴 ++ 𝐵)) − 1) − (♯‘𝐴)))) |
| 25 | 2 | oveq1d 7446 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (((♯‘(𝐴 ++ 𝐵)) − 1) − (♯‘𝐴)) = ((((♯‘𝐴) + (♯‘𝐵)) − 1) −
(♯‘𝐴))) |
| 26 | 4 | nn0cnd 12589 |
. . . . . . 7
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℂ) |
| 27 | | lencl 14571 |
. . . . . . . 8
⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈
ℕ0) |
| 28 | 27 | nn0cnd 12589 |
. . . . . . 7
⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℂ) |
| 29 | | addcl 11237 |
. . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℂ) |
| 30 | | 1cnd 11256 |
. . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) → 1 ∈
ℂ) |
| 31 | | simpl 482 |
. . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) →
(♯‘𝐴) ∈
ℂ) |
| 32 | 29, 30, 31 | sub32d 11652 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) →
((((♯‘𝐴) +
(♯‘𝐵)) −
1) − (♯‘𝐴)) = ((((♯‘𝐴) + (♯‘𝐵)) − (♯‘𝐴)) − 1)) |
| 33 | | pncan2 11515 |
. . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) →
(((♯‘𝐴) +
(♯‘𝐵)) −
(♯‘𝐴)) =
(♯‘𝐵)) |
| 34 | 33 | oveq1d 7446 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) →
((((♯‘𝐴) +
(♯‘𝐵)) −
(♯‘𝐴)) −
1) = ((♯‘𝐵)
− 1)) |
| 35 | 32, 34 | eqtrd 2777 |
. . . . . . 7
⊢
(((♯‘𝐴)
∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) →
((((♯‘𝐴) +
(♯‘𝐵)) −
1) − (♯‘𝐴)) = ((♯‘𝐵) − 1)) |
| 36 | 26, 28, 35 | syl2an 596 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((((♯‘𝐴) + (♯‘𝐵)) − 1) − (♯‘𝐴)) = ((♯‘𝐵) − 1)) |
| 37 | 25, 36 | eqtrd 2777 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (((♯‘(𝐴 ++ 𝐵)) − 1) − (♯‘𝐴)) = ((♯‘𝐵) − 1)) |
| 38 | 37 | 3adant3 1133 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) →
(((♯‘(𝐴 ++
𝐵)) − 1) −
(♯‘𝐴)) =
((♯‘𝐵) −
1)) |
| 39 | 38 | fveq2d 6910 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (𝐵‘(((♯‘(𝐴 ++ 𝐵)) − 1) − (♯‘𝐴))) = (𝐵‘((♯‘𝐵) − 1))) |
| 40 | 24, 39 | eqtrd 2777 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘((♯‘(𝐴 ++ 𝐵)) − 1)) = (𝐵‘((♯‘𝐵) − 1))) |
| 41 | | ovex 7464 |
. . 3
⊢ (𝐴 ++ 𝐵) ∈ V |
| 42 | | lsw 14602 |
. . 3
⊢ ((𝐴 ++ 𝐵) ∈ V → (lastS‘(𝐴 ++ 𝐵)) = ((𝐴 ++ 𝐵)‘((♯‘(𝐴 ++ 𝐵)) − 1))) |
| 43 | 41, 42 | mp1i 13 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (lastS‘(𝐴 ++ 𝐵)) = ((𝐴 ++ 𝐵)‘((♯‘(𝐴 ++ 𝐵)) − 1))) |
| 44 | | lsw 14602 |
. . 3
⊢ (𝐵 ∈ Word 𝑉 → (lastS‘𝐵) = (𝐵‘((♯‘𝐵) − 1))) |
| 45 | 44 | 3ad2ant2 1135 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (lastS‘𝐵) = (𝐵‘((♯‘𝐵) − 1))) |
| 46 | 40, 43, 45 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (lastS‘(𝐴 ++ 𝐵)) = (lastS‘𝐵)) |