Theorem elzdif0

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

	Ref	Expression
Assertion	elzdif0	⊢ ( 𝑀 ∈ ( ℤ ∖ { 0 } ) → ( 𝑀 ∈ ℕ ∨ - 𝑀 ∈ ℕ ) )

Proof

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