Metamath Proof Explorer

Theorem swrdrlen

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

Ref Expression
Assertion swrdrlen ⊢ W ∈ Word V ∧ I ∈ 0 … W → W substr I W = W − I

Proof

Step Hyp Ref Expression
1 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
2 nn0fz0 ⊢ W ∈ ℕ 0 ↔ W ∈ 0 … W
3 1 2 sylib ⊢ W ∈ Word V → W ∈ 0 … W
4 3 adantr ⊢ W ∈ Word V ∧ I ∈ 0 … W → W ∈ 0 … W
5 swrdlen ⊢ W ∈ Word V ∧ I ∈ 0 … W ∧ W ∈ 0 … W → W substr I W = W − I
6 4 5 mpd3an3 ⊢ W ∈ Word V ∧ I ∈ 0 … W → W substr I W = W − I