Theorem dmgmn0

Description: If A is not a nonpositive integer, then A is nonzero. (Contributed by Mario Carneiro, 3-Jul-2017)

	Ref	Expression
Hypothesis	dmgmn0.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
Assertion	dmgmn0	⊢ ( 𝜑 → 𝐴 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		dmgmn0.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
2	1	eldifad	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
3	2	addridd	⊢ ( 𝜑 → ( 𝐴 + 0 ) = 𝐴 )
4		0nn0	⊢ 0 ∈ ℕ0
5		dmgmaddn0	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 0 ∈ ℕ0 ) → ( 𝐴 + 0 ) ≠ 0 )
6	1 4 5	sylancl	⊢ ( 𝜑 → ( 𝐴 + 0 ) ≠ 0 )
7	3 6	eqnetrrd	⊢ ( 𝜑 → 𝐴 ≠ 0 )