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 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
negn0nposznnd.2 ⊢ ( 𝜑 → ¬ 0 < 𝐴 )
negn0nposznnd.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
Assertion negn0nposznnd ( 𝜑 → - 𝐴 ∈ ℕ )

Proof

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