subeluzsub

Description: Membership of a difference in an earlier upper set of integers. (Contributed by AV, 10-May-2022)

		Ref	Expression
	Assertion	subeluzsub	$⊢ (M \in ℤ \land N \in ℤ_{\geq K}) \to M - K \in ℤ_{\geq (M - N)}$

Step	Hyp	Ref	Expression
1		eluzelz	$⊢ N \in ℤ_{\geq K} \to N \in ℤ$
2		zsubcl	$⊢ (M \in ℤ \land N \in ℤ) \to M - N \in ℤ$
3	1 2	sylan2	$⊢ (M \in ℤ \land N \in ℤ_{\geq K}) \to M - N \in ℤ$
4		eluzel2	$⊢ N \in ℤ_{\geq K} \to K \in ℤ$
5		zsubcl	$⊢ (M \in ℤ \land K \in ℤ) \to M - K \in ℤ$
6	4 5	sylan2	$⊢ (M \in ℤ \land N \in ℤ_{\geq K}) \to M - K \in ℤ$
7	4	zred	$⊢ N \in ℤ_{\geq K} \to K \in ℝ$
8	7	adantl	$⊢ (M \in ℤ \land N \in ℤ_{\geq K}) \to K \in ℝ$
9	1	zred	$⊢ N \in ℤ_{\geq K} \to N \in ℝ$
10	9	adantl	$⊢ (M \in ℤ \land N \in ℤ_{\geq K}) \to N \in ℝ$
11		zre	$⊢ M \in ℤ \to M \in ℝ$
12	11	adantr	$⊢ (M \in ℤ \land N \in ℤ_{\geq K}) \to M \in ℝ$
13		eluzle	$⊢ N \in ℤ_{\geq K} \to K \leq N$
14	13	adantl	$⊢ (M \in ℤ \land N \in ℤ_{\geq K}) \to K \leq N$
15	8 10 12 14	lesub2dd	$⊢ (M \in ℤ \land N \in ℤ_{\geq K}) \to M - N \leq M - K$
16		eluz2	$⊢ M - K \in ℤ_{\geq (M - N)} \leftrightarrow (M - N \in ℤ \land M - K \in ℤ \land M - N \leq M - K)$
17	3 6 15 16	syl3anbrc	$⊢ (M \in ℤ \land N \in ℤ_{\geq K}) \to M - K \in ℤ_{\geq (M - N)}$

Metamath Proof Explorer