Metamath Proof Explorer

Theorem addlenrevpfx

Description: The sum of the lengths of two reversed parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018) (Revised by AV, 3-May-2020)

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

Proof

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