Metamath Proof Explorer

Theorem dmgmaddn0

Description: If A is not a nonpositive integer, then A + N is nonzero for any nonnegative integer N . (Contributed by Mario Carneiro, 12-Jul-2014)

		Ref	Expression
	Assertion	dmgmaddn0	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to A + N \neq 0$

Proof

Step	Hyp	Ref	Expression
1		eldmgm	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \leftrightarrow (A \in ℂ \land \neg - A \in ℕ_{0})$
2	1	simprbi	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to \neg - A \in ℕ_{0}$
3	2	adantr	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to \neg - A \in ℕ_{0}$
4		df-neg	$⊢ - A = 0 - A$
5	4	eqeq1i	$⊢ - A = N \leftrightarrow 0 - A = N$
6		0cnd	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to 0 \in ℂ$
7		eldifi	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to A \in ℂ$
8	7	adantr	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to A \in ℂ$
9		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
10	9	adantl	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to N \in ℂ$
11	6 8 10	subaddd	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to (0 - A = N \leftrightarrow A + N = 0)$
12	5 11	bitrid	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to (- A = N \leftrightarrow A + N = 0)$
13		simpr	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to N \in ℕ_{0}$
14		eleq1	$⊢ - A = N \to (- A \in ℕ_{0} \leftrightarrow N \in ℕ_{0})$
15	13 14	syl5ibrcom	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to (- A = N \to - A \in ℕ_{0})$
16	12 15	sylbird	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to (A + N = 0 \to - A \in ℕ_{0})$
17	16	necon3bd	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to (\neg - A \in ℕ_{0} \to A + N \neq 0)$
18	3 17	mpd	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land N \in ℕ_{0}) \to A + N \neq 0$