This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gcdcom

Description: The gcd operator is commutative. Theorem 1.4(a) in ApostolNT p. 16. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 ancom 
 |-  ( ( M = 0 /\ N = 0 ) <-> ( N = 0 /\ M = 0 ) )
2 ancom 
 |-  ( ( n || M /\ n || N ) <-> ( n || N /\ n || M ) )
3 2 rabbii 
 |-  { n e. ZZ | ( n || M /\ n || N ) } = { n e. ZZ | ( n || N /\ n || M ) }
4 3 supeq1i 
 |-  sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) = sup ( { n e. ZZ | ( n || N /\ n || M ) } , RR , < )
5 1 4 ifbieq2i 
 |-  if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) = if ( ( N = 0 /\ M = 0 ) , 0 , sup ( { n e. ZZ | ( n || N /\ n || M ) } , RR , < ) )
6 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 , < ) ) )
7 gcdval 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N gcd M ) = if ( ( N = 0 /\ M = 0 ) , 0 , sup ( { n e. ZZ | ( n || N /\ n || M ) } , RR , < ) ) )
8 7 ancoms 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N gcd M ) = if ( ( N = 0 /\ M = 0 ) , 0 , sup ( { n e. ZZ | ( n || N /\ n || M ) } , RR , < ) ) )
9 5 6 8 3eqtr4a 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( N gcd M ) )