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 ∈ ℂ ∖ ℤ ∖ ℕ ∧ N ∈ ℕ 0 → A + N ≠ 0

Proof

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