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	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℤ ↔ ( abs ‘ 𝐴 ) ∈ ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( ( abs ‘ 𝐴 ) = 𝐴 → ( ( abs ‘ 𝐴 ) ∈ ℤ ↔ 𝐴 ∈ ℤ ) )
2	1	bicomd	⊢ ( ( abs ‘ 𝐴 ) = 𝐴 → ( 𝐴 ∈ ℤ ↔ ( abs ‘ 𝐴 ) ∈ ℤ ) )
3	2	a1i	⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) = 𝐴 → ( 𝐴 ∈ ℤ ↔ ( abs ‘ 𝐴 ) ∈ ℤ ) ) )
4		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
5		znegclb	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℤ ↔ - 𝐴 ∈ ℤ ) )
6	4 5	syl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℤ ↔ - 𝐴 ∈ ℤ ) )
7		eleq1	⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( abs ‘ 𝐴 ) ∈ ℤ ↔ - 𝐴 ∈ ℤ ) )
8	7	bibi2d	⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( 𝐴 ∈ ℤ ↔ ( abs ‘ 𝐴 ) ∈ ℤ ) ↔ ( 𝐴 ∈ ℤ ↔ - 𝐴 ∈ ℤ ) ) )
9	6 8	syl5ibrcom	⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) = - 𝐴 → ( 𝐴 ∈ ℤ ↔ ( abs ‘ 𝐴 ) ∈ ℤ ) ) )
10		absor	⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) = 𝐴 ∨ ( abs ‘ 𝐴 ) = - 𝐴 ) )
11	3 9 10	mpjaod	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℤ ↔ ( abs ‘ 𝐴 ) ∈ ℤ ) )