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 \in (0 \dots N) \land M \in (0 \dots N) \land K \leq M) \to M - K \in (0 \dots N)$

Proof

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

Metamath Proof Explorer

Theorem difelfzle

Proof