Metamath Proof Explorer


Theorem ccatws1lenp1b

Description: The length of a word is N iff the length of the concatenation of the word with a singleton word is N + 1 . (Contributed by AV, 4-Mar-2022)

Ref Expression
Assertion ccatws1lenp1b ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ 𝑊 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 ccatws1len ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
2 1 adantr ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
3 2 eqeq1d ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ↔ ( ( ♯ ‘ 𝑊 ) + 1 ) = ( 𝑁 + 1 ) ) )
4 lencl ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
5 4 nn0cnd ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
6 5 adantr ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℕ0 ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
7 nn0cn ( 𝑁 ∈ ℕ0𝑁 ∈ ℂ )
8 7 adantl ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
9 1cnd ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℕ0 ) → 1 ∈ ℂ )
10 6 8 9 addcan2d ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
11 3 10 bitrd ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ 𝑊 ) = 𝑁 ) )