# Metamath Proof Explorer

## Theorem gcdmultiplezOLD

Description: Obsolete proof of gcdmultiplez as of 12-Jan-2024. Extend gcdmultiple so N can be an integer. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion gcdmultiplezOLD
`|- ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. N ) ) = M )`

### Proof

Step Hyp Ref Expression
1 oveq2
` |-  ( N = 0 -> ( M x. N ) = ( M x. 0 ) )`
2 1 oveq2d
` |-  ( N = 0 -> ( M gcd ( M x. N ) ) = ( M gcd ( M x. 0 ) ) )`
3 2 eqeq1d
` |-  ( N = 0 -> ( ( M gcd ( M x. N ) ) = M <-> ( M gcd ( M x. 0 ) ) = M ) )`
4 nncn
` |-  ( M e. NN -> M e. CC )`
5 zcn
` |-  ( N e. ZZ -> N e. CC )`
6 absmul
` |-  ( ( M e. CC /\ N e. CC ) -> ( abs ` ( M x. N ) ) = ( ( abs ` M ) x. ( abs ` N ) ) )`
7 4 5 6 syl2an
` |-  ( ( M e. NN /\ N e. ZZ ) -> ( abs ` ( M x. N ) ) = ( ( abs ` M ) x. ( abs ` N ) ) )`
8 nnre
` |-  ( M e. NN -> M e. RR )`
9 nnnn0
` |-  ( M e. NN -> M e. NN0 )`
10 9 nn0ge0d
` |-  ( M e. NN -> 0 <_ M )`
11 8 10 absidd
` |-  ( M e. NN -> ( abs ` M ) = M )`
12 11 oveq1d
` |-  ( M e. NN -> ( ( abs ` M ) x. ( abs ` N ) ) = ( M x. ( abs ` N ) ) )`
` |-  ( ( M e. NN /\ N e. ZZ ) -> ( ( abs ` M ) x. ( abs ` N ) ) = ( M x. ( abs ` N ) ) )`
14 7 13 eqtrd
` |-  ( ( M e. NN /\ N e. ZZ ) -> ( abs ` ( M x. N ) ) = ( M x. ( abs ` N ) ) )`
15 14 oveq2d
` |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( abs ` ( M x. N ) ) ) = ( M gcd ( M x. ( abs ` N ) ) ) )`
` |-  ( ( ( M e. NN /\ N e. ZZ ) /\ N =/= 0 ) -> ( M gcd ( abs ` ( M x. N ) ) ) = ( M gcd ( M x. ( abs ` N ) ) ) )`
17 simpll
` |-  ( ( ( M e. NN /\ N e. ZZ ) /\ N =/= 0 ) -> M e. NN )`
18 17 nnzd
` |-  ( ( ( M e. NN /\ N e. ZZ ) /\ N =/= 0 ) -> M e. ZZ )`
19 nnz
` |-  ( M e. NN -> M e. ZZ )`
20 zmulcl
` |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )`
21 19 20 sylan
` |-  ( ( M e. NN /\ N e. ZZ ) -> ( M x. N ) e. ZZ )`
` |-  ( ( ( M e. NN /\ N e. ZZ ) /\ N =/= 0 ) -> ( M x. N ) e. ZZ )`
23 gcdabs2
` |-  ( ( M e. ZZ /\ ( M x. N ) e. ZZ ) -> ( M gcd ( abs ` ( M x. N ) ) ) = ( M gcd ( M x. N ) ) )`
24 18 22 23 syl2anc
` |-  ( ( ( M e. NN /\ N e. ZZ ) /\ N =/= 0 ) -> ( M gcd ( abs ` ( M x. N ) ) ) = ( M gcd ( M x. N ) ) )`
25 nnabscl
` |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN )`
26 gcdmultiple
` |-  ( ( M e. NN /\ ( abs ` N ) e. NN ) -> ( M gcd ( M x. ( abs ` N ) ) ) = M )`
27 25 26 sylan2
` |-  ( ( M e. NN /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( M gcd ( M x. ( abs ` N ) ) ) = M )`
28 27 anassrs
` |-  ( ( ( M e. NN /\ N e. ZZ ) /\ N =/= 0 ) -> ( M gcd ( M x. ( abs ` N ) ) ) = M )`
29 16 24 28 3eqtr3d
` |-  ( ( ( M e. NN /\ N e. ZZ ) /\ N =/= 0 ) -> ( M gcd ( M x. N ) ) = M )`
30 mul01
` |-  ( M e. CC -> ( M x. 0 ) = 0 )`
31 30 oveq2d
` |-  ( M e. CC -> ( M gcd ( M x. 0 ) ) = ( M gcd 0 ) )`
32 4 31 syl
` |-  ( M e. NN -> ( M gcd ( M x. 0 ) ) = ( M gcd 0 ) )`
` |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. 0 ) ) = ( M gcd 0 ) )`
` |-  ( M e. NN0 -> ( M gcd 0 ) = M )`
` |-  ( M e. NN -> ( M gcd 0 ) = M )`
` |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd 0 ) = M )`
` |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. 0 ) ) = M )`
` |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. N ) ) = M )`