Metamath Proof Explorer

Theorem elzdif0

Description: Lemma for qqhval2 . (Contributed by Thierry Arnoux, 29-Oct-2017)

Ref Expression
Assertion elzdif0 ⊢M∈ℤ∖0→M∈ℕ∨−M∈ℕ

Proof

Step Hyp Ref Expression
1 eldifsnneq ⊢M∈ℤ∖0→¬M=0
2 eldifi ⊢M∈ℤ∖0→M∈ℤ
3 elz ⊢M∈ℤ↔M∈ℝ∧M=0∨M∈ℕ∨−M∈ℕ
4 2 3 sylib ⊢M∈ℤ∖0→M∈ℝ∧M=0∨M∈ℕ∨−M∈ℕ
5 4 simprd ⊢M∈ℤ∖0→M=0∨M∈ℕ∨−M∈ℕ
6 3orass ⊢M=0∨M∈ℕ∨−M∈ℕ↔M=0∨M∈ℕ∨−M∈ℕ
7 5 6 sylib ⊢M∈ℤ∖0→M=0∨M∈ℕ∨−M∈ℕ
8 orel1 ⊢¬M=0→M=0∨M∈ℕ∨−M∈ℕ→M∈ℕ∨−M∈ℕ
9 1 7 8 sylc ⊢M∈ℤ∖0→M∈ℕ∨−M∈ℕ