This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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