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 ∈ ℕ