swrdrlen

Description: Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018)

		Ref	Expression
	Assertion	swrdrlen	$⊢ (W \in Word V \land I \in (0 \dots \|W\|)) \to \|W substr ⟨I, \|W\|⟩\| = \|W\| - I$

Step	Hyp	Ref	Expression
1		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
2		nn0fz0	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in (0 \dots \|W\|)$
3	1 2	sylib	$⊢ W \in Word V \to \|W\| \in (0 \dots \|W\|)$
4	3	adantr	$⊢ (W \in Word V \land I \in (0 \dots \|W\|)) \to \|W\| \in (0 \dots \|W\|)$
5		swrdlen	$⊢ (W \in Word V \land I \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|W\|)) \to \|W substr ⟨I, \|W\|⟩\| = \|W\| - I$
6	4 5	mpd3an3	$⊢ (W \in Word V \land I \in (0 \dots \|W\|)) \to \|W substr ⟨I, \|W\|⟩\| = \|W\| - I$

Metamath Proof Explorer