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 ) ) )
7 6 3adant1 
 |-  ( ( 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 ) )
32 31 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) )
33 32 oveq2d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( abs ` K ) x. ( ( abs ` M ) gcd ( abs ` N ) ) ) = ( ( abs ` K ) x. ( M gcd N ) ) )
34 30 33 eqtrd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( ( abs ` K ) x. ( M gcd N ) ) )
35 7 12 34 3eqtr4rd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( abs ` ( K x. ( M gcd N ) ) ) )