Metamath Proof Explorer

Theorem swrdlen2

Description: Length of an extracted subword. (Contributed by AV, 5-May-2020)

		Ref	Expression
	Assertion	swrdlen2	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to \|S substr ⟨F, L⟩\| = L - F$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to S \in Word V$
2		simpl	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to F \in ℕ_{0}$
3		eluznn0	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to L \in ℕ_{0}$
4		eluzle	$⊢ L \in ℤ_{\geq F} \to F \leq L$
5	4	adantl	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to F \leq L$
6	2 3 5	3jca	$⊢ (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \to (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L)$
7	6	3ad2ant2	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L)$
8		elfz2nn0	$⊢ F \in (0 \dots L) \leftrightarrow (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L)$
9	7 8	sylibr	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to F \in (0 \dots L)$
10	3	3ad2ant2	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to L \in ℕ_{0}$
11		lencl	$⊢ S \in Word V \to \|S\| \in ℕ_{0}$
12	11	3ad2ant1	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to \|S\| \in ℕ_{0}$
13		simp3	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to L \leq \|S\|$
14	10 12 13	3jca	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to (L \in ℕ_{0} \land \|S\| \in ℕ_{0} \land L \leq \|S\|)$
15		elfz2nn0	$⊢ L \in (0 \dots \|S\|) \leftrightarrow (L \in ℕ_{0} \land \|S\| \in ℕ_{0} \land L \leq \|S\|)$
16	14 15	sylibr	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to L \in (0 \dots \|S\|)$
17		swrdlen	$⊢ (S \in Word V \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to \|S substr ⟨F, L⟩\| = L - F$
18	1 9 16 17	syl3anc	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℤ_{\geq F}) \land L \leq \|S\|) \to \|S substr ⟨F, L⟩\| = L - F$