eluzsub

Description: Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by SN, 7-Feb-2025)

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

Step	Hyp	Ref	Expression
1		simp1	$⊢ (M \in ℤ \land K \in ℤ \land N \in ℤ_{\geq (M + K)}) \to M \in ℤ$
2		eluzelz	$⊢ N \in ℤ_{\geq (M + K)} \to N \in ℤ$
3	2	3ad2ant3	$⊢ (M \in ℤ \land K \in ℤ \land N \in ℤ_{\geq (M + K)}) \to N \in ℤ$
4		simp2	$⊢ (M \in ℤ \land K \in ℤ \land N \in ℤ_{\geq (M + K)}) \to K \in ℤ$
5	3 4	zsubcld	$⊢ (M \in ℤ \land K \in ℤ \land N \in ℤ_{\geq (M + K)}) \to N - K \in ℤ$
6		eluzle	$⊢ N \in ℤ_{\geq (M + K)} \to M + K \leq N$
7	6	3ad2ant3	$⊢ (M \in ℤ \land K \in ℤ \land N \in ℤ_{\geq (M + K)}) \to M + K \leq N$
8		zre	$⊢ M \in ℤ \to M \in ℝ$
9		zre	$⊢ K \in ℤ \to K \in ℝ$
10		eluzelre	$⊢ N \in ℤ_{\geq (M + K)} \to N \in ℝ$
11		leaddsub	$⊢ (M \in ℝ \land K \in ℝ \land N \in ℝ) \to (M + K \leq N \leftrightarrow M \leq N - K)$
12	8 9 10 11	syl3an	$⊢ (M \in ℤ \land K \in ℤ \land N \in ℤ_{\geq (M + K)}) \to (M + K \leq N \leftrightarrow M \leq N - K)$
13	7 12	mpbid	$⊢ (M \in ℤ \land K \in ℤ \land N \in ℤ_{\geq (M + K)}) \to M \leq N - K$
14		eluz2	$⊢ N - K \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N - K \in ℤ \land M \leq N - K)$
15	1 5 13 14	syl3anbrc	$⊢ (M \in ℤ \land K \in ℤ \land N \in ℤ_{\geq (M + K)}) \to N - K \in ℤ_{\geq M}$

Metamath Proof Explorer