Theorem gcdn0cl

Description: Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011)

	Ref	Expression
Assertion	gcdn0cl	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		gcdn0val	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) )
2		eqid	|- { n e. ZZ | A. z e. { M , N } n || z } = { n e. ZZ | A. z e. { M , N } n || z }
3		eqid	|- { n e. ZZ | ( n || M /\ n || N ) } = { n e. ZZ | ( n || M /\ n || N ) }
4	2 3	gcdcllem3	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) e. NN /\ ( sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) || M /\ sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) || N ) /\ ( ( K e. ZZ /\ K || M /\ K || N ) -> K <_ sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) ) )
5	4	simp1d	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) e. NN )
6	1 5	eqeltrd	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) e. NN )