Theorem gzaddcl

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

	Ref	Expression
Assertion	gzaddcl	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A + 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		addcl	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
4	1 2 3	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A + B ) e. CC )
5		readd	|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` B ) ) )
6	1 2 5	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` 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		zaddcl	|- ( ( ( Re ` A ) e. ZZ /\ ( Re ` B ) e. ZZ ) -> ( ( Re ` A ) + ( Re ` B ) ) e. ZZ )
12	8 10 11	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( Re ` A ) + ( Re ` B ) ) e. ZZ )
13	6 12	eqeltrd	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Re ` ( A + B ) ) e. ZZ )
14		imadd	|- ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) ) )
15	1 2 14	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) ) )
16	7	simp3bi	|- ( A e. Z[i] -> ( Im ` A ) e. ZZ )
17	9	simp3bi	|- ( B e. Z[i] -> ( Im ` B ) e. ZZ )
18		zaddcl	|- ( ( ( Im ` A ) e. ZZ /\ ( Im ` B ) e. ZZ ) -> ( ( Im ` A ) + ( Im ` B ) ) e. ZZ )
19	16 17 18	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( Im ` A ) + ( Im ` B ) ) e. ZZ )
20	15 19	eqeltrd	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Im ` ( A + B ) ) e. ZZ )
21		elgz	|- ( ( A + B ) e. Z[i] <-> ( ( A + B ) e. CC /\ ( Re ` ( A + B ) ) e. ZZ /\ ( Im ` ( A + B ) ) e. ZZ ) )
22	4 13 20 21	syl3anbrc	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A + B ) e. Z[i] )