Metamath Proof Explorer

Theorem difelfznle

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

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

Proof

Step Hyp Ref Expression
1 elfz2nn0 
 |-  ( M e. ( 0 ... N ) <-> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
2 nn0addcl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M + N ) e. NN0 )
3 2 nn0zd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M + N ) e. ZZ )
4 3 3adant3 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( M + N ) e. ZZ )
5 1 4 sylbi 
 |-  ( M e. ( 0 ... N ) -> ( M + N ) e. ZZ )
6 elfzelz 
 |-  ( K e. ( 0 ... N ) -> K e. ZZ )
7 zsubcl 
 |-  ( ( ( M + N ) e. ZZ /\ K e. ZZ ) -> ( ( M + N ) - K ) e. ZZ )
8 5 6 7 syl2anr 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> ( ( M + N ) - K ) e. ZZ )
9 8 3adant3 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> ( ( M + N ) - K ) e. ZZ )
10 6 zred 
 |-  ( K e. ( 0 ... N ) -> K e. RR )
11 10 adantr 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> K e. RR )
12 elfzel2 
 |-  ( K e. ( 0 ... N ) -> N e. ZZ )
13 12 zred 
 |-  ( K e. ( 0 ... N ) -> N e. RR )
14 13 adantr 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> N e. RR )
15 nn0readdcl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M + N ) e. RR )
16 15 3adant3 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( M + N ) e. RR )
17 1 16 sylbi 
 |-  ( M e. ( 0 ... N ) -> ( M + N ) e. RR )
18 17 adantl 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> ( M + N ) e. RR )
19 elfzle2 
 |-  ( K e. ( 0 ... N ) -> K <_ N )
20 elfzle1 
 |-  ( M e. ( 0 ... N ) -> 0 <_ M )
21 nn0re 
 |-  ( M e. NN0 -> M e. RR )
22 nn0re 
 |-  ( N e. NN0 -> N e. RR )
23 21 22 anim12ci 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N e. RR /\ M e. RR ) )
24 23 3adant3 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( N e. RR /\ M e. RR ) )
25 1 24 sylbi 
 |-  ( M e. ( 0 ... N ) -> ( N e. RR /\ M e. RR ) )
26 addge02 
 |-  ( ( N e. RR /\ M e. RR ) -> ( 0 <_ M <-> N <_ ( M + N ) ) )
27 25 26 syl 
 |-  ( M e. ( 0 ... N ) -> ( 0 <_ M <-> N <_ ( M + N ) ) )
28 20 27 mpbid 
 |-  ( M e. ( 0 ... N ) -> N <_ ( M + N ) )
29 19 28 anim12i 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> ( K <_ N /\ N <_ ( M + N ) ) )
30 letr 
 |-  ( ( K e. RR /\ N e. RR /\ ( M + N ) e. RR ) -> ( ( K <_ N /\ N <_ ( M + N ) ) -> K <_ ( M + N ) ) )
31 30 imp 
 |-  ( ( ( K e. RR /\ N e. RR /\ ( M + N ) e. RR ) /\ ( K <_ N /\ N <_ ( M + N ) ) ) -> K <_ ( M + N ) )
32 11 14 18 29 31 syl31anc 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> K <_ ( M + N ) )
33 32 3adant3 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> K <_ ( M + N ) )
34 zre 
 |-  ( K e. ZZ -> K e. RR )
35 21 22 anim12i 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M e. RR /\ N e. RR ) )
36 35 3adant3 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( M e. RR /\ N e. RR ) )
37 1 36 sylbi 
 |-  ( M e. ( 0 ... N ) -> ( M e. RR /\ N e. RR ) )
38 readdcl 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M + N ) e. RR )
39 37 38 syl 
 |-  ( M e. ( 0 ... N ) -> ( M + N ) e. RR )
40 34 39 anim12ci 
 |-  ( ( K e. ZZ /\ M e. ( 0 ... N ) ) -> ( ( M + N ) e. RR /\ K e. RR ) )
41 6 40 sylan 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> ( ( M + N ) e. RR /\ K e. RR ) )
42 41 3adant3 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> ( ( M + N ) e. RR /\ K e. RR ) )
43 subge0 
 |-  ( ( ( M + N ) e. RR /\ K e. RR ) -> ( 0 <_ ( ( M + N ) - K ) <-> K <_ ( M + N ) ) )
44 42 43 syl 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> ( 0 <_ ( ( M + N ) - K ) <-> K <_ ( M + N ) ) )
45 33 44 mpbird 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> 0 <_ ( ( M + N ) - K ) )
46 elnn0z 
 |-  ( ( ( M + N ) - K ) e. NN0 <-> ( ( ( M + N ) - K ) e. ZZ /\ 0 <_ ( ( M + N ) - K ) ) )
47 9 45 46 sylanbrc 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> ( ( M + N ) - K ) e. NN0 )
48 elfz3nn0 
 |-  ( K e. ( 0 ... N ) -> N e. NN0 )
49 48 3ad2ant1 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> N e. NN0 )
50 elfzelz 
 |-  ( M e. ( 0 ... N ) -> M e. ZZ )
51 zre 
 |-  ( M e. ZZ -> M e. RR )
52 ltnle 
 |-  ( ( M e. RR /\ K e. RR ) -> ( M < K <-> -. K <_ M ) )
53 52 ancoms 
 |-  ( ( K e. RR /\ M e. RR ) -> ( M < K <-> -. K <_ M ) )
54 ltle 
 |-  ( ( M e. RR /\ K e. RR ) -> ( M < K -> M <_ K ) )
55 54 ancoms 
 |-  ( ( K e. RR /\ M e. RR ) -> ( M < K -> M <_ K ) )
56 53 55 sylbird 
 |-  ( ( K e. RR /\ M e. RR ) -> ( -. K <_ M -> M <_ K ) )
57 34 51 56 syl2an 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( -. K <_ M -> M <_ K ) )
58 6 50 57 syl2an 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> ( -. K <_ M -> M <_ K ) )
59 58 3impia 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> M <_ K )
60 50 zred 
 |-  ( M e. ( 0 ... N ) -> M e. RR )
61 60 adantl 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> M e. RR )
62 61 11 14 leadd1d 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> ( M <_ K <-> ( M + N ) <_ ( K + N ) ) )
63 62 3adant3 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> ( M <_ K <-> ( M + N ) <_ ( K + N ) ) )
64 59 63 mpbid 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> ( M + N ) <_ ( K + N ) )
65 18 11 14 lesubadd2d 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> ( ( ( M + N ) - K ) <_ N <-> ( M + N ) <_ ( K + N ) ) )
66 65 3adant3 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> ( ( ( M + N ) - K ) <_ N <-> ( M + N ) <_ ( K + N ) ) )
67 64 66 mpbird 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> ( ( M + N ) - K ) <_ N )
68 elfz2nn0 
 |-  ( ( ( M + N ) - K ) e. ( 0 ... N ) <-> ( ( ( M + N ) - K ) e. NN0 /\ N e. NN0 /\ ( ( M + N ) - K ) <_ N ) )
69 47 49 67 68 syl3anbrc 
 |-  ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> ( ( M + N ) - K ) e. ( 0 ... N ) )