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