# 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 ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge {M}\in \left(0\dots {N}\right)\wedge {K}\le {M}\right)\to {M}-{K}\in \left(0\dots {N}\right)$

### Proof

Step Hyp Ref Expression
1 elfznn0 ${⊢}{K}\in \left(0\dots {N}\right)\to {K}\in {ℕ}_{0}$
2 elfznn0 ${⊢}{M}\in \left(0\dots {N}\right)\to {M}\in {ℕ}_{0}$
3 nn0z ${⊢}{M}\in {ℕ}_{0}\to {M}\in ℤ$
4 nn0z ${⊢}{K}\in {ℕ}_{0}\to {K}\in ℤ$
5 zsubcl ${⊢}\left({M}\in ℤ\wedge {K}\in ℤ\right)\to {M}-{K}\in ℤ$
6 3 4 5 syl2anr ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to {M}-{K}\in ℤ$
7 6 adantr ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\wedge {K}\le {M}\right)\to {M}-{K}\in ℤ$
8 nn0re ${⊢}{M}\in {ℕ}_{0}\to {M}\in ℝ$
9 nn0re ${⊢}{K}\in {ℕ}_{0}\to {K}\in ℝ$
10 subge0 ${⊢}\left({M}\in ℝ\wedge {K}\in ℝ\right)\to \left(0\le {M}-{K}↔{K}\le {M}\right)$
11 8 9 10 syl2anr ${⊢}\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\to \left(0\le {M}-{K}↔{K}\le {M}\right)$
12 11 biimpar ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\wedge {K}\le {M}\right)\to 0\le {M}-{K}$
13 7 12 jca ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge {M}\in {ℕ}_{0}\right)\wedge {K}\le {M}\right)\to \left({M}-{K}\in ℤ\wedge 0\le {M}-{K}\right)$
14 13 exp31 ${⊢}{K}\in {ℕ}_{0}\to \left({M}\in {ℕ}_{0}\to \left({K}\le {M}\to \left({M}-{K}\in ℤ\wedge 0\le {M}-{K}\right)\right)\right)$
15 1 2 14 syl2im ${⊢}{K}\in \left(0\dots {N}\right)\to \left({M}\in \left(0\dots {N}\right)\to \left({K}\le {M}\to \left({M}-{K}\in ℤ\wedge 0\le {M}-{K}\right)\right)\right)$
16 15 3imp ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge {M}\in \left(0\dots {N}\right)\wedge {K}\le {M}\right)\to \left({M}-{K}\in ℤ\wedge 0\le {M}-{K}\right)$
17 elnn0z ${⊢}{M}-{K}\in {ℕ}_{0}↔\left({M}-{K}\in ℤ\wedge 0\le {M}-{K}\right)$
18 16 17 sylibr ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge {M}\in \left(0\dots {N}\right)\wedge {K}\le {M}\right)\to {M}-{K}\in {ℕ}_{0}$
19 elfz3nn0 ${⊢}{K}\in \left(0\dots {N}\right)\to {N}\in {ℕ}_{0}$
20 19 3ad2ant1 ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge {M}\in \left(0\dots {N}\right)\wedge {K}\le {M}\right)\to {N}\in {ℕ}_{0}$
21 elfz2nn0 ${⊢}{M}\in \left(0\dots {N}\right)↔\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)$
22 8 3ad2ant1 ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\to {M}\in ℝ$
23 resubcl ${⊢}\left({M}\in ℝ\wedge {K}\in ℝ\right)\to {M}-{K}\in ℝ$
24 22 9 23 syl2an ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\wedge {K}\in {ℕ}_{0}\right)\to {M}-{K}\in ℝ$
25 22 adantr ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\wedge {K}\in {ℕ}_{0}\right)\to {M}\in ℝ$
26 nn0re ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℝ$
27 26 3ad2ant2 ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\to {N}\in ℝ$
28 27 adantr ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\wedge {K}\in {ℕ}_{0}\right)\to {N}\in ℝ$
29 nn0ge0 ${⊢}{K}\in {ℕ}_{0}\to 0\le {K}$
30 29 adantl ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\wedge {K}\in {ℕ}_{0}\right)\to 0\le {K}$
31 subge02 ${⊢}\left({M}\in ℝ\wedge {K}\in ℝ\right)\to \left(0\le {K}↔{M}-{K}\le {M}\right)$
32 22 9 31 syl2an ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left(0\le {K}↔{M}-{K}\le {M}\right)$
33 30 32 mpbid ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\wedge {K}\in {ℕ}_{0}\right)\to {M}-{K}\le {M}$
34 simpl3 ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\wedge {K}\in {ℕ}_{0}\right)\to {M}\le {N}$
35 24 25 28 33 34 letrd ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\wedge {K}\in {ℕ}_{0}\right)\to {M}-{K}\le {N}$
36 35 ex ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}\le {N}\right)\to \left({K}\in {ℕ}_{0}\to {M}-{K}\le {N}\right)$
37 21 36 sylbi ${⊢}{M}\in \left(0\dots {N}\right)\to \left({K}\in {ℕ}_{0}\to {M}-{K}\le {N}\right)$
38 1 37 syl5com ${⊢}{K}\in \left(0\dots {N}\right)\to \left({M}\in \left(0\dots {N}\right)\to {M}-{K}\le {N}\right)$
39 38 a1dd ${⊢}{K}\in \left(0\dots {N}\right)\to \left({M}\in \left(0\dots {N}\right)\to \left({K}\le {M}\to {M}-{K}\le {N}\right)\right)$
40 39 3imp ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge {M}\in \left(0\dots {N}\right)\wedge {K}\le {M}\right)\to {M}-{K}\le {N}$
41 elfz2nn0 ${⊢}{M}-{K}\in \left(0\dots {N}\right)↔\left({M}-{K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {M}-{K}\le {N}\right)$
42 18 20 40 41 syl3anbrc ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge {M}\in \left(0\dots {N}\right)\wedge {K}\le {M}\right)\to {M}-{K}\in \left(0\dots {N}\right)$