Metamath Proof Explorer

Theorem dmgmaddnn0

Description: If A is not a nonpositive integer and N is a nonnegative integer, then A + N is also not a nonpositive integer. (Contributed by Mario Carneiro, 6-Jul-2017)

Ref Expression
Hypotheses dmgmn0.a ⊢ φ → A ∈ ℂ ∖ ℤ ∖ ℕ
dmgmaddnn0.n ⊢ φ → N ∈ ℕ 0
Assertion dmgmaddnn0 ⊢ φ → A + N ∈ ℂ ∖ ℤ ∖ ℕ

Proof

Step Hyp Ref Expression
1 dmgmn0.a ⊢ φ → A ∈ ℂ ∖ ℤ ∖ ℕ
2 dmgmaddnn0.n ⊢ φ → N ∈ ℕ 0
3 1 eldifad ⊢ φ → A ∈ ℂ
4 2 nn0cnd ⊢ φ → N ∈ ℂ
5 3 4 addcld ⊢ φ → A + N ∈ ℂ
6 eldmgm ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ ↔ A ∈ ℂ ∧ ¬ − A ∈ ℕ 0
7 1 6 sylib ⊢ φ → A ∈ ℂ ∧ ¬ − A ∈ ℕ 0
8 7 simprd ⊢ φ → ¬ − A ∈ ℕ 0
9 3 4 negdi2d ⊢ φ → − A + N = - A - N
10 9 oveq1d ⊢ φ → - A + N + N = − A - N + N
11 3 negcld ⊢ φ → − A ∈ ℂ
12 11 4 npcand ⊢ φ → − A - N + N = − A
13 10 12 eqtrd ⊢ φ → - A + N + N = − A
14 13 adantr ⊢ φ ∧ − A + N ∈ ℕ 0 → - A + N + N = − A
15 simpr ⊢ φ ∧ − A + N ∈ ℕ 0 → − A + N ∈ ℕ 0
16 2 adantr ⊢ φ ∧ − A + N ∈ ℕ 0 → N ∈ ℕ 0
17 15 16 nn0addcld ⊢ φ ∧ − A + N ∈ ℕ 0 → - A + N + N ∈ ℕ 0
18 14 17 eqeltrrd ⊢ φ ∧ − A + N ∈ ℕ 0 → − A ∈ ℕ 0
19 8 18 mtand ⊢ φ → ¬ − A + N ∈ ℕ 0
20 eldmgm ⊢ A + N ∈ ℂ ∖ ℤ ∖ ℕ ↔ A + N ∈ ℂ ∧ ¬ − A + N ∈ ℕ 0
21 5 19 20 sylanbrc ⊢ φ → A + N ∈ ℂ ∖ ℤ ∖ ℕ