Metamath Proof Explorer

Theorem gcddvds

Description: The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 dvds0 
 |-  ( 0 e. ZZ -> 0 || 0 )
3 1 2 ax-mp 
 |-  0 || 0
4 breq2 
 |-  ( M = 0 -> ( 0 || M <-> 0 || 0 ) )
5 breq2 
 |-  ( N = 0 -> ( 0 || N <-> 0 || 0 ) )
6 4 5 bi2anan9 
 |-  ( ( M = 0 /\ N = 0 ) -> ( ( 0 || M /\ 0 || N ) <-> ( 0 || 0 /\ 0 || 0 ) ) )
7 anidm 
 |-  ( ( 0 || 0 /\ 0 || 0 ) <-> 0 || 0 )
8 6 7 bitrdi 
 |-  ( ( M = 0 /\ N = 0 ) -> ( ( 0 || M /\ 0 || N ) <-> 0 || 0 ) )
9 3 8 mpbiri 
 |-  ( ( M = 0 /\ N = 0 ) -> ( 0 || M /\ 0 || N ) )
10 oveq12 
 |-  ( ( M = 0 /\ N = 0 ) -> ( M gcd N ) = ( 0 gcd 0 ) )
11 gcd0val 
 |-  ( 0 gcd 0 ) = 0
12 10 11 eqtrdi 
 |-  ( ( M = 0 /\ N = 0 ) -> ( M gcd N ) = 0 )
13 12 breq1d 
 |-  ( ( M = 0 /\ N = 0 ) -> ( ( M gcd N ) || M <-> 0 || M ) )
14 12 breq1d 
 |-  ( ( M = 0 /\ N = 0 ) -> ( ( M gcd N ) || N <-> 0 || N ) )
15 13 14 anbi12d 
 |-  ( ( M = 0 /\ N = 0 ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || N ) <-> ( 0 || M /\ 0 || N ) ) )
16 9 15 mpbird 
 |-  ( ( M = 0 /\ N = 0 ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
17 16 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 /\ N = 0 ) ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
18 eqid 
 |-  { n e. ZZ | A. z e. { M , N } n || z } = { n e. ZZ | A. z e. { M , N } n || z }
19 eqid 
 |-  { n e. ZZ | ( n || M /\ n || N ) } = { n e. ZZ | ( n || M /\ n || N ) }
20 18 19 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 , < ) ) ) )
21 20 simp2d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) || M /\ sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) || N ) )
22 gcdn0val 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) )
23 22 breq1d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( M gcd N ) || M <-> sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) || M ) )
24 22 breq1d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( M gcd N ) || N <-> sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) || N ) )
25 23 24 anbi12d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || N ) <-> ( sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) || M /\ sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) || N ) ) )
26 21 25 mpbird 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
27 17 26 pm2.61dan 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )