Metamath Proof Explorer

Theorem znegclb

Description: A complex number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion znegclb 
|- ( A e. CC -> ( A e. ZZ <-> -u A e. ZZ ) )

Proof

Step Hyp Ref Expression
1 znegcl 
 |-  ( A e. ZZ -> -u A e. ZZ )
2 znegcl 
 |-  ( -u A e. ZZ -> -u -u A e. ZZ )
3 negneg 
 |-  ( A e. CC -> -u -u A = A )
4 3 eleq1d 
 |-  ( A e. CC -> ( -u -u A e. ZZ <-> A e. ZZ ) )
5 2 4 syl5ib 
 |-  ( A e. CC -> ( -u A e. ZZ -> A e. ZZ ) )
6 1 5 impbid2 
 |-  ( A e. CC -> ( A e. ZZ <-> -u A e. ZZ ) )