eluzmn

Description: Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018)

		Ref	Expression
	Assertion	eluzmn	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to M \in ℤ_{\geq (M - N)}$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to M \in ℤ$
2		simpr	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
3	2	nn0zd	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to N \in ℤ$
4	1 3	zsubcld	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to M - N \in ℤ$
5	1	zred	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to M \in ℝ$
6	2	nn0red	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to N \in ℝ$
7	5 6	readdcld	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to M + N \in ℝ$
8		nn0addge1	$⊢ (M \in ℝ \land N \in ℕ_{0}) \to M \leq M + N$
9	5 8	sylancom	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to M \leq M + N$
10	5 7 6 9	lesub1dd	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to M - N \leq M + N - N$
11	5	recnd	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to M \in ℂ$
12	6	recnd	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to N \in ℂ$
13	11 12	pncand	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to M + N - N = M$
14	10 13	breqtrd	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to M - N \leq M$
15		eluz2	$⊢ M \in ℤ_{\geq (M - N)} \leftrightarrow (M - N \in ℤ \land M \in ℤ \land M - N \leq M)$
16	4 1 14 15	syl3anbrc	$⊢ (M \in ℤ \land N \in ℕ_{0}) \to M \in ℤ_{\geq (M - N)}$

Metamath Proof Explorer