uzneg

Description: Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005)

		Ref	Expression
	Assertion	uzneg	$⊢ N \in ℤ_{\geq M} \to - M \in ℤ_{\geq -N}$

Step	Hyp	Ref	Expression
1		eluzle	$⊢ N \in ℤ_{\geq M} \to M \leq N$
2		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
3		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
4		zre	$⊢ M \in ℤ \to M \in ℝ$
5		zre	$⊢ N \in ℤ \to N \in ℝ$
6		leneg	$⊢ (M \in ℝ \land N \in ℝ) \to (M \leq N \leftrightarrow - N \leq - M)$
7	4 5 6	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to (M \leq N \leftrightarrow - N \leq - M)$
8	2 3 7	syl2anc	$⊢ N \in ℤ_{\geq M} \to (M \leq N \leftrightarrow - N \leq - M)$
9	1 8	mpbid	$⊢ N \in ℤ_{\geq M} \to - N \leq - M$
10		znegcl	$⊢ N \in ℤ \to - N \in ℤ$
11		znegcl	$⊢ M \in ℤ \to - M \in ℤ$
12		eluz	$⊢ (- N \in ℤ \land - M \in ℤ) \to (- M \in ℤ_{\geq -N} \leftrightarrow - N \leq - M)$
13	10 11 12	syl2an	$⊢ (N \in ℤ \land M \in ℤ) \to (- M \in ℤ_{\geq -N} \leftrightarrow - N \leq - M)$
14	3 2 13	syl2anc	$⊢ N \in ℤ_{\geq M} \to (- M \in ℤ_{\geq -N} \leftrightarrow - N \leq - M)$
15	9 14	mpbird	$⊢ N \in ℤ_{\geq M} \to - M \in ℤ_{\geq -N}$

Metamath Proof Explorer