Step |
Hyp |
Ref |
Expression |
1 |
|
fz0fzelfz0 |
|- ( ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) -> K e. ( 0 ... N ) ) |
2 |
|
elfzle1 |
|- ( K e. ( M ... N ) -> M <_ K ) |
3 |
2
|
adantl |
|- ( ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) -> M <_ K ) |
4 |
3
|
adantl |
|- ( ( K e. ( 0 ... N ) /\ ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) ) -> M <_ K ) |
5 |
|
elfznn0 |
|- ( M e. ( 0 ... N ) -> M e. NN0 ) |
6 |
5
|
adantr |
|- ( ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) -> M e. NN0 ) |
7 |
|
elfznn0 |
|- ( K e. ( 0 ... N ) -> K e. NN0 ) |
8 |
|
nn0sub |
|- ( ( M e. NN0 /\ K e. NN0 ) -> ( M <_ K <-> ( K - M ) e. NN0 ) ) |
9 |
6 7 8
|
syl2anr |
|- ( ( K e. ( 0 ... N ) /\ ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) ) -> ( M <_ K <-> ( K - M ) e. NN0 ) ) |
10 |
4 9
|
mpbid |
|- ( ( K e. ( 0 ... N ) /\ ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) ) -> ( K - M ) e. NN0 ) |
11 |
|
elfz3nn0 |
|- ( K e. ( 0 ... N ) -> N e. NN0 ) |
12 |
11
|
adantr |
|- ( ( K e. ( 0 ... N ) /\ ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) ) -> N e. NN0 ) |
13 |
|
elfz2nn0 |
|- ( M e. ( 0 ... N ) <-> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) |
14 |
|
elfz2 |
|- ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) ) |
15 |
|
zsubcl |
|- ( ( K e. ZZ /\ M e. ZZ ) -> ( K - M ) e. ZZ ) |
16 |
15
|
zred |
|- ( ( K e. ZZ /\ M e. ZZ ) -> ( K - M ) e. RR ) |
17 |
16
|
ancoms |
|- ( ( M e. ZZ /\ K e. ZZ ) -> ( K - M ) e. RR ) |
18 |
17
|
3adant2 |
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( K - M ) e. RR ) |
19 |
|
zre |
|- ( K e. ZZ -> K e. RR ) |
20 |
19
|
3ad2ant3 |
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> K e. RR ) |
21 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
22 |
21
|
3ad2ant2 |
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> N e. RR ) |
23 |
18 20 22
|
3jca |
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( ( K - M ) e. RR /\ K e. RR /\ N e. RR ) ) |
24 |
23
|
adantr |
|- ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ M e. NN0 ) -> ( ( K - M ) e. RR /\ K e. RR /\ N e. RR ) ) |
25 |
24
|
adantr |
|- ( ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ M e. NN0 ) /\ K <_ N ) -> ( ( K - M ) e. RR /\ K e. RR /\ N e. RR ) ) |
26 |
|
nn0ge0 |
|- ( M e. NN0 -> 0 <_ M ) |
27 |
26
|
adantl |
|- ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ M e. NN0 ) -> 0 <_ M ) |
28 |
|
nn0re |
|- ( M e. NN0 -> M e. RR ) |
29 |
|
subge02 |
|- ( ( K e. RR /\ M e. RR ) -> ( 0 <_ M <-> ( K - M ) <_ K ) ) |
30 |
20 28 29
|
syl2an |
|- ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ M e. NN0 ) -> ( 0 <_ M <-> ( K - M ) <_ K ) ) |
31 |
27 30
|
mpbid |
|- ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ M e. NN0 ) -> ( K - M ) <_ K ) |
32 |
31
|
anim1i |
|- ( ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ M e. NN0 ) /\ K <_ N ) -> ( ( K - M ) <_ K /\ K <_ N ) ) |
33 |
|
letr |
|- ( ( ( K - M ) e. RR /\ K e. RR /\ N e. RR ) -> ( ( ( K - M ) <_ K /\ K <_ N ) -> ( K - M ) <_ N ) ) |
34 |
25 32 33
|
sylc |
|- ( ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ M e. NN0 ) /\ K <_ N ) -> ( K - M ) <_ N ) |
35 |
34
|
exp31 |
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M e. NN0 -> ( K <_ N -> ( K - M ) <_ N ) ) ) |
36 |
35
|
a1i |
|- ( N e. NN0 -> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M e. NN0 -> ( K <_ N -> ( K - M ) <_ N ) ) ) ) |
37 |
36
|
com14 |
|- ( K <_ N -> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M e. NN0 -> ( N e. NN0 -> ( K - M ) <_ N ) ) ) ) |
38 |
37
|
adantl |
|- ( ( M <_ K /\ K <_ N ) -> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M e. NN0 -> ( N e. NN0 -> ( K - M ) <_ N ) ) ) ) |
39 |
38
|
impcom |
|- ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) -> ( M e. NN0 -> ( N e. NN0 -> ( K - M ) <_ N ) ) ) |
40 |
14 39
|
sylbi |
|- ( K e. ( M ... N ) -> ( M e. NN0 -> ( N e. NN0 -> ( K - M ) <_ N ) ) ) |
41 |
40
|
com13 |
|- ( N e. NN0 -> ( M e. NN0 -> ( K e. ( M ... N ) -> ( K - M ) <_ N ) ) ) |
42 |
41
|
impcom |
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( K e. ( M ... N ) -> ( K - M ) <_ N ) ) |
43 |
42
|
3adant3 |
|- ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( K e. ( M ... N ) -> ( K - M ) <_ N ) ) |
44 |
13 43
|
sylbi |
|- ( M e. ( 0 ... N ) -> ( K e. ( M ... N ) -> ( K - M ) <_ N ) ) |
45 |
44
|
imp |
|- ( ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) -> ( K - M ) <_ N ) |
46 |
45
|
adantl |
|- ( ( K e. ( 0 ... N ) /\ ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) ) -> ( K - M ) <_ N ) |
47 |
10 12 46
|
3jca |
|- ( ( K e. ( 0 ... N ) /\ ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) ) -> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) ) |
48 |
1 47
|
mpancom |
|- ( ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) -> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) ) |
49 |
|
elfz2nn0 |
|- ( ( K - M ) e. ( 0 ... N ) <-> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) ) |
50 |
48 49
|
sylibr |
|- ( ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) -> ( K - M ) e. ( 0 ... N ) ) |