Metamath Proof Explorer

Theorem uzneg

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

Ref Expression
Assertion uzneg ⊢ N ∈ ℤ ≥ M → − M ∈ ℤ ≥ -N

Proof

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