Metamath Proof Explorer

Theorem difelfzle

Description: The difference of two integers from a finite set of sequential nonnegative integers is also element of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 12-Jun-2018)

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

Proof

Step Hyp Ref Expression
1 elfznn0 
 |-  ( K e. ( 0 ... N ) -> K e. NN0 )
2 elfznn0 
 |-  ( M e. ( 0 ... N ) -> M e. NN0 )
3 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
4 nn0z 
 |-  ( K e. NN0 -> K e. ZZ )
5 zsubcl 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M - K ) e. ZZ )
6 3 4 5 syl2anr 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( M - K ) e. ZZ )
7 6 adantr 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ K <_ M ) -> ( M - K ) e. ZZ )
8 nn0re 
 |-  ( M e. NN0 -> M e. RR )
9 nn0re 
 |-  ( K e. NN0 -> K e. RR )
10 subge0 
 |-  ( ( M e. RR /\ K e. RR ) -> ( 0 <_ ( M - K ) <-> K <_ M ) )
11 8 9 10 syl2anr 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( 0 <_ ( M - K ) <-> K <_ M ) )
12 11 biimpar 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ K <_ M ) -> 0 <_ ( M - K ) )
13 7 12 jca 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ K <_ M ) -> ( ( M - K ) e. ZZ /\ 0 <_ ( M - K ) ) )
14 13 exp31 
 |-  ( K e. NN0 -> ( M e. NN0 -> ( K <_ M -> ( ( M - K ) e. ZZ /\ 0 <_ ( M - K ) ) ) ) )
15 1 2 14 syl2im 
 |-  ( K e. ( 0 ... N ) -> ( M e. ( 0 ... N ) -> ( K <_ M -> ( ( M - K ) e. ZZ /\ 0 <_ ( M - K ) ) ) ) )
16 15 3imp 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ K <_ M ) -> ( ( M - K ) e. ZZ /\ 0 <_ ( M - K ) ) )
17 elnn0z 
 |-  ( ( M - K ) e. NN0 <-> ( ( M - K ) e. ZZ /\ 0 <_ ( M - K ) ) )
18 16 17 sylibr 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ K <_ M ) -> ( M - K ) e. NN0 )
19 elfz3nn0 
 |-  ( K e. ( 0 ... N ) -> N e. NN0 )
20 19 3ad2ant1 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ K <_ M ) -> N e. NN0 )
21 elfz2nn0 
 |-  ( M e. ( 0 ... N ) <-> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
22 8 3ad2ant1 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> M e. RR )
23 resubcl 
 |-  ( ( M e. RR /\ K e. RR ) -> ( M - K ) e. RR )
24 22 9 23 syl2an 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ K e. NN0 ) -> ( M - K ) e. RR )
25 22 adantr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ K e. NN0 ) -> M e. RR )
26 nn0re 
 |-  ( N e. NN0 -> N e. RR )
27 26 3ad2ant2 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> N e. RR )
28 27 adantr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ K e. NN0 ) -> N e. RR )
29 nn0ge0 
 |-  ( K e. NN0 -> 0 <_ K )
30 29 adantl 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ K e. NN0 ) -> 0 <_ K )
31 subge02 
 |-  ( ( M e. RR /\ K e. RR ) -> ( 0 <_ K <-> ( M - K ) <_ M ) )
32 22 9 31 syl2an 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ K e. NN0 ) -> ( 0 <_ K <-> ( M - K ) <_ M ) )
33 30 32 mpbid 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ K e. NN0 ) -> ( M - K ) <_ M )
34 simpl3 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ K e. NN0 ) -> M <_ N )
35 24 25 28 33 34 letrd 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ K e. NN0 ) -> ( M - K ) <_ N )
36 35 ex 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( K e. NN0 -> ( M - K ) <_ N ) )
37 21 36 sylbi 
 |-  ( M e. ( 0 ... N ) -> ( K e. NN0 -> ( M - K ) <_ N ) )
38 1 37 syl5com 
 |-  ( K e. ( 0 ... N ) -> ( M e. ( 0 ... N ) -> ( M - K ) <_ N ) )
39 38 a1dd 
 |-  ( K e. ( 0 ... N ) -> ( M e. ( 0 ... N ) -> ( K <_ M -> ( M - K ) <_ N ) ) )
40 39 3imp 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ K <_ M ) -> ( M - K ) <_ N )
41 elfz2nn0 
 |-  ( ( M - K ) e. ( 0 ... N ) <-> ( ( M - K ) e. NN0 /\ N e. NN0 /\ ( M - K ) <_ N ) )
42 18 20 40 41 syl3anbrc 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ K <_ M ) -> ( M - K ) e. ( 0 ... N ) )