# Metamath Proof Explorer

## Theorem gcdmultipleOLD

Description: Obsolete proof of gcdmultiple as of 12-Jan-2024. The GCD of a multiple of a number is the number itself. (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 oveq2
` |-  ( k = 1 -> ( M x. k ) = ( M x. 1 ) )`
2 1 oveq2d
` |-  ( k = 1 -> ( M gcd ( M x. k ) ) = ( M gcd ( M x. 1 ) ) )`
3 2 eqeq1d
` |-  ( k = 1 -> ( ( M gcd ( M x. k ) ) = M <-> ( M gcd ( M x. 1 ) ) = M ) )`
4 3 imbi2d
` |-  ( k = 1 -> ( ( M e. NN -> ( M gcd ( M x. k ) ) = M ) <-> ( M e. NN -> ( M gcd ( M x. 1 ) ) = M ) ) )`
5 oveq2
` |-  ( k = n -> ( M x. k ) = ( M x. n ) )`
6 5 oveq2d
` |-  ( k = n -> ( M gcd ( M x. k ) ) = ( M gcd ( M x. n ) ) )`
7 6 eqeq1d
` |-  ( k = n -> ( ( M gcd ( M x. k ) ) = M <-> ( M gcd ( M x. n ) ) = M ) )`
8 7 imbi2d
` |-  ( k = n -> ( ( M e. NN -> ( M gcd ( M x. k ) ) = M ) <-> ( M e. NN -> ( M gcd ( M x. n ) ) = M ) ) )`
9 oveq2
` |-  ( k = ( n + 1 ) -> ( M x. k ) = ( M x. ( n + 1 ) ) )`
10 9 oveq2d
` |-  ( k = ( n + 1 ) -> ( M gcd ( M x. k ) ) = ( M gcd ( M x. ( n + 1 ) ) ) )`
11 10 eqeq1d
` |-  ( k = ( n + 1 ) -> ( ( M gcd ( M x. k ) ) = M <-> ( M gcd ( M x. ( n + 1 ) ) ) = M ) )`
12 11 imbi2d
` |-  ( k = ( n + 1 ) -> ( ( M e. NN -> ( M gcd ( M x. k ) ) = M ) <-> ( M e. NN -> ( M gcd ( M x. ( n + 1 ) ) ) = M ) ) )`
13 oveq2
` |-  ( k = N -> ( M x. k ) = ( M x. N ) )`
14 13 oveq2d
` |-  ( k = N -> ( M gcd ( M x. k ) ) = ( M gcd ( M x. N ) ) )`
15 14 eqeq1d
` |-  ( k = N -> ( ( M gcd ( M x. k ) ) = M <-> ( M gcd ( M x. N ) ) = M ) )`
16 15 imbi2d
` |-  ( k = N -> ( ( M e. NN -> ( M gcd ( M x. k ) ) = M ) <-> ( M e. NN -> ( M gcd ( M x. N ) ) = M ) ) )`
17 nncn
` |-  ( M e. NN -> M e. CC )`
18 17 mulid1d
` |-  ( M e. NN -> ( M x. 1 ) = M )`
19 18 oveq2d
` |-  ( M e. NN -> ( M gcd ( M x. 1 ) ) = ( M gcd M ) )`
20 nnz
` |-  ( M e. NN -> M e. ZZ )`
21 gcdid
` |-  ( M e. ZZ -> ( M gcd M ) = ( abs ` M ) )`
22 20 21 syl
` |-  ( M e. NN -> ( M gcd M ) = ( abs ` M ) )`
23 nnre
` |-  ( M e. NN -> M e. RR )`
24 nnnn0
` |-  ( M e. NN -> M e. NN0 )`
25 24 nn0ge0d
` |-  ( M e. NN -> 0 <_ M )`
26 23 25 absidd
` |-  ( M e. NN -> ( abs ` M ) = M )`
27 22 26 eqtrd
` |-  ( M e. NN -> ( M gcd M ) = M )`
28 19 27 eqtrd
` |-  ( M e. NN -> ( M gcd ( M x. 1 ) ) = M )`
29 1z
` |-  1 e. ZZ`
30 nnz
` |-  ( n e. NN -> n e. ZZ )`
31 zmulcl
` |-  ( ( M e. ZZ /\ n e. ZZ ) -> ( M x. n ) e. ZZ )`
32 20 30 31 syl2an
` |-  ( ( M e. NN /\ n e. NN ) -> ( M x. n ) e. ZZ )`
` |-  ( ( 1 e. ZZ /\ M e. ZZ /\ ( M x. n ) e. ZZ ) -> ( M gcd ( M x. n ) ) = ( M gcd ( ( M x. n ) + ( 1 x. M ) ) ) )`
34 29 20 32 33 mp3an2ani
` |-  ( ( M e. NN /\ n e. NN ) -> ( M gcd ( M x. n ) ) = ( M gcd ( ( M x. n ) + ( 1 x. M ) ) ) )`
35 nncn
` |-  ( n e. NN -> n e. CC )`
36 ax-1cn
` |-  1 e. CC`
` |-  ( ( M e. CC /\ n e. CC /\ 1 e. CC ) -> ( M x. ( n + 1 ) ) = ( ( M x. n ) + ( M x. 1 ) ) )`
38 36 37 mp3an3
` |-  ( ( M e. CC /\ n e. CC ) -> ( M x. ( n + 1 ) ) = ( ( M x. n ) + ( M x. 1 ) ) )`
39 mulcom
` |-  ( ( M e. CC /\ 1 e. CC ) -> ( M x. 1 ) = ( 1 x. M ) )`
40 36 39 mpan2
` |-  ( M e. CC -> ( M x. 1 ) = ( 1 x. M ) )`
` |-  ( ( M e. CC /\ n e. CC ) -> ( M x. 1 ) = ( 1 x. M ) )`
42 41 oveq2d
` |-  ( ( M e. CC /\ n e. CC ) -> ( ( M x. n ) + ( M x. 1 ) ) = ( ( M x. n ) + ( 1 x. M ) ) )`
43 38 42 eqtrd
` |-  ( ( M e. CC /\ n e. CC ) -> ( M x. ( n + 1 ) ) = ( ( M x. n ) + ( 1 x. M ) ) )`
44 17 35 43 syl2an
` |-  ( ( M e. NN /\ n e. NN ) -> ( M x. ( n + 1 ) ) = ( ( M x. n ) + ( 1 x. M ) ) )`
45 44 oveq2d
` |-  ( ( M e. NN /\ n e. NN ) -> ( M gcd ( M x. ( n + 1 ) ) ) = ( M gcd ( ( M x. n ) + ( 1 x. M ) ) ) )`
46 34 45 eqtr4d
` |-  ( ( M e. NN /\ n e. NN ) -> ( M gcd ( M x. n ) ) = ( M gcd ( M x. ( n + 1 ) ) ) )`
47 46 eqeq1d
` |-  ( ( M e. NN /\ n e. NN ) -> ( ( M gcd ( M x. n ) ) = M <-> ( M gcd ( M x. ( n + 1 ) ) ) = M ) )`
48 47 biimpd
` |-  ( ( M e. NN /\ n e. NN ) -> ( ( M gcd ( M x. n ) ) = M -> ( M gcd ( M x. ( n + 1 ) ) ) = M ) )`
49 48 expcom
` |-  ( n e. NN -> ( M e. NN -> ( ( M gcd ( M x. n ) ) = M -> ( M gcd ( M x. ( n + 1 ) ) ) = M ) ) )`
50 49 a2d
` |-  ( n e. NN -> ( ( M e. NN -> ( M gcd ( M x. n ) ) = M ) -> ( M e. NN -> ( M gcd ( M x. ( n + 1 ) ) ) = M ) ) )`
51 4 8 12 16 28 50 nnind
` |-  ( N e. NN -> ( M e. NN -> ( M gcd ( M x. N ) ) = M ) )`
52 51 impcom
` |-  ( ( M e. NN /\ N e. NN ) -> ( M gcd ( M x. N ) ) = M )`