Metamath Proof Explorer

Theorem addlenpfx

Description: The sum of the lengths of two parts of a word is the length of the word. (Contributed by AV, 21-Oct-2018) (Revised by AV, 3-May-2020)

		Ref	Expression
	Assertion	addlenpfx	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to \|W prefix M\| + \|W substr ⟨M, \|W\|⟩\| = \|W\|$

Proof

Step	Hyp	Ref	Expression
1		pfxlen	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to \|W prefix M\| = M$
2		swrdrlen	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to \|W substr ⟨M, \|W\|⟩\| = \|W\| - M$
3	1 2	oveq12d	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to \|W prefix M\| + \|W substr ⟨M, \|W\|⟩\| = M + \|W\| - M$
4		elfznn0	$⊢ M \in (0 \dots \|W\|) \to M \in ℕ_{0}$
5	4	nn0cnd	$⊢ M \in (0 \dots \|W\|) \to M \in ℂ$
6		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
7	6	nn0cnd	$⊢ W \in Word V \to \|W\| \in ℂ$
8		pncan3	$⊢ (M \in ℂ \land \|W\| \in ℂ) \to M + \|W\| - M = \|W\|$
9	5 7 8	syl2anr	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to M + \|W\| - M = \|W\|$
10	3 9	eqtrd	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to \|W prefix M\| + \|W substr ⟨M, \|W\|⟩\| = \|W\|$