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	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 + 𝑁 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		eldmgm	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ - 𝐴 ∈ ℕ0 ) )
2	1	simprbi	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ¬ - 𝐴 ∈ ℕ0 )
3	2	adantr	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → ¬ - 𝐴 ∈ ℕ0 )
4		df-neg	⊢ - 𝐴 = ( 0 − 𝐴 )
5	4	eqeq1i	⊢ ( - 𝐴 = 𝑁 ↔ ( 0 − 𝐴 ) = 𝑁 )
6		0cnd	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → 0 ∈ ℂ )
7		eldifi	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → 𝐴 ∈ ℂ )
8	7	adantr	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
9		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
10	9	adantl	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
11	6 8 10	subaddd	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 0 − 𝐴 ) = 𝑁 ↔ ( 𝐴 + 𝑁 ) = 0 ) )
12	5 11	bitrid	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → ( - 𝐴 = 𝑁 ↔ ( 𝐴 + 𝑁 ) = 0 ) )
13		simpr	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
14		eleq1	⊢ ( - 𝐴 = 𝑁 → ( - 𝐴 ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 ) )
15	13 14	syl5ibrcom	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → ( - 𝐴 = 𝑁 → - 𝐴 ∈ ℕ0 ) )
16	12 15	sylbird	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 + 𝑁 ) = 0 → - 𝐴 ∈ ℕ0 ) )
17	16	necon3bd	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ¬ - 𝐴 ∈ ℕ0 → ( 𝐴 + 𝑁 ) ≠ 0 ) )
18	3 17	mpd	⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 + 𝑁 ) ≠ 0 )