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 ∈ ℤ