Metamath Proof Explorer


Theorem repswswrd

Description: A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption N <_ L is required, because otherwise ( L < N ) : ( ( S repeatS L ) substr <. M , N >. ) = (/) , but for M < N ( S repeatS ( N - M ) ) ) =/= (/) ! The proof is relatively long because the border cases ( M = N , -. ( M ..^ N ) C_ ( 0 ..^ L ) must have been considered. (Contributed by AV, 6-Nov-2018)

Ref Expression
Assertion repswswrd
|- ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( ( S repeatS L ) substr <. M , N >. ) = ( S repeatS ( N - M ) ) )

Proof

Step Hyp Ref Expression
1 repsw
 |-  ( ( S e. V /\ L e. NN0 ) -> ( S repeatS L ) e. Word V )
2 nn0z
 |-  ( M e. NN0 -> M e. ZZ )
3 nn0z
 |-  ( N e. NN0 -> N e. ZZ )
4 2 3 anim12i
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M e. ZZ /\ N e. ZZ ) )
5 1 4 anim12i
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( S repeatS L ) e. Word V /\ ( M e. ZZ /\ N e. ZZ ) ) )
6 3anass
 |-  ( ( ( S repeatS L ) e. Word V /\ M e. ZZ /\ N e. ZZ ) <-> ( ( S repeatS L ) e. Word V /\ ( M e. ZZ /\ N e. ZZ ) ) )
7 5 6 sylibr
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( S repeatS L ) e. Word V /\ M e. ZZ /\ N e. ZZ ) )
8 7 3adant3
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( ( S repeatS L ) e. Word V /\ M e. ZZ /\ N e. ZZ ) )
9 swrdval
 |-  ( ( ( S repeatS L ) e. Word V /\ M e. ZZ /\ N e. ZZ ) -> ( ( S repeatS L ) substr <. M , N >. ) = if ( ( M ..^ N ) C_ dom ( S repeatS L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) )
10 8 9 syl
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( ( S repeatS L ) substr <. M , N >. ) = if ( ( M ..^ N ) C_ dom ( S repeatS L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) )
11 repsf
 |-  ( ( S e. V /\ L e. NN0 ) -> ( S repeatS L ) : ( 0 ..^ L ) --> V )
12 11 3ad2ant1
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( S repeatS L ) : ( 0 ..^ L ) --> V )
13 12 fdmd
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> dom ( S repeatS L ) = ( 0 ..^ L ) )
14 13 sseq2d
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( ( M ..^ N ) C_ dom ( S repeatS L ) <-> ( M ..^ N ) C_ ( 0 ..^ L ) ) )
15 14 ifbid
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> if ( ( M ..^ N ) C_ dom ( S repeatS L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) )
16 fzon
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N <_ M <-> ( M ..^ N ) = (/) ) )
17 4 16 syl
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N <_ M <-> ( M ..^ N ) = (/) ) )
18 17 adantl
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( N <_ M <-> ( M ..^ N ) = (/) ) )
19 18 biimpac
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( M ..^ N ) = (/) )
20 0ss
 |-  (/) C_ ( 0 ..^ L )
21 19 20 eqsstrdi
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( M ..^ N ) C_ ( 0 ..^ L ) )
22 iftrue
 |-  ( ( M ..^ N ) C_ ( 0 ..^ L ) -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) )
23 21 22 syl
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) )
24 nn0re
 |-  ( M e. NN0 -> M e. RR )
25 nn0re
 |-  ( N e. NN0 -> N e. RR )
26 24 25 anim12ci
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N e. RR /\ M e. RR ) )
27 26 adantl
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( N e. RR /\ M e. RR ) )
28 suble0
 |-  ( ( N e. RR /\ M e. RR ) -> ( ( N - M ) <_ 0 <-> N <_ M ) )
29 27 28 syl
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( N - M ) <_ 0 <-> N <_ M ) )
30 29 biimparc
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( N - M ) <_ 0 )
31 0z
 |-  0 e. ZZ
32 zsubcl
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N - M ) e. ZZ )
33 3 2 32 syl2anr
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N - M ) e. ZZ )
34 33 adantl
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( N - M ) e. ZZ )
35 34 adantl
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( N - M ) e. ZZ )
36 fzon
 |-  ( ( 0 e. ZZ /\ ( N - M ) e. ZZ ) -> ( ( N - M ) <_ 0 <-> ( 0 ..^ ( N - M ) ) = (/) ) )
37 31 35 36 sylancr
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( ( N - M ) <_ 0 <-> ( 0 ..^ ( N - M ) ) = (/) ) )
38 30 37 mpbid
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( 0 ..^ ( N - M ) ) = (/) )
39 38 mpteq1d
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) = ( x e. (/) |-> ( ( S repeatS L ) ` ( x + M ) ) ) )
40 mpt0
 |-  ( x e. (/) |-> ( ( S repeatS L ) ` ( x + M ) ) ) = (/)
41 oveq2
 |-  ( M = N -> ( N - M ) = ( N - N ) )
42 41 oveq2d
 |-  ( M = N -> ( S repeatS ( N - M ) ) = ( S repeatS ( N - N ) ) )
43 nn0cn
 |-  ( N e. NN0 -> N e. CC )
44 43 adantl
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> N e. CC )
45 44 subidd
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N - N ) = 0 )
46 45 adantl
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( N - N ) = 0 )
47 46 oveq2d
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( S repeatS ( N - N ) ) = ( S repeatS 0 ) )
48 repsw0
 |-  ( S e. V -> ( S repeatS 0 ) = (/) )
49 48 ad2antrr
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( S repeatS 0 ) = (/) )
50 47 49 eqtrd
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( S repeatS ( N - N ) ) = (/) )
51 42 50 sylan9eqr
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) /\ M = N ) -> ( S repeatS ( N - M ) ) = (/) )
52 51 ex
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( M = N -> ( S repeatS ( N - M ) ) = (/) ) )
53 52 adantl
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( M = N -> ( S repeatS ( N - M ) ) = (/) ) )
54 53 com12
 |-  ( M = N -> ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( S repeatS ( N - M ) ) = (/) ) )
55 elnn0z
 |-  ( ( N - M ) e. NN0 <-> ( ( N - M ) e. ZZ /\ 0 <_ ( N - M ) ) )
56 subge0
 |-  ( ( N e. RR /\ M e. RR ) -> ( 0 <_ ( N - M ) <-> M <_ N ) )
57 25 24 56 syl2anr
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( 0 <_ ( N - M ) <-> M <_ N ) )
58 24 25 anim12i
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M e. RR /\ N e. RR ) )
59 letri3
 |-  ( ( M e. RR /\ N e. RR ) -> ( M = N <-> ( M <_ N /\ N <_ M ) ) )
60 58 59 syl
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M = N <-> ( M <_ N /\ N <_ M ) ) )
61 60 biimprd
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M <_ N /\ N <_ M ) -> M = N ) )
62 61 expd
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N -> ( N <_ M -> M = N ) ) )
63 57 62 sylbid
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( 0 <_ ( N - M ) -> ( N <_ M -> M = N ) ) )
64 63 com23
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N <_ M -> ( 0 <_ ( N - M ) -> M = N ) ) )
65 64 adantl
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( N <_ M -> ( 0 <_ ( N - M ) -> M = N ) ) )
66 65 impcom
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( 0 <_ ( N - M ) -> M = N ) )
67 66 com12
 |-  ( 0 <_ ( N - M ) -> ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> M = N ) )
68 55 67 simplbiim
 |-  ( ( N - M ) e. NN0 -> ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> M = N ) )
69 68 com12
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( ( N - M ) e. NN0 -> M = N ) )
70 69 con3d
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( -. M = N -> -. ( N - M ) e. NN0 ) )
71 70 impcom
 |-  ( ( -. M = N /\ ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) ) -> -. ( N - M ) e. NN0 )
72 df-nel
 |-  ( ( N - M ) e/ NN0 <-> -. ( N - M ) e. NN0 )
73 71 72 sylibr
 |-  ( ( -. M = N /\ ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) ) -> ( N - M ) e/ NN0 )
74 repsundef
 |-  ( ( N - M ) e/ NN0 -> ( S repeatS ( N - M ) ) = (/) )
75 73 74 syl
 |-  ( ( -. M = N /\ ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) ) -> ( S repeatS ( N - M ) ) = (/) )
76 75 ex
 |-  ( -. M = N -> ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( S repeatS ( N - M ) ) = (/) ) )
77 54 76 pm2.61i
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( S repeatS ( N - M ) ) = (/) )
78 40 77 eqtr4id
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( x e. (/) |-> ( ( S repeatS L ) ` ( x + M ) ) ) = ( S repeatS ( N - M ) ) )
79 23 39 78 3eqtrd
 |-  ( ( N <_ M /\ ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( S repeatS ( N - M ) ) )
80 79 expcom
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( N <_ M -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( S repeatS ( N - M ) ) ) )
81 80 3adant3
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( N <_ M -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( S repeatS ( N - M ) ) ) )
82 ltnle
 |-  ( ( M e. RR /\ N e. RR ) -> ( M < N <-> -. N <_ M ) )
83 58 82 syl
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M < N <-> -. N <_ M ) )
84 83 bicomd
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( -. N <_ M <-> M < N ) )
85 84 3ad2ant2
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( -. N <_ M <-> M < N ) )
86 22 adantr
 |-  ( ( ( M ..^ N ) C_ ( 0 ..^ L ) /\ ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) ) -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) )
87 4 3ad2ant2
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( M e. ZZ /\ N e. ZZ ) )
88 87 adantr
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( M e. ZZ /\ N e. ZZ ) )
89 0zd
 |-  ( S e. V -> 0 e. ZZ )
90 nn0z
 |-  ( L e. NN0 -> L e. ZZ )
91 89 90 anim12i
 |-  ( ( S e. V /\ L e. NN0 ) -> ( 0 e. ZZ /\ L e. ZZ ) )
92 91 3ad2ant1
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( 0 e. ZZ /\ L e. ZZ ) )
93 92 adantr
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( 0 e. ZZ /\ L e. ZZ ) )
94 simpr
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> M < N )
95 ssfzo12bi
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( 0 e. ZZ /\ L e. ZZ ) /\ M < N ) -> ( ( M ..^ N ) C_ ( 0 ..^ L ) <-> ( 0 <_ M /\ N <_ L ) ) )
96 88 93 94 95 syl3anc
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( ( M ..^ N ) C_ ( 0 ..^ L ) <-> ( 0 <_ M /\ N <_ L ) ) )
97 simpl1l
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> S e. V )
98 97 ad2antrr
 |-  ( ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> S e. V )
99 simpl1r
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> L e. NN0 )
100 99 ad2antrr
 |-  ( ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> L e. NN0 )
101 nn0addcl
 |-  ( ( x e. NN0 /\ M e. NN0 ) -> ( x + M ) e. NN0 )
102 101 expcom
 |-  ( M e. NN0 -> ( x e. NN0 -> ( x + M ) e. NN0 ) )
103 102 adantr
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( x e. NN0 -> ( x + M ) e. NN0 ) )
104 103 3ad2ant2
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( x e. NN0 -> ( x + M ) e. NN0 ) )
105 104 ad2antrr
 |-  ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) -> ( x e. NN0 -> ( x + M ) e. NN0 ) )
106 elfzonn0
 |-  ( x e. ( 0 ..^ ( N - M ) ) -> x e. NN0 )
107 105 106 impel
 |-  ( ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. NN0 )
108 90 adantl
 |-  ( ( S e. V /\ L e. NN0 ) -> L e. ZZ )
109 108 3ad2ant1
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> L e. ZZ )
110 109 adantr
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> L e. ZZ )
111 nn0re
 |-  ( L e. NN0 -> L e. RR )
112 111 adantl
 |-  ( ( S e. V /\ L e. NN0 ) -> L e. RR )
113 112 58 anim12ci
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( M e. RR /\ N e. RR ) /\ L e. RR ) )
114 df-3an
 |-  ( ( M e. RR /\ N e. RR /\ L e. RR ) <-> ( ( M e. RR /\ N e. RR ) /\ L e. RR ) )
115 113 114 sylibr
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( M e. RR /\ N e. RR /\ L e. RR ) )
116 ltletr
 |-  ( ( M e. RR /\ N e. RR /\ L e. RR ) -> ( ( M < N /\ N <_ L ) -> M < L ) )
117 115 116 syl
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( M < N /\ N <_ L ) -> M < L ) )
118 elnn0z
 |-  ( M e. NN0 <-> ( M e. ZZ /\ 0 <_ M ) )
119 0red
 |-  ( ( M e. ZZ /\ ( S e. V /\ L e. NN0 ) ) -> 0 e. RR )
120 zre
 |-  ( M e. ZZ -> M e. RR )
121 120 adantr
 |-  ( ( M e. ZZ /\ ( S e. V /\ L e. NN0 ) ) -> M e. RR )
122 112 adantl
 |-  ( ( M e. ZZ /\ ( S e. V /\ L e. NN0 ) ) -> L e. RR )
123 lelttr
 |-  ( ( 0 e. RR /\ M e. RR /\ L e. RR ) -> ( ( 0 <_ M /\ M < L ) -> 0 < L ) )
124 119 121 122 123 syl3anc
 |-  ( ( M e. ZZ /\ ( S e. V /\ L e. NN0 ) ) -> ( ( 0 <_ M /\ M < L ) -> 0 < L ) )
125 124 expd
 |-  ( ( M e. ZZ /\ ( S e. V /\ L e. NN0 ) ) -> ( 0 <_ M -> ( M < L -> 0 < L ) ) )
126 125 impancom
 |-  ( ( M e. ZZ /\ 0 <_ M ) -> ( ( S e. V /\ L e. NN0 ) -> ( M < L -> 0 < L ) ) )
127 118 126 sylbi
 |-  ( M e. NN0 -> ( ( S e. V /\ L e. NN0 ) -> ( M < L -> 0 < L ) ) )
128 127 adantr
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( S e. V /\ L e. NN0 ) -> ( M < L -> 0 < L ) ) )
129 128 impcom
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( M < L -> 0 < L ) )
130 117 129 syld
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( M < N /\ N <_ L ) -> 0 < L ) )
131 130 expcomd
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( N <_ L -> ( M < N -> 0 < L ) ) )
132 131 3impia
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( M < N -> 0 < L ) )
133 132 imp
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> 0 < L )
134 elnnz
 |-  ( L e. NN <-> ( L e. ZZ /\ 0 < L ) )
135 110 133 134 sylanbrc
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> L e. NN )
136 135 ad2antrr
 |-  ( ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> L e. NN )
137 elfzo0
 |-  ( x e. ( 0 ..^ ( N - M ) ) <-> ( x e. NN0 /\ ( N - M ) e. NN /\ x < ( N - M ) ) )
138 nn0readdcl
 |-  ( ( x e. NN0 /\ M e. NN0 ) -> ( x + M ) e. RR )
139 138 expcom
 |-  ( M e. NN0 -> ( x e. NN0 -> ( x + M ) e. RR ) )
140 139 ad2antrl
 |-  ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( x e. NN0 -> ( x + M ) e. RR ) )
141 140 impcom
 |-  ( ( x e. NN0 /\ ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( x + M ) e. RR )
142 25 adantl
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> N e. RR )
143 142 adantl
 |-  ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> N e. RR )
144 143 adantl
 |-  ( ( x e. NN0 /\ ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> N e. RR )
145 111 ad2antrl
 |-  ( ( x e. NN0 /\ ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> L e. RR )
146 141 144 145 3jca
 |-  ( ( x e. NN0 /\ ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( ( x + M ) e. RR /\ N e. RR /\ L e. RR ) )
147 146 ex
 |-  ( x e. NN0 -> ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( x + M ) e. RR /\ N e. RR /\ L e. RR ) ) )
148 147 adantr
 |-  ( ( x e. NN0 /\ x < ( N - M ) ) -> ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( x + M ) e. RR /\ N e. RR /\ L e. RR ) ) )
149 148 impcom
 |-  ( ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) /\ ( x e. NN0 /\ x < ( N - M ) ) ) -> ( ( x + M ) e. RR /\ N e. RR /\ L e. RR ) )
150 149 adantr
 |-  ( ( ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) /\ ( x e. NN0 /\ x < ( N - M ) ) ) /\ N <_ L ) -> ( ( x + M ) e. RR /\ N e. RR /\ L e. RR ) )
151 nn0re
 |-  ( x e. NN0 -> x e. RR )
152 151 adantr
 |-  ( ( x e. NN0 /\ ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> x e. RR )
153 24 ad2antrl
 |-  ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> M e. RR )
154 153 adantl
 |-  ( ( x e. NN0 /\ ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> M e. RR )
155 152 154 144 ltaddsubd
 |-  ( ( x e. NN0 /\ ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( ( x + M ) < N <-> x < ( N - M ) ) )
156 idd
 |-  ( ( ( x e. NN0 /\ ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) ) /\ N <_ L ) -> ( ( x + M ) < N -> ( x + M ) < N ) )
157 156 ex
 |-  ( ( x e. NN0 /\ ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( N <_ L -> ( ( x + M ) < N -> ( x + M ) < N ) ) )
158 157 com23
 |-  ( ( x e. NN0 /\ ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( ( x + M ) < N -> ( N <_ L -> ( x + M ) < N ) ) )
159 155 158 sylbird
 |-  ( ( x e. NN0 /\ ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) ) -> ( x < ( N - M ) -> ( N <_ L -> ( x + M ) < N ) ) )
160 159 impancom
 |-  ( ( x e. NN0 /\ x < ( N - M ) ) -> ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( N <_ L -> ( x + M ) < N ) ) )
161 160 impcom
 |-  ( ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) /\ ( x e. NN0 /\ x < ( N - M ) ) ) -> ( N <_ L -> ( x + M ) < N ) )
162 161 impac
 |-  ( ( ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) /\ ( x e. NN0 /\ x < ( N - M ) ) ) /\ N <_ L ) -> ( ( x + M ) < N /\ N <_ L ) )
163 ltletr
 |-  ( ( ( x + M ) e. RR /\ N e. RR /\ L e. RR ) -> ( ( ( x + M ) < N /\ N <_ L ) -> ( x + M ) < L ) )
164 150 162 163 sylc
 |-  ( ( ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) /\ ( x e. NN0 /\ x < ( N - M ) ) ) /\ N <_ L ) -> ( x + M ) < L )
165 164 exp31
 |-  ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( x e. NN0 /\ x < ( N - M ) ) -> ( N <_ L -> ( x + M ) < L ) ) )
166 165 com23
 |-  ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( N <_ L -> ( ( x e. NN0 /\ x < ( N - M ) ) -> ( x + M ) < L ) ) )
167 166 ex
 |-  ( L e. NN0 -> ( ( M e. NN0 /\ N e. NN0 ) -> ( N <_ L -> ( ( x e. NN0 /\ x < ( N - M ) ) -> ( x + M ) < L ) ) ) )
168 167 adantl
 |-  ( ( S e. V /\ L e. NN0 ) -> ( ( M e. NN0 /\ N e. NN0 ) -> ( N <_ L -> ( ( x e. NN0 /\ x < ( N - M ) ) -> ( x + M ) < L ) ) ) )
169 168 3imp
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( ( x e. NN0 /\ x < ( N - M ) ) -> ( x + M ) < L ) )
170 169 ad2antrr
 |-  ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) -> ( ( x e. NN0 /\ x < ( N - M ) ) -> ( x + M ) < L ) )
171 170 com12
 |-  ( ( x e. NN0 /\ x < ( N - M ) ) -> ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) -> ( x + M ) < L ) )
172 171 3adant2
 |-  ( ( x e. NN0 /\ ( N - M ) e. NN /\ x < ( N - M ) ) -> ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) -> ( x + M ) < L ) )
173 137 172 sylbi
 |-  ( x e. ( 0 ..^ ( N - M ) ) -> ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) -> ( x + M ) < L ) )
174 173 impcom
 |-  ( ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) < L )
175 elfzo0
 |-  ( ( x + M ) e. ( 0 ..^ L ) <-> ( ( x + M ) e. NN0 /\ L e. NN /\ ( x + M ) < L ) )
176 107 136 174 175 syl3anbrc
 |-  ( ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( x + M ) e. ( 0 ..^ L ) )
177 repswsymb
 |-  ( ( S e. V /\ L e. NN0 /\ ( x + M ) e. ( 0 ..^ L ) ) -> ( ( S repeatS L ) ` ( x + M ) ) = S )
178 98 100 176 177 syl3anc
 |-  ( ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) /\ x e. ( 0 ..^ ( N - M ) ) ) -> ( ( S repeatS L ) ` ( x + M ) ) = S )
179 178 mpteq2dva
 |-  ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) -> ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) = ( x e. ( 0 ..^ ( N - M ) ) |-> S ) )
180 33 3ad2ant2
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( N - M ) e. ZZ )
181 180 adantr
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( N - M ) e. ZZ )
182 58 3ad2ant2
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( M e. RR /\ N e. RR ) )
183 ltle
 |-  ( ( M e. RR /\ N e. RR ) -> ( M < N -> M <_ N ) )
184 182 183 syl
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( M < N -> M <_ N ) )
185 26 3ad2ant2
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( N e. RR /\ M e. RR ) )
186 185 56 syl
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( 0 <_ ( N - M ) <-> M <_ N ) )
187 184 186 sylibrd
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( M < N -> 0 <_ ( N - M ) ) )
188 187 imp
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> 0 <_ ( N - M ) )
189 181 188 55 sylanbrc
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( N - M ) e. NN0 )
190 97 189 jca
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( S e. V /\ ( N - M ) e. NN0 ) )
191 190 adantr
 |-  ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) -> ( S e. V /\ ( N - M ) e. NN0 ) )
192 reps
 |-  ( ( S e. V /\ ( N - M ) e. NN0 ) -> ( S repeatS ( N - M ) ) = ( x e. ( 0 ..^ ( N - M ) ) |-> S ) )
193 192 eqcomd
 |-  ( ( S e. V /\ ( N - M ) e. NN0 ) -> ( x e. ( 0 ..^ ( N - M ) ) |-> S ) = ( S repeatS ( N - M ) ) )
194 191 193 syl
 |-  ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) -> ( x e. ( 0 ..^ ( N - M ) ) |-> S ) = ( S repeatS ( N - M ) ) )
195 179 194 eqtrd
 |-  ( ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) /\ ( 0 <_ M /\ N <_ L ) ) -> ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) = ( S repeatS ( N - M ) ) )
196 195 ex
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( ( 0 <_ M /\ N <_ L ) -> ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) = ( S repeatS ( N - M ) ) ) )
197 96 196 sylbid
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( ( M ..^ N ) C_ ( 0 ..^ L ) -> ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) = ( S repeatS ( N - M ) ) ) )
198 197 impcom
 |-  ( ( ( M ..^ N ) C_ ( 0 ..^ L ) /\ ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) ) -> ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) = ( S repeatS ( N - M ) ) )
199 86 198 eqtrd
 |-  ( ( ( M ..^ N ) C_ ( 0 ..^ L ) /\ ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) ) -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( S repeatS ( N - M ) ) )
200 iffalse
 |-  ( -. ( M ..^ N ) C_ ( 0 ..^ L ) -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = (/) )
201 200 adantr
 |-  ( ( -. ( M ..^ N ) C_ ( 0 ..^ L ) /\ ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) ) -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = (/) )
202 96 notbid
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( -. ( M ..^ N ) C_ ( 0 ..^ L ) <-> -. ( 0 <_ M /\ N <_ L ) ) )
203 ianor
 |-  ( -. ( 0 <_ M /\ N <_ L ) <-> ( -. 0 <_ M \/ -. N <_ L ) )
204 nn0ge0
 |-  ( M e. NN0 -> 0 <_ M )
205 pm2.24
 |-  ( 0 <_ M -> ( -. 0 <_ M -> ( S repeatS ( N - M ) ) = (/) ) )
206 204 205 syl
 |-  ( M e. NN0 -> ( -. 0 <_ M -> ( S repeatS ( N - M ) ) = (/) ) )
207 206 adantr
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( -. 0 <_ M -> ( S repeatS ( N - M ) ) = (/) ) )
208 207 3ad2ant2
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( -. 0 <_ M -> ( S repeatS ( N - M ) ) = (/) ) )
209 208 adantr
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( -. 0 <_ M -> ( S repeatS ( N - M ) ) = (/) ) )
210 209 com12
 |-  ( -. 0 <_ M -> ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( S repeatS ( N - M ) ) = (/) ) )
211 pm2.24
 |-  ( N <_ L -> ( -. N <_ L -> ( S repeatS ( N - M ) ) = (/) ) )
212 211 3ad2ant3
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( -. N <_ L -> ( S repeatS ( N - M ) ) = (/) ) )
213 212 adantr
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( -. N <_ L -> ( S repeatS ( N - M ) ) = (/) ) )
214 213 com12
 |-  ( -. N <_ L -> ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( S repeatS ( N - M ) ) = (/) ) )
215 210 214 jaoi
 |-  ( ( -. 0 <_ M \/ -. N <_ L ) -> ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( S repeatS ( N - M ) ) = (/) ) )
216 203 215 sylbi
 |-  ( -. ( 0 <_ M /\ N <_ L ) -> ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( S repeatS ( N - M ) ) = (/) ) )
217 216 com12
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( -. ( 0 <_ M /\ N <_ L ) -> ( S repeatS ( N - M ) ) = (/) ) )
218 202 217 sylbid
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> ( -. ( M ..^ N ) C_ ( 0 ..^ L ) -> ( S repeatS ( N - M ) ) = (/) ) )
219 218 impcom
 |-  ( ( -. ( M ..^ N ) C_ ( 0 ..^ L ) /\ ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) ) -> ( S repeatS ( N - M ) ) = (/) )
220 201 219 eqtr4d
 |-  ( ( -. ( M ..^ N ) C_ ( 0 ..^ L ) /\ ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) ) -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( S repeatS ( N - M ) ) )
221 199 220 pm2.61ian
 |-  ( ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) /\ M < N ) -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( S repeatS ( N - M ) ) )
222 221 ex
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( M < N -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( S repeatS ( N - M ) ) ) )
223 85 222 sylbid
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( -. N <_ M -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( S repeatS ( N - M ) ) ) )
224 81 223 pm2.61d
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> if ( ( M ..^ N ) C_ ( 0 ..^ L ) , ( x e. ( 0 ..^ ( N - M ) ) |-> ( ( S repeatS L ) ` ( x + M ) ) ) , (/) ) = ( S repeatS ( N - M ) ) )
225 10 15 224 3eqtrd
 |-  ( ( ( S e. V /\ L e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) /\ N <_ L ) -> ( ( S repeatS L ) substr <. M , N >. ) = ( S repeatS ( N - M ) ) )