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 )
33 gcdaddm 
 |-  ( ( 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
37 adddi 
 |-  ( ( 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 ) )
41 40 adantr 
 |-  ( ( 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 )