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