fz0fzdiffz0

Description: The difference of an integer in a finite set of sequential nonnegative integers and and an integer of a finite set of sequential integers with the same upper bound and the nonnegative integer as lower bound is a member of the finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 6-Jun-2018)

		Ref	Expression
	Assertion	fz0fzdiffz0	$⊢ (M \in (0 \dots N) \land K \in (M \dots N)) \to K - M \in (0 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		fz0fzelfz0	$⊢ (M \in (0 \dots N) \land K \in (M \dots N)) \to K \in (0 \dots N)$
2		elfzle1	$⊢ K \in (M \dots N) \to M \leq K$
3	2	adantl	$⊢ (M \in (0 \dots N) \land K \in (M \dots N)) \to M \leq K$
4	3	adantl	$⊢ (K \in (0 \dots N) \land (M \in (0 \dots N) \land K \in (M \dots N))) \to M \leq K$
5		elfznn0	$⊢ M \in (0 \dots N) \to M \in ℕ_{0}$
6	5	adantr	$⊢ (M \in (0 \dots N) \land K \in (M \dots N)) \to M \in ℕ_{0}$
7		elfznn0	$⊢ K \in (0 \dots N) \to K \in ℕ_{0}$
8		nn0sub	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to (M \leq K \leftrightarrow K - M \in ℕ_{0})$
9	6 7 8	syl2anr	$⊢ (K \in (0 \dots N) \land (M \in (0 \dots N) \land K \in (M \dots N))) \to (M \leq K \leftrightarrow K - M \in ℕ_{0})$
10	4 9	mpbid	$⊢ (K \in (0 \dots N) \land (M \in (0 \dots N) \land K \in (M \dots N))) \to K - M \in ℕ_{0}$
11		elfz3nn0	$⊢ K \in (0 \dots N) \to N \in ℕ_{0}$
12	11	adantr	$⊢ (K \in (0 \dots N) \land (M \in (0 \dots N) \land K \in (M \dots N))) \to N \in ℕ_{0}$
13		elfz2nn0	$⊢ M \in (0 \dots N) \leftrightarrow (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
14		elfz2	$⊢ K \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N))$
15		zsubcl	$⊢ (K \in ℤ \land M \in ℤ) \to K - M \in ℤ$
16	15	zred	$⊢ (K \in ℤ \land M \in ℤ) \to K - M \in ℝ$
17	16	ancoms	$⊢ (M \in ℤ \land K \in ℤ) \to K - M \in ℝ$
18	17	3adant2	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to K - M \in ℝ$
19		zre	$⊢ K \in ℤ \to K \in ℝ$
20	19	3ad2ant3	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to K \in ℝ$
21		zre	$⊢ N \in ℤ \to N \in ℝ$
22	21	3ad2ant2	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to N \in ℝ$
23	18 20 22	3jca	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (K - M \in ℝ \land K \in ℝ \land N \in ℝ)$
24	23	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \in ℕ_{0}) \to (K - M \in ℝ \land K \in ℝ \land N \in ℝ)$
25	24	adantr	$⊢ (((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \in ℕ_{0}) \land K \leq N) \to (K - M \in ℝ \land K \in ℝ \land N \in ℝ)$
26		nn0ge0	$⊢ M \in ℕ_{0} \to 0 \leq M$
27	26	adantl	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \in ℕ_{0}) \to 0 \leq M$
28		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
29		subge02	$⊢ (K \in ℝ \land M \in ℝ) \to (0 \leq M \leftrightarrow K - M \leq K)$
30	20 28 29	syl2an	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \in ℕ_{0}) \to (0 \leq M \leftrightarrow K - M \leq K)$
31	27 30	mpbid	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \in ℕ_{0}) \to K - M \leq K$
32	31	anim1i	$⊢ (((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \in ℕ_{0}) \land K \leq N) \to (K - M \leq K \land K \leq N)$
33		letr	$⊢ (K - M \in ℝ \land K \in ℝ \land N \in ℝ) \to ((K - M \leq K \land K \leq N) \to K - M \leq N)$
34	25 32 33	sylc	$⊢ (((M \in ℤ \land N \in ℤ \land K \in ℤ) \land M \in ℕ_{0}) \land K \leq N) \to K - M \leq N$
35	34	exp31	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M \in ℕ_{0} \to (K \leq N \to K - M \leq N))$
36	35	a1i	$⊢ N \in ℕ_{0} \to ((M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M \in ℕ_{0} \to (K \leq N \to K - M \leq N)))$
37	36	com14	$⊢ K \leq N \to ((M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M \in ℕ_{0} \to (N \in ℕ_{0} \to K - M \leq N)))$
38	37	adantl	$⊢ (M \leq K \land K \leq N) \to ((M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M \in ℕ_{0} \to (N \in ℕ_{0} \to K - M \leq N)))$
39	38	impcom	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N)) \to (M \in ℕ_{0} \to (N \in ℕ_{0} \to K - M \leq N))$
40	14 39	sylbi	$⊢ K \in (M \dots N) \to (M \in ℕ_{0} \to (N \in ℕ_{0} \to K - M \leq N))$
41	40	com13	$⊢ N \in ℕ_{0} \to (M \in ℕ_{0} \to (K \in (M \dots N) \to K - M \leq N))$
42	41	impcom	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (K \in (M \dots N) \to K - M \leq N)$
43	42	3adant3	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to (K \in (M \dots N) \to K - M \leq N)$
44	13 43	sylbi	$⊢ M \in (0 \dots N) \to (K \in (M \dots N) \to K - M \leq N)$
45	44	imp	$⊢ (M \in (0 \dots N) \land K \in (M \dots N)) \to K - M \leq N$
46	45	adantl	$⊢ (K \in (0 \dots N) \land (M \in (0 \dots N) \land K \in (M \dots N))) \to K - M \leq N$
47	10 12 46	3jca	$⊢ (K \in (0 \dots N) \land (M \in (0 \dots N) \land K \in (M \dots N))) \to (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N)$
48	1 47	mpancom	$⊢ (M \in (0 \dots N) \land K \in (M \dots N)) \to (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N)$
49		elfz2nn0	$⊢ K - M \in (0 \dots N) \leftrightarrow (K - M \in ℕ_{0} \land N \in ℕ_{0} \land K - M \leq N)$
50	48 49	sylibr	$⊢ (M \in (0 \dots N) \land K \in (M \dots N)) \to K - M \in (0 \dots N)$

Metamath Proof Explorer

Theorem fz0fzdiffz0

Proof