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