Metamath Proof Explorer

Theorem gzreim

Description: Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014)

Ref Expression
Assertion gzreim 
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A + ( _i x. B ) ) e. Z[i] )

Proof

Step Hyp Ref Expression
1 zgz 
 |-  ( A e. ZZ -> A e. Z[i] )
2 igz 
 |-  _i e. Z[i]
3 zgz 
 |-  ( B e. ZZ -> B e. Z[i] )
4 gzmulcl 
 |-  ( ( _i e. Z[i] /\ B e. Z[i] ) -> ( _i x. B ) e. Z[i] )
5 2 3 4 sylancr 
 |-  ( B e. ZZ -> ( _i x. B ) e. Z[i] )
6 gzaddcl 
 |-  ( ( A e. Z[i] /\ ( _i x. B ) e. Z[i] ) -> ( A + ( _i x. B ) ) e. Z[i] )
7 1 5 6 syl2an 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + ( _i x. B ) ) e. Z[i] )