Description: The length of a word is the length of the word concatenated with a singleton word minus 1. (Contributed by AV, 28-Jun-2018) (Revised by AV, 5-Mar-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wrdlenccats1lenm1 | ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) = ( ♯ ‘ 𝑊 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ccatws1len | ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) | |
| 2 | 1 | oveq1d | ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) ) |
| 3 | lencl | ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) | |
| 4 | 3 | nn0cnd | ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℂ ) |
| 5 | pncan1 | ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( ♯ ‘ 𝑊 ) ) | |
| 6 | 4 5 | syl | ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ( ♯ ‘ 𝑊 ) + 1 ) − 1 ) = ( ♯ ‘ 𝑊 ) ) |
| 7 | 2 6 | eqtrd | ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) − 1 ) = ( ♯ ‘ 𝑊 ) ) |