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 ⊢ W ∈ Word V ∧ N ∈ ℕ 0 → W ++ ⟨“ X ”⟩ = N + 1 ↔ W = N

Proof

Step Hyp Ref Expression
1 ccatws1len ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ = W + 1
2 1 adantr ⊢ W ∈ Word V ∧ N ∈ ℕ 0 → W ++ ⟨“ X ”⟩ = W + 1
3 2 eqeq1d ⊢ W ∈ Word V ∧ N ∈ ℕ 0 → W ++ ⟨“ X ”⟩ = N + 1 ↔ W + 1 = N + 1
4 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
5 4 nn0cnd ⊢ W ∈ Word V → W ∈ ℂ
6 5 adantr ⊢ W ∈ Word V ∧ N ∈ ℕ 0 → W ∈ ℂ
7 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
8 7 adantl ⊢ W ∈ Word V ∧ N ∈ ℕ 0 → N ∈ ℂ
9 1cnd ⊢ W ∈ Word V ∧ N ∈ ℕ 0 → 1 ∈ ℂ
10 6 8 9 addcan2d ⊢ W ∈ Word V ∧ N ∈ ℕ 0 → W + 1 = N + 1 ↔ W = N
11 3 10 bitrd ⊢ W ∈ Word V ∧ N ∈ ℕ 0 → W ++ ⟨“ X ”⟩ = N + 1 ↔ W = N