Metamath Proof Explorer


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 syl5bb
 |-  ( ( 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 )