Theorem elgz

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

	Ref	Expression
Assertion	elgz	⊢ ( 𝐴 ∈ ℤ[i] ↔ ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝐴 → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ 𝐴 ) )
2	1	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( ℜ ‘ 𝑥 ) ∈ ℤ ↔ ( ℜ ‘ 𝐴 ) ∈ ℤ ) )
3		fveq2	⊢ ( 𝑥 = 𝐴 → ( ℑ ‘ 𝑥 ) = ( ℑ ‘ 𝐴 ) )
4	3	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( ℑ ‘ 𝑥 ) ∈ ℤ ↔ ( ℑ ‘ 𝐴 ) ∈ ℤ ) )
5	2 4	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( ℜ ‘ 𝑥 ) ∈ ℤ ∧ ( ℑ ‘ 𝑥 ) ∈ ℤ ) ↔ ( ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) ) )
6		df-gz	⊢ ℤ[i] = { 𝑥 ∈ ℂ ∣ ( ( ℜ ‘ 𝑥 ) ∈ ℤ ∧ ( ℑ ‘ 𝑥 ) ∈ ℤ ) }
7	5 6	elrab2	⊢ ( 𝐴 ∈ ℤ[i] ↔ ( 𝐴 ∈ ℂ ∧ ( ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) ) )
8		3anass	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) ↔ ( 𝐴 ∈ ℂ ∧ ( ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) ) )
9	7 8	bitr4i	⊢ ( 𝐴 ∈ ℤ[i] ↔ ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) )