This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → - 𝑀 ∈ ( ℤ≥ ‘ - 𝑁 ) )