Theorem uzneg

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

	Ref	Expression
Assertion	uzneg	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → - 𝑀 ∈ ( ℤ≥ ‘ - 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑁 )
2		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
3		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
4		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
5		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
6		leneg	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ - 𝑁 ≤ - 𝑀 ) )
7	4 5 6	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ - 𝑁 ≤ - 𝑀 ) )
8	2 3 7	syl2anc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ≤ 𝑁 ↔ - 𝑁 ≤ - 𝑀 ) )
9	1 8	mpbid	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → - 𝑁 ≤ - 𝑀 )
10		znegcl	⊢ ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ )
11		znegcl	⊢ ( 𝑀 ∈ ℤ → - 𝑀 ∈ ℤ )
12		eluz	⊢ ( ( - 𝑁 ∈ ℤ ∧ - 𝑀 ∈ ℤ ) → ( - 𝑀 ∈ ( ℤ≥ ‘ - 𝑁 ) ↔ - 𝑁 ≤ - 𝑀 ) )
13	10 11 12	syl2an	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( - 𝑀 ∈ ( ℤ≥ ‘ - 𝑁 ) ↔ - 𝑁 ≤ - 𝑀 ) )
14	3 2 13	syl2anc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( - 𝑀 ∈ ( ℤ≥ ‘ - 𝑁 ) ↔ - 𝑁 ≤ - 𝑀 ) )
15	9 14	mpbird	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → - 𝑀 ∈ ( ℤ≥ ‘ - 𝑁 ) )