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

### Proof

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