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 
|- ( A e. Z[i] -> ( ( abs ` A ) ^ 2 ) e. NN0 )

Proof

Step Hyp Ref Expression
1 gzcn 
 |-  ( A e. Z[i] -> A e. CC )
2 1 absvalsq2d 
 |-  ( A e. Z[i] -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
3 elgz 
 |-  ( A e. Z[i] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )
4 3 simp2bi 
 |-  ( A e. Z[i] -> ( Re ` A ) e. ZZ )
5 zsqcl2 
 |-  ( ( Re ` A ) e. ZZ -> ( ( Re ` A ) ^ 2 ) e. NN0 )
6 4 5 syl 
 |-  ( A e. Z[i] -> ( ( Re ` A ) ^ 2 ) e. NN0 )
7 3 simp3bi 
 |-  ( A e. Z[i] -> ( Im ` A ) e. ZZ )
8 zsqcl2 
 |-  ( ( Im ` A ) e. ZZ -> ( ( Im ` A ) ^ 2 ) e. NN0 )
9 7 8 syl 
 |-  ( A e. Z[i] -> ( ( Im ` A ) ^ 2 ) e. NN0 )
10 6 9 nn0addcld 
 |-  ( A e. Z[i] -> ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) e. NN0 )
11 2 10 eqeltrd 
 |-  ( A e. Z[i] -> ( ( abs ` A ) ^ 2 ) e. NN0 )