Metamath Proof Explorer

Theorem elgz

Description: Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion elgz ⊢ A ∈ ℤ i ↔ A ∈ ℂ ∧ ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ A ∈ ℤ

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ x = A → ℜ ⁡ x = ℜ ⁡ A
2 1 eleq1d ⊢ x = A → ℜ ⁡ x ∈ ℤ ↔ ℜ ⁡ A ∈ ℤ
3 fveq2 ⊢ x = A → ℑ ⁡ x = ℑ ⁡ A
4 3 eleq1d ⊢ x = A → ℑ ⁡ x ∈ ℤ ↔ ℑ ⁡ A ∈ ℤ
5 2 4 anbi12d ⊢ x = A → ℜ ⁡ x ∈ ℤ ∧ ℑ ⁡ x ∈ ℤ ↔ ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ A ∈ ℤ
6 df-gz ⊢ ℤ i = x ∈ ℂ | ℜ ⁡ x ∈ ℤ ∧ ℑ ⁡ x ∈ ℤ
7 5 6 elrab2 ⊢ A ∈ ℤ i ↔ A ∈ ℂ ∧ ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ A ∈ ℤ
8 3anass ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ A ∈ ℤ ↔ A ∈ ℂ ∧ ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ A ∈ ℤ
9 7 8 bitr4i ⊢ A ∈ ℤ i ↔ A ∈ ℂ ∧ ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ A ∈ ℤ