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 \in Word V \land N \in ℕ_{0}) \to (\|W ++ ⟨“ X ”⟩\| = N + 1 \leftrightarrow \|W\| = N)$

Proof

Step	Hyp	Ref	Expression
1		ccatws1len	$⊢ W \in Word V \to \|W ++ ⟨“ X ”⟩\| = \|W\| + 1$
2	1	adantr	$⊢ (W \in Word V \land N \in ℕ_{0}) \to \|W ++ ⟨“ X ”⟩\| = \|W\| + 1$
3	2	eqeq1d	$⊢ (W \in Word V \land N \in ℕ_{0}) \to (\|W ++ ⟨“ X ”⟩\| = N + 1 \leftrightarrow \|W\| + 1 = N + 1)$
4		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
5	4	nn0cnd	$⊢ W \in Word V \to \|W\| \in ℂ$
6	5	adantr	$⊢ (W \in Word V \land N \in ℕ_{0}) \to \|W\| \in ℂ$
7		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
8	7	adantl	$⊢ (W \in Word V \land N \in ℕ_{0}) \to N \in ℂ$
9		1cnd	$⊢ (W \in Word V \land N \in ℕ_{0}) \to 1 \in ℂ$
10	6 8 9	addcan2d	$⊢ (W \in Word V \land N \in ℕ_{0}) \to (\|W\| + 1 = N + 1 \leftrightarrow \|W\| = N)$
11	3 10	bitrd	$⊢ (W \in Word V \land N \in ℕ_{0}) \to (\|W ++ ⟨“ X ”⟩\| = N + 1 \leftrightarrow \|W\| = N)$