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

Metamath Proof Explorer

Theorem negn0nposznnd

Description: Lemma for dffltz . (Contributed by Steven Nguyen, 27-Feb-2023)

Ref Expression
Hypotheses negn0nposznnd.1 ⊢ φ → A ≠ 0
negn0nposznnd.2 ⊢ φ → ¬ 0 < A
negn0nposznnd.3 ⊢ φ → A ∈ ℤ
Assertion negn0nposznnd ⊢ φ → − A ∈ ℕ

Proof

Step Hyp Ref Expression
1 negn0nposznnd.1 ⊢ φ → A ≠ 0
2 negn0nposznnd.2 ⊢ φ → ¬ 0 < A
3 negn0nposznnd.3 ⊢ φ → A ∈ ℤ
4 nngt0 ⊢ A ∈ ℕ → 0 < A
5 2 4 nsyl ⊢ φ → ¬ A ∈ ℕ
6 1 neneqd ⊢ φ → ¬ A = 0
7 5 6 jca ⊢ φ → ¬ A ∈ ℕ ∧ ¬ A = 0
8 pm4.56 ⊢ ¬ A ∈ ℕ ∧ ¬ A = 0 ↔ ¬ A ∈ ℕ ∨ A = 0
9 7 8 sylib ⊢ φ → ¬ A ∈ ℕ ∨ A = 0
10 elnn0 ⊢ A ∈ ℕ 0 ↔ A ∈ ℕ ∨ A = 0
11 9 10 sylnibr ⊢ φ → ¬ A ∈ ℕ 0
12 znnn0nn ⊢ A ∈ ℤ ∧ ¬ A ∈ ℕ 0 → − A ∈ ℕ
13 3 11 12 syl2anc ⊢ φ → − A ∈ ℕ