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	|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
	dmgmaddnn0.n	|- ( ph -> N e. NN0 )
Assertion	dmgmaddnn0	|- ( ph -> ( A + N ) e. ( CC \ ( ZZ \ NN ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmgmn0.a	|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
2		dmgmaddnn0.n	|- ( ph -> N e. NN0 )
3	1	eldifad	|- ( ph -> A e. CC )
4	2	nn0cnd	|- ( ph -> N e. CC )
5	3 4	addcld	|- ( ph -> ( A + N ) e. CC )
6		eldmgm	|- ( A e. ( CC \ ( ZZ \ NN ) ) <-> ( A e. CC /\ -. -u A e. NN0 ) )
7	1 6	sylib	|- ( ph -> ( A e. CC /\ -. -u A e. NN0 ) )
8	7	simprd	|- ( ph -> -. -u A e. NN0 )
9	3 4	negdi2d	|- ( ph -> -u ( A + N ) = ( -u A - N ) )
10	9	oveq1d	|- ( ph -> ( -u ( A + N ) + N ) = ( ( -u A - N ) + N ) )
11	3	negcld	|- ( ph -> -u A e. CC )
12	11 4	npcand	|- ( ph -> ( ( -u A - N ) + N ) = -u A )
13	10 12	eqtrd	|- ( ph -> ( -u ( A + N ) + N ) = -u A )
14	13	adantr	|- ( ( ph /\ -u ( A + N ) e. NN0 ) -> ( -u ( A + N ) + N ) = -u A )
15		simpr	|- ( ( ph /\ -u ( A + N ) e. NN0 ) -> -u ( A + N ) e. NN0 )
16	2	adantr	|- ( ( ph /\ -u ( A + N ) e. NN0 ) -> N e. NN0 )
17	15 16	nn0addcld	|- ( ( ph /\ -u ( A + N ) e. NN0 ) -> ( -u ( A + N ) + N ) e. NN0 )
18	14 17	eqeltrrd	|- ( ( ph /\ -u ( A + N ) e. NN0 ) -> -u A e. NN0 )
19	8 18	mtand	|- ( ph -> -. -u ( A + N ) e. NN0 )
20		eldmgm	|- ( ( A + N ) e. ( CC \ ( ZZ \ NN ) ) <-> ( ( A + N ) e. CC /\ -. -u ( A + N ) e. NN0 ) )
21	5 19 20	sylanbrc	|- ( ph -> ( A + N ) e. ( CC \ ( ZZ \ NN ) ) )