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 e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( A + N ) =/= 0 )

Proof

Step	Hyp	Ref	Expression
1		eldmgm	|- ( A e. ( CC \ ( ZZ \ NN ) ) <-> ( A e. CC /\ -. -u A e. NN0 ) )
2	1	simprbi	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> -. -u A e. NN0 )
3	2	adantr	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> -. -u A e. NN0 )
4		df-neg	|- -u A = ( 0 - A )
5	4	eqeq1i	|- ( -u A = N <-> ( 0 - A ) = N )
6		0cnd	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> 0 e. CC )
7		eldifi	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> A e. CC )
8	7	adantr	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> A e. CC )
9		nn0cn	|- ( N e. NN0 -> N e. CC )
10	9	adantl	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> N e. CC )
11	6 8 10	subaddd	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( ( 0 - A ) = N <-> ( A + N ) = 0 ) )
12	5 11	bitrid	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( -u A = N <-> ( A + N ) = 0 ) )
13		simpr	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> N e. NN0 )
14		eleq1	|- ( -u A = N -> ( -u A e. NN0 <-> N e. NN0 ) )
15	13 14	syl5ibrcom	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( -u A = N -> -u A e. NN0 ) )
16	12 15	sylbird	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( ( A + N ) = 0 -> -u A e. NN0 ) )
17	16	necon3bd	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( -. -u A e. NN0 -> ( A + N ) =/= 0 ) )
18	3 17	mpd	|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( A + N ) =/= 0 )