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	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
	dmgmaddnn0.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	dmgmaddnn0	⊢ ( 𝜑 → ( 𝐴 + 𝑁 ) ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )

Proof

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