| 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 ) ) |