Step |
Hyp |
Ref |
Expression |
1 |
|
elfzofz |
|- ( F e. ( 0 ..^ L ) -> F e. ( 0 ... L ) ) |
2 |
1
|
3anim2i |
|- ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) ) |
3 |
|
fzonnsub |
|- ( F e. ( 0 ..^ L ) -> ( L - F ) e. NN ) |
4 |
3
|
3ad2ant2 |
|- ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( L - F ) e. NN ) |
5 |
|
lbfzo0 |
|- ( 0 e. ( 0 ..^ ( L - F ) ) <-> ( L - F ) e. NN ) |
6 |
4 5
|
sylibr |
|- ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> 0 e. ( 0 ..^ ( L - F ) ) ) |
7 |
|
swrdfv |
|- ( ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) /\ 0 e. ( 0 ..^ ( L - F ) ) ) -> ( ( S substr <. F , L >. ) ` 0 ) = ( S ` ( 0 + F ) ) ) |
8 |
2 6 7
|
syl2anc |
|- ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( ( S substr <. F , L >. ) ` 0 ) = ( S ` ( 0 + F ) ) ) |
9 |
|
elfzoelz |
|- ( F e. ( 0 ..^ L ) -> F e. ZZ ) |
10 |
9
|
zcnd |
|- ( F e. ( 0 ..^ L ) -> F e. CC ) |
11 |
10
|
addid2d |
|- ( F e. ( 0 ..^ L ) -> ( 0 + F ) = F ) |
12 |
11
|
fveq2d |
|- ( F e. ( 0 ..^ L ) -> ( S ` ( 0 + F ) ) = ( S ` F ) ) |
13 |
12
|
3ad2ant2 |
|- ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S ` ( 0 + F ) ) = ( S ` F ) ) |
14 |
8 13
|
eqtrd |
|- ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( ( S substr <. F , L >. ) ` 0 ) = ( S ` F ) ) |