Theorem gzsubcl

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

	Ref	Expression
Assertion	gzsubcl	|- ( ( 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		negsub	|- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
4	1 2 3	syl2an	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A + -u B ) = ( A - B ) )
5		gznegcl	|- ( B e. Z[i] -> -u B e. Z[i] )
6		gzaddcl	|- ( ( A e. Z[i] /\ -u B e. Z[i] ) -> ( A + -u B ) e. Z[i] )
7	5 6	sylan2	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A + -u B ) e. Z[i] )
8	4 7	eqeltrrd	|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A - B ) e. Z[i] )