Step |
Hyp |
Ref |
Expression |
1 |
|
simpr1 |
|- ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( W e. Word V /\ U e. Word V ) ) |
2 |
|
simpr2 |
|- ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( M e. NN0 /\ N e. NN0 ) ) |
3 |
|
simpl |
|- ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> N <_ M ) |
4 |
|
swrdsb0eq |
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ M ) -> ( W substr <. M , N >. ) = ( U substr <. M , N >. ) ) |
5 |
1 2 3 4
|
syl3anc |
|- ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( W substr <. M , N >. ) = ( U substr <. M , N >. ) ) |
6 |
5
|
fveq2d |
|- ( ( N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) ) |
7 |
|
nn0re |
|- ( M e. NN0 -> M e. RR ) |
8 |
|
nn0re |
|- ( N e. NN0 -> N e. RR ) |
9 |
|
ltnle |
|- ( ( M e. RR /\ N e. RR ) -> ( M < N <-> -. N <_ M ) ) |
10 |
|
ltle |
|- ( ( M e. RR /\ N e. RR ) -> ( M < N -> M <_ N ) ) |
11 |
9 10
|
sylbird |
|- ( ( M e. RR /\ N e. RR ) -> ( -. N <_ M -> M <_ N ) ) |
12 |
7 8 11
|
syl2an |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( -. N <_ M -> M <_ N ) ) |
13 |
12
|
3ad2ant2 |
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( -. N <_ M -> M <_ N ) ) |
14 |
|
simpl1l |
|- ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> W e. Word V ) |
15 |
|
simpl2l |
|- ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> M e. NN0 ) |
16 |
|
nn0z |
|- ( M e. NN0 -> M e. ZZ ) |
17 |
|
nn0z |
|- ( N e. NN0 -> N e. ZZ ) |
18 |
16 17
|
anim12i |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M e. ZZ /\ N e. ZZ ) ) |
19 |
18
|
3ad2ant2 |
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( M e. ZZ /\ N e. ZZ ) ) |
20 |
19
|
anim1i |
|- ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( ( M e. ZZ /\ N e. ZZ ) /\ M <_ N ) ) |
21 |
|
df-3an |
|- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) <-> ( ( M e. ZZ /\ N e. ZZ ) /\ M <_ N ) ) |
22 |
20 21
|
sylibr |
|- ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) ) |
23 |
|
eluz2 |
|- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) ) |
24 |
22 23
|
sylibr |
|- ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> N e. ( ZZ>= ` M ) ) |
25 |
|
simpl3l |
|- ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> N <_ ( # ` W ) ) |
26 |
|
swrdlen2 |
|- ( ( W e. Word V /\ ( M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ N <_ ( # ` W ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( N - M ) ) |
27 |
14 15 24 25 26
|
syl121anc |
|- ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( # ` ( W substr <. M , N >. ) ) = ( N - M ) ) |
28 |
|
simpl1r |
|- ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> U e. Word V ) |
29 |
|
simpl3r |
|- ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> N <_ ( # ` U ) ) |
30 |
|
swrdlen2 |
|- ( ( U e. Word V /\ ( M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ N <_ ( # ` U ) ) -> ( # ` ( U substr <. M , N >. ) ) = ( N - M ) ) |
31 |
28 15 24 29 30
|
syl121anc |
|- ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( # ` ( U substr <. M , N >. ) ) = ( N - M ) ) |
32 |
27 31
|
eqtr4d |
|- ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M <_ N ) -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) ) |
33 |
32
|
ex |
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( M <_ N -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) ) ) |
34 |
13 33
|
syld |
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( -. N <_ M -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) ) ) |
35 |
34
|
impcom |
|- ( ( -. N <_ M /\ ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) ) |
36 |
6 35
|
pm2.61ian |
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( N <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( # ` ( U substr <. M , N >. ) ) ) |