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