# Metamath Proof Explorer

## Theorem absmulgcd

Description: Distribute absolute value of multiplication over gcd. Theorem 1.4(c) in ApostolNT p. 16. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion absmulgcd
`|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( abs ` ( K x. ( M gcd N ) ) ) )`

### Proof

Step Hyp Ref Expression
1 gcdcl
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )`
2 nn0re
` |-  ( ( M gcd N ) e. NN0 -> ( M gcd N ) e. RR )`
3 nn0ge0
` |-  ( ( M gcd N ) e. NN0 -> 0 <_ ( M gcd N ) )`
4 2 3 absidd
` |-  ( ( M gcd N ) e. NN0 -> ( abs ` ( M gcd N ) ) = ( M gcd N ) )`
5 1 4 syl
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( abs ` ( M gcd N ) ) = ( M gcd N ) )`
6 5 oveq2d
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` K ) x. ( abs ` ( M gcd N ) ) ) = ( ( abs ` K ) x. ( M gcd N ) ) )`
` |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( abs ` K ) x. ( abs ` ( M gcd N ) ) ) = ( ( abs ` K ) x. ( M gcd N ) ) )`
8 zcn
` |-  ( K e. ZZ -> K e. CC )`
9 1 nn0cnd
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. CC )`
10 absmul
` |-  ( ( K e. CC /\ ( M gcd N ) e. CC ) -> ( abs ` ( K x. ( M gcd N ) ) ) = ( ( abs ` K ) x. ( abs ` ( M gcd N ) ) ) )`
11 8 9 10 syl2an
` |-  ( ( K e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( abs ` ( K x. ( M gcd N ) ) ) = ( ( abs ` K ) x. ( abs ` ( M gcd N ) ) ) )`
12 11 3impb
` |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( abs ` ( K x. ( M gcd N ) ) ) = ( ( abs ` K ) x. ( abs ` ( M gcd N ) ) ) )`
13 zcn
` |-  ( M e. ZZ -> M e. CC )`
14 zcn
` |-  ( N e. ZZ -> N e. CC )`
15 absmul
` |-  ( ( K e. CC /\ M e. CC ) -> ( abs ` ( K x. M ) ) = ( ( abs ` K ) x. ( abs ` M ) ) )`
16 absmul
` |-  ( ( K e. CC /\ N e. CC ) -> ( abs ` ( K x. N ) ) = ( ( abs ` K ) x. ( abs ` N ) ) )`
17 15 16 oveqan12d
` |-  ( ( ( K e. CC /\ M e. CC ) /\ ( K e. CC /\ N e. CC ) ) -> ( ( abs ` ( K x. M ) ) gcd ( abs ` ( K x. N ) ) ) = ( ( ( abs ` K ) x. ( abs ` M ) ) gcd ( ( abs ` K ) x. ( abs ` N ) ) ) )`
18 17 3impdi
` |-  ( ( K e. CC /\ M e. CC /\ N e. CC ) -> ( ( abs ` ( K x. M ) ) gcd ( abs ` ( K x. N ) ) ) = ( ( ( abs ` K ) x. ( abs ` M ) ) gcd ( ( abs ` K ) x. ( abs ` N ) ) ) )`
19 8 13 14 18 syl3an
` |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( K x. M ) ) gcd ( abs ` ( K x. N ) ) ) = ( ( ( abs ` K ) x. ( abs ` M ) ) gcd ( ( abs ` K ) x. ( abs ` N ) ) ) )`
20 zmulcl
` |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( K x. M ) e. ZZ )`
21 zmulcl
` |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( K x. N ) e. ZZ )`
22 gcdabs
` |-  ( ( ( K x. M ) e. ZZ /\ ( K x. N ) e. ZZ ) -> ( ( abs ` ( K x. M ) ) gcd ( abs ` ( K x. N ) ) ) = ( ( K x. M ) gcd ( K x. N ) ) )`
23 20 21 22 syl2an
` |-  ( ( ( K e. ZZ /\ M e. ZZ ) /\ ( K e. ZZ /\ N e. ZZ ) ) -> ( ( abs ` ( K x. M ) ) gcd ( abs ` ( K x. N ) ) ) = ( ( K x. M ) gcd ( K x. N ) ) )`
24 23 3impdi
` |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( K x. M ) ) gcd ( abs ` ( K x. N ) ) ) = ( ( K x. M ) gcd ( K x. N ) ) )`
25 nn0abscl
` |-  ( K e. ZZ -> ( abs ` K ) e. NN0 )`
26 zabscl
` |-  ( M e. ZZ -> ( abs ` M ) e. ZZ )`
27 zabscl
` |-  ( N e. ZZ -> ( abs ` N ) e. ZZ )`
28 mulgcd
` |-  ( ( ( abs ` K ) e. NN0 /\ ( abs ` M ) e. ZZ /\ ( abs ` N ) e. ZZ ) -> ( ( ( abs ` K ) x. ( abs ` M ) ) gcd ( ( abs ` K ) x. ( abs ` N ) ) ) = ( ( abs ` K ) x. ( ( abs ` M ) gcd ( abs ` N ) ) ) )`
29 25 26 27 28 syl3an
` |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` K ) x. ( abs ` M ) ) gcd ( ( abs ` K ) x. ( abs ` N ) ) ) = ( ( abs ` K ) x. ( ( abs ` M ) gcd ( abs ` N ) ) ) )`
30 19 24 29 3eqtr3d
` |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( ( abs ` K ) x. ( ( abs ` M ) gcd ( abs ` N ) ) ) )`
31 gcdabs
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) )`
` |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) )`
` |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( abs ` K ) x. ( ( abs ` M ) gcd ( abs ` N ) ) ) = ( ( abs ` K ) x. ( M gcd N ) ) )`
` |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( ( abs ` K ) x. ( M gcd N ) ) )`
` |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( abs ` ( K x. ( M gcd N ) ) ) )`