Metamath Proof Explorer

Theorem gcdn0val

Description: The value of the gcd operator when at least one operand is nonzero. (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	gcdn0val	\|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = sup ( { n e. ZZ \| ( n \|\| M /\ n \|\| N ) } , RR , < ) )

Proof

Step	Hyp	Ref	Expression
1		gcdval	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ \| ( n \|\| M /\ n \|\| N ) } , RR , < ) ) )
2		iffalse	\|- ( -. ( M = 0 /\ N = 0 ) -> if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ \| ( n \|\| M /\ n \|\| N ) } , RR , < ) ) = sup ( { n e. ZZ \| ( n \|\| M /\ n \|\| N ) } , RR , < ) )
3	1 2	sylan9eq	\|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = sup ( { n e. ZZ \| ( n \|\| M /\ n \|\| N ) } , RR , < ) )

Step

Hyp

Ref

Expression

gcdval

 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) )

iffalse

 |-  ( -. ( M = 0 /\ N = 0 ) -> if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) = sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) )

1 2

sylan9eq

 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) )