This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem swrdlen2

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

Ref Expression
Assertion swrdlen2 ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝐹 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝑆 ∈ Word 𝑉 )
2 simpl ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → 𝐹 ∈ ℕ0 )
3 eluznn0 ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → 𝐿 ∈ ℕ0 )
4 eluzle ⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) → 𝐹 ≤ 𝐿 )
5 4 adantl ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → 𝐹 ≤ 𝐿 )
6 2 3 5 3jca ⊢ ( ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) → ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) )
7 6 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) )
8 elfz2nn0 ⊢ ( 𝐹 ∈ ( 0 ... 𝐿 ) ↔ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐹 ≤ 𝐿 ) )
9 7 8 sylibr ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝐹 ∈ ( 0 ... 𝐿 ) )
10 3 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝐿 ∈ ℕ0 )
11 lencl ⊢ ( 𝑆 ∈ Word 𝑉 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
12 11 3ad2ant1 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
13 simp3 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝐿 ≤ ( ♯ ‘ 𝑆 ) )
14 10 12 13 3jca ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) )
15 elfz2nn0 ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ↔ ( 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) )
16 14 15 sylibr ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
17 swrdlen ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝐹 ) )
18 1 9 16 17 syl3anc ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ( ℤ≥ ‘ 𝐹 ) ) ∧ 𝐿 ≤ ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝐹 ) )