This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem absz

Description: A real number is an integer iff its absolute value is an integer. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion absz 
|- ( A e. RR -> ( A e. ZZ <-> ( abs ` A ) e. ZZ ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( ( abs ` A ) = A -> ( ( abs ` A ) e. ZZ <-> A e. ZZ ) )
2 1 bicomd 
 |-  ( ( abs ` A ) = A -> ( A e. ZZ <-> ( abs ` A ) e. ZZ ) )
3 2 a1i 
 |-  ( A e. RR -> ( ( abs ` A ) = A -> ( A e. ZZ <-> ( abs ` A ) e. ZZ ) ) )
4 recn 
 |-  ( A e. RR -> A e. CC )
5 znegclb 
 |-  ( A e. CC -> ( A e. ZZ <-> -u A e. ZZ ) )
6 4 5 syl 
 |-  ( A e. RR -> ( A e. ZZ <-> -u A e. ZZ ) )
7 eleq1 
 |-  ( ( abs ` A ) = -u A -> ( ( abs ` A ) e. ZZ <-> -u A e. ZZ ) )
8 7 bibi2d 
 |-  ( ( abs ` A ) = -u A -> ( ( A e. ZZ <-> ( abs ` A ) e. ZZ ) <-> ( A e. ZZ <-> -u A e. ZZ ) ) )
9 6 8 syl5ibrcom 
 |-  ( A e. RR -> ( ( abs ` A ) = -u A -> ( A e. ZZ <-> ( abs ` A ) e. ZZ ) ) )
10 absor 
 |-  ( A e. RR -> ( ( abs ` A ) = A \/ ( abs ` A ) = -u A ) )
11 3 9 10 mpjaod 
 |-  ( A e. RR -> ( A e. ZZ <-> ( abs ` A ) e. ZZ ) )