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	$$⊢\phi \to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
Assertion	dmgmn0	$$⊢\phi \to A\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		dmgmn0.a	$$⊢\phi \to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
2	1	eldifad	$$⊢\phi \to A\in ℂ$$
3	2	addridd	$$⊢\phi \to A+0=A$$
4		0nn0	$$⊢0\in {\mathbb{N}}_0$$
5		dmgmaddn0	$$⊢\left(A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\wedge 0\in {\mathbb{N}}_0\right)\to A+0\ne 0$$
6	1 4 5	sylancl	$$⊢\phi \to A+0\ne 0$$
7	3 6	eqnetrrd	$$⊢\phi \to A\ne 0$$