Theorem gcdval

Description: The value of the gcd operator. ( M gcd N ) is the greatest common divisor of M and N . If M and N are both 0 , the result is defined conventionally as 0 . (Contributed by Paul Chapman, 21-Mar-2011) (Revised by Mario Carneiro, 10-Nov-2013)

	Ref	Expression
Assertion	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 , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	|- ( x = M -> ( x = 0 <-> M = 0 ) )
2	1	anbi1d	|- ( x = M -> ( ( x = 0 /\ y = 0 ) <-> ( M = 0 /\ y = 0 ) ) )
3		breq2	|- ( x = M -> ( n || x <-> n || M ) )
4	3	anbi1d	|- ( x = M -> ( ( n || x /\ n || y ) <-> ( n || M /\ n || y ) ) )
5	4	rabbidv	|- ( x = M -> { n e. ZZ | ( n || x /\ n || y ) } = { n e. ZZ | ( n || M /\ n || y ) } )
6	5	supeq1d	|- ( x = M -> sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) = sup ( { n e. ZZ | ( n || M /\ n || y ) } , RR , < ) )
7	2 6	ifbieq2d	|- ( x = M -> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) = if ( ( M = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || y ) } , RR , < ) ) )
8		eqeq1	|- ( y = N -> ( y = 0 <-> N = 0 ) )
9	8	anbi2d	|- ( y = N -> ( ( M = 0 /\ y = 0 ) <-> ( M = 0 /\ N = 0 ) ) )
10		breq2	|- ( y = N -> ( n || y <-> n || N ) )
11	10	anbi2d	|- ( y = N -> ( ( n || M /\ n || y ) <-> ( n || M /\ n || N ) ) )
12	11	rabbidv	|- ( y = N -> { n e. ZZ | ( n || M /\ n || y ) } = { n e. ZZ | ( n || M /\ n || N ) } )
13	12	supeq1d	|- ( y = N -> sup ( { n e. ZZ | ( n || M /\ n || y ) } , RR , < ) = sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) )
14	9 13	ifbieq2d	|- ( y = N -> if ( ( M = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || y ) } , RR , < ) ) = if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) )
15		df-gcd	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
16		c0ex	|- 0 e. _V
17		ltso	|- < Or RR
18	17	supex	|- sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) e. _V
19	16 18	ifex	|- if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) e. _V
20	7 14 15 19	ovmpo	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) )