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 ) ) )
13 12 adantr 
 |-  ( ( 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 ) ) ) )
16 15 adantr 
 |-  ( ( ( 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 )
22 21 adantr 
 |-  ( ( ( 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 ) )
33 32 adantr 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. 0 ) ) = ( M gcd 0 ) )
34 nn0gcdid0 
 |-  ( M e. NN0 -> ( M gcd 0 ) = M )
35 9 34 syl 
 |-  ( M e. NN -> ( M gcd 0 ) = M )
36 35 adantr 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd 0 ) = M )
37 33 36 eqtrd 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. 0 ) ) = M )
38 3 29 37 pm2.61ne 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. N ) ) = M )