Metamath Proof Explorer

Theorem dmgmn0

Description: If A is not a nonpositive integer, then A is nonzero. (Contributed by Mario Carneiro, 3-Jul-2017)

Ref Expression
Hypothesis dmgmn0.a 
|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
Assertion dmgmn0 
|- ( ph -> A =/= 0 )

Proof

Step Hyp Ref Expression
1 dmgmn0.a 
 |-  ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
2 1 eldifad 
 |-  ( ph -> A e. CC )
3 2 addridd 
 |-  ( ph -> ( A + 0 ) = A )
4 0nn0 
 |-  0 e. NN0
5 dmgmaddn0 
 |-  ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ 0 e. NN0 ) -> ( A + 0 ) =/= 0 )
6 1 4 5 sylancl 
 |-  ( ph -> ( A + 0 ) =/= 0 )
7 3 6 eqnetrrd 
 |-  ( ph -> A =/= 0 )