Theorem gzmulcl

Description: The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Assertion	gzmulcl	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A x. B ) e. Z[i] )

Proof

Step	Hyp	Ref	Expression
1		gzcn	|- ( A e. Z[i] -> A e. CC )
2		gzcn	|- ( B e. Z[i] -> B e. CC )
3		mulcl	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
4	1 2 3	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A x. B ) e. CC )
5		remul	|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) )
6	1 2 5	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) )
7		elgz	|- ( A e. Z[i] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )
8	7	simp2bi	|- ( A e. Z[i] -> ( Re ` A ) e. ZZ )
9		elgz	|- ( B e. Z[i] <-> ( B e. CC /\ ( Re ` B ) e. ZZ /\ ( Im ` B ) e. ZZ ) )
10	9	simp2bi	|- ( B e. Z[i] -> ( Re ` B ) e. ZZ )
11		zmulcl	|- ( ( ( Re ` A ) e. ZZ /\ ( Re ` B ) e. ZZ ) -> ( ( Re ` A ) x. ( Re ` B ) ) e. ZZ )
12	8 10 11	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( Re ` A ) x. ( Re ` B ) ) e. ZZ )
13	7	simp3bi	|- ( A e. Z[i] -> ( Im ` A ) e. ZZ )
14	9	simp3bi	|- ( B e. Z[i] -> ( Im ` B ) e. ZZ )
15		zmulcl	|- ( ( ( Im ` A ) e. ZZ /\ ( Im ` B ) e. ZZ ) -> ( ( Im ` A ) x. ( Im ` B ) ) e. ZZ )
16	13 14 15	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( Im ` A ) x. ( Im ` B ) ) e. ZZ )
17	12 16	zsubcld	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) e. ZZ )
18	6 17	eqeltrd	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Re ` ( A x. B ) ) e. ZZ )
19		immul	|- ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
20	1 2 19	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
21		zmulcl	|- ( ( ( Re ` A ) e. ZZ /\ ( Im ` B ) e. ZZ ) -> ( ( Re ` A ) x. ( Im ` B ) ) e. ZZ )
22	8 14 21	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( Re ` A ) x. ( Im ` B ) ) e. ZZ )
23		zmulcl	|- ( ( ( Im ` A ) e. ZZ /\ ( Re ` B ) e. ZZ ) -> ( ( Im ` A ) x. ( Re ` B ) ) e. ZZ )
24	13 10 23	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( Im ` A ) x. ( Re ` B ) ) e. ZZ )
25	22 24	zaddcld	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) e. ZZ )
26	20 25	eqeltrd	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Im ` ( A x. B ) ) e. ZZ )
27		elgz	|- ( ( A x. B ) e. Z[i] <-> ( ( A x. B ) e. CC /\ ( Re ` ( A x. B ) ) e. ZZ /\ ( Im ` ( A x. B ) ) e. ZZ ) )
28	4 18 26 27	syl3anbrc	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A x. B ) e. Z[i] )