Metamath Proof Explorer

Theorem swrdlen2

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

Ref Expression
Assertion swrdlen2 ⊢ S ∈ Word V ∧ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F ∧ L ≤ S → S substr F L = L − F

Proof

Step Hyp Ref Expression
1 simp1 ⊢ S ∈ Word V ∧ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F ∧ L ≤ S → S ∈ Word V
2 simpl ⊢ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F → F ∈ ℕ 0
3 eluznn0 ⊢ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F → L ∈ ℕ 0
4 eluzle ⊢ L ∈ ℤ ≥ F → F ≤ L
5 4 adantl ⊢ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F → F ≤ L
6 2 3 5 3jca ⊢ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F → F ∈ ℕ 0 ∧ L ∈ ℕ 0 ∧ F ≤ L
7 6 3ad2ant2 ⊢ S ∈ Word V ∧ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F ∧ L ≤ S → F ∈ ℕ 0 ∧ L ∈ ℕ 0 ∧ F ≤ L
8 elfz2nn0 ⊢ F ∈ 0 … L ↔ F ∈ ℕ 0 ∧ L ∈ ℕ 0 ∧ F ≤ L
9 7 8 sylibr ⊢ S ∈ Word V ∧ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F ∧ L ≤ S → F ∈ 0 … L
10 3 3ad2ant2 ⊢ S ∈ Word V ∧ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F ∧ L ≤ S → L ∈ ℕ 0
11 lencl ⊢ S ∈ Word V → S ∈ ℕ 0
12 11 3ad2ant1 ⊢ S ∈ Word V ∧ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F ∧ L ≤ S → S ∈ ℕ 0
13 simp3 ⊢ S ∈ Word V ∧ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F ∧ L ≤ S → L ≤ S
14 10 12 13 3jca ⊢ S ∈ Word V ∧ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F ∧ L ≤ S → L ∈ ℕ 0 ∧ S ∈ ℕ 0 ∧ L ≤ S
15 elfz2nn0 ⊢ L ∈ 0 … S ↔ L ∈ ℕ 0 ∧ S ∈ ℕ 0 ∧ L ≤ S
16 14 15 sylibr ⊢ S ∈ Word V ∧ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F ∧ L ≤ S → L ∈ 0 … S
17 swrdlen ⊢ S ∈ Word V ∧ F ∈ 0 … L ∧ L ∈ 0 … S → S substr F L = L − F
18 1 9 16 17 syl3anc ⊢ S ∈ Word V ∧ F ∈ ℕ 0 ∧ L ∈ ℤ ≥ F ∧ L ≤ S → S substr F L = L − F