Metamath Proof Explorer


Theorem fz0fzdiffz0

Description: The difference of an integer in a finite set of sequential nonnegative integers and and an integer of a finite set of sequential integers with the same upper bound and the nonnegative integer as lower bound is a member of the finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 6-Jun-2018)

Ref Expression
Assertion fz0fzdiffz0
|- ( ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) -> ( K - M ) e. ( 0 ... N ) )

Proof

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