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 ) )