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	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
	dmgmaddnn0.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	dmgmaddnn0	$⊢ φ \to A + N \in (ℂ ∖ (ℤ ∖ ℕ))$

Proof

Step	Hyp	Ref	Expression
1		dmgmn0.a	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
2		dmgmaddnn0.n	$⊢ φ \to N \in ℕ_{0}$
3	1	eldifad	$⊢ φ \to A \in ℂ$
4	2	nn0cnd	$⊢ φ \to N \in ℂ$
5	3 4	addcld	$⊢ φ \to A + N \in ℂ$
6		eldmgm	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \leftrightarrow (A \in ℂ \land \neg - A \in ℕ_{0})$
7	1 6	sylib	$⊢ φ \to (A \in ℂ \land \neg - A \in ℕ_{0})$
8	7	simprd	$⊢ φ \to \neg - A \in ℕ_{0}$
9	3 4	negdi2d	$⊢ φ \to - (A + N) = - A - N$
10	9	oveq1d	$⊢ φ \to - (A + N) + N = (- A) - N + N$
11	3	negcld	$⊢ φ \to - A \in ℂ$
12	11 4	npcand	$⊢ φ \to (- A) - N + N = - A$
13	10 12	eqtrd	$⊢ φ \to - (A + N) + N = - A$
14	13	adantr	$⊢ (φ \land - (A + N) \in ℕ_{0}) \to - (A + N) + N = - A$
15		simpr	$⊢ (φ \land - (A + N) \in ℕ_{0}) \to - (A + N) \in ℕ_{0}$
16	2	adantr	$⊢ (φ \land - (A + N) \in ℕ_{0}) \to N \in ℕ_{0}$
17	15 16	nn0addcld	$⊢ (φ \land - (A + N) \in ℕ_{0}) \to - (A + N) + N \in ℕ_{0}$
18	14 17	eqeltrrd	$⊢ (φ \land - (A + N) \in ℕ_{0}) \to - A \in ℕ_{0}$
19	8 18	mtand	$⊢ φ \to \neg - (A + N) \in ℕ_{0}$
20		eldmgm	$⊢ A + N \in (ℂ ∖ (ℤ ∖ ℕ)) \leftrightarrow (A + N \in ℂ \land \neg - (A + N) \in ℕ_{0})$
21	5 19 20	sylanbrc	$⊢ φ \to A + N \in (ℂ ∖ (ℤ ∖ ℕ))$

Metamath Proof Explorer

Theorem dmgmaddnn0

Proof