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∈ℝ→A∈ℤ↔A∈ℤ

Proof

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