Metamath Proof Explorer

Theorem gzabssqcl

Description: The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014)

Ref Expression
Assertion gzabssqcl ( 𝐴 ∈ ℤ[i] → ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 gzcn ⊢ ( 𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ )
2 1 absvalsq2d ⊢ ( 𝐴 ∈ ℤ[i] → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝐴 ) ↑ 2 ) + ( ( ℑ ‘ 𝐴 ) ↑ 2 ) ) )
3 elgz ⊢ ( 𝐴 ∈ ℤ[i] ↔ ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) )
4 3 simp2bi ⊢ ( 𝐴 ∈ ℤ[i] → ( ℜ ‘ 𝐴 ) ∈ ℤ )
5 zsqcl2 ⊢ ( ( ℜ ‘ 𝐴 ) ∈ ℤ → ( ( ℜ ‘ 𝐴 ) ↑ 2 ) ∈ ℕ0 )
6 4 5 syl ⊢ ( 𝐴 ∈ ℤ[i] → ( ( ℜ ‘ 𝐴 ) ↑ 2 ) ∈ ℕ0 )
7 3 simp3bi ⊢ ( 𝐴 ∈ ℤ[i] → ( ℑ ‘ 𝐴 ) ∈ ℤ )
8 zsqcl2 ⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℤ → ( ( ℑ ‘ 𝐴 ) ↑ 2 ) ∈ ℕ0 )
9 7 8 syl ⊢ ( 𝐴 ∈ ℤ[i] → ( ( ℑ ‘ 𝐴 ) ↑ 2 ) ∈ ℕ0 )
10 6 9 nn0addcld ⊢ ( 𝐴 ∈ ℤ[i] → ( ( ( ℜ ‘ 𝐴 ) ↑ 2 ) + ( ( ℑ ‘ 𝐴 ) ↑ 2 ) ) ∈ ℕ0 )
11 2 10 eqeltrd ⊢ ( 𝐴 ∈ ℤ[i] → ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℕ0 )