Metamath Proof Explorer

Theorem swrdlen2

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

Ref Expression
Assertion swrdlen2 
|- ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( # ` ( S substr <. F , L >. ) ) = ( L - F ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> S e. Word V )
2 simpl 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> F e. NN0 )
3 eluznn0 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> L e. NN0 )
4 eluzle 
 |-  ( L e. ( ZZ>= ` F ) -> F <_ L )
5 4 adantl 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> F <_ L )
6 2 3 5 3jca 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> ( F e. NN0 /\ L e. NN0 /\ F <_ L ) )
7 6 3ad2ant2 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( F e. NN0 /\ L e. NN0 /\ F <_ L ) )
8 elfz2nn0 
 |-  ( F e. ( 0 ... L ) <-> ( F e. NN0 /\ L e. NN0 /\ F <_ L ) )
9 7 8 sylibr 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> F e. ( 0 ... L ) )
10 3 3ad2ant2 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> L e. NN0 )
11 lencl 
 |-  ( S e. Word V -> ( # ` S ) e. NN0 )
12 11 3ad2ant1 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( # ` S ) e. NN0 )
13 simp3 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> L <_ ( # ` S ) )
14 10 12 13 3jca 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( L e. NN0 /\ ( # ` S ) e. NN0 /\ L <_ ( # ` S ) ) )
15 elfz2nn0 
 |-  ( L e. ( 0 ... ( # ` S ) ) <-> ( L e. NN0 /\ ( # ` S ) e. NN0 /\ L <_ ( # ` S ) ) )
16 14 15 sylibr 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> L e. ( 0 ... ( # ` S ) ) )
17 swrdlen 
 |-  ( ( S e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. F , L >. ) ) = ( L - F ) )
18 1 9 16 17 syl3anc 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( # ` ( S substr <. F , L >. ) ) = ( L - F ) )