Metamath Proof Explorer

Theorem gcdaddmlem

Description: Lemma for gcdaddm . (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Hypotheses gcdaddmlem.1 
|- K e. ZZ
gcdaddmlem.2 
|- M e. ZZ
gcdaddmlem.3 
|- N e. ZZ
Assertion gcdaddmlem 
|- ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) )

Proof

Step Hyp Ref Expression
1 gcdaddmlem.1 
 |-  K e. ZZ
2 gcdaddmlem.2 
 |-  M e. ZZ
3 gcdaddmlem.3 
 |-  N e. ZZ
4 gcddvds 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
5 2 3 4 mp2an 
 |-  ( ( M gcd N ) || M /\ ( M gcd N ) || N )
6 5 simpli 
 |-  ( M gcd N ) || M
7 gcdcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )
8 2 3 7 mp2an 
 |-  ( M gcd N ) e. NN0
9 8 nn0zi 
 |-  ( M gcd N ) e. ZZ
10 1z 
 |-  1 e. ZZ
11 dvds2ln 
 |-  ( ( ( K e. ZZ /\ 1 e. ZZ ) /\ ( ( M gcd N ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || N ) -> ( M gcd N ) || ( ( K x. M ) + ( 1 x. N ) ) ) )
12 1 10 11 mpanl12 
 |-  ( ( ( M gcd N ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || N ) -> ( M gcd N ) || ( ( K x. M ) + ( 1 x. N ) ) ) )
13 9 2 3 12 mp3an 
 |-  ( ( ( M gcd N ) || M /\ ( M gcd N ) || N ) -> ( M gcd N ) || ( ( K x. M ) + ( 1 x. N ) ) )
14 5 13 ax-mp 
 |-  ( M gcd N ) || ( ( K x. M ) + ( 1 x. N ) )
15 zcn 
 |-  ( N e. ZZ -> N e. CC )
16 3 15 ax-mp 
 |-  N e. CC
17 16 mulid2i 
 |-  ( 1 x. N ) = N
18 17 oveq2i 
 |-  ( ( K x. M ) + ( 1 x. N ) ) = ( ( K x. M ) + N )
19 14 18 breqtri 
 |-  ( M gcd N ) || ( ( K x. M ) + N )
20 zmulcl 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( K x. M ) e. ZZ )
21 1 2 20 mp2an 
 |-  ( K x. M ) e. ZZ
22 zaddcl 
 |-  ( ( ( K x. M ) e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) + N ) e. ZZ )
23 21 3 22 mp2an 
 |-  ( ( K x. M ) + N ) e. ZZ
24 dvdslegcd 
 |-  ( ( ( ( M gcd N ) e. ZZ /\ M e. ZZ /\ ( ( K x. M ) + N ) e. ZZ ) /\ -. ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || ( ( K x. M ) + N ) ) -> ( M gcd N ) <_ ( M gcd ( ( K x. M ) + N ) ) ) )
25 24 ex 
 |-  ( ( ( M gcd N ) e. ZZ /\ M e. ZZ /\ ( ( K x. M ) + N ) e. ZZ ) -> ( -. ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || ( ( K x. M ) + N ) ) -> ( M gcd N ) <_ ( M gcd ( ( K x. M ) + N ) ) ) ) )
26 9 2 23 25 mp3an 
 |-  ( -. ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || ( ( K x. M ) + N ) ) -> ( M gcd N ) <_ ( M gcd ( ( K x. M ) + N ) ) ) )
27 6 19 26 mp2ani 
 |-  ( -. ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) -> ( M gcd N ) <_ ( M gcd ( ( K x. M ) + N ) ) )
28 gcddvds 
 |-  ( ( M e. ZZ /\ ( ( K x. M ) + N ) e. ZZ ) -> ( ( M gcd ( ( K x. M ) + N ) ) || M /\ ( M gcd ( ( K x. M ) + N ) ) || ( ( K x. M ) + N ) ) )
29 2 23 28 mp2an 
 |-  ( ( M gcd ( ( K x. M ) + N ) ) || M /\ ( M gcd ( ( K x. M ) + N ) ) || ( ( K x. M ) + N ) )
30 29 simpli 
 |-  ( M gcd ( ( K x. M ) + N ) ) || M
31 gcdcl 
 |-  ( ( M e. ZZ /\ ( ( K x. M ) + N ) e. ZZ ) -> ( M gcd ( ( K x. M ) + N ) ) e. NN0 )
32 2 23 31 mp2an 
 |-  ( M gcd ( ( K x. M ) + N ) ) e. NN0
33 32 nn0zi 
 |-  ( M gcd ( ( K x. M ) + N ) ) e. ZZ
34 znegcl 
 |-  ( K e. ZZ -> -u K e. ZZ )
35 1 34 ax-mp 
 |-  -u K e. ZZ
36 dvds2ln 
 |-  ( ( ( -u K e. ZZ /\ 1 e. ZZ ) /\ ( ( M gcd ( ( K x. M ) + N ) ) e. ZZ /\ M e. ZZ /\ ( ( K x. M ) + N ) e. ZZ ) ) -> ( ( ( M gcd ( ( K x. M ) + N ) ) || M /\ ( M gcd ( ( K x. M ) + N ) ) || ( ( K x. M ) + N ) ) -> ( M gcd ( ( K x. M ) + N ) ) || ( ( -u K x. M ) + ( 1 x. ( ( K x. M ) + N ) ) ) ) )
37 35 10 36 mpanl12 
 |-  ( ( ( M gcd ( ( K x. M ) + N ) ) e. ZZ /\ M e. ZZ /\ ( ( K x. M ) + N ) e. ZZ ) -> ( ( ( M gcd ( ( K x. M ) + N ) ) || M /\ ( M gcd ( ( K x. M ) + N ) ) || ( ( K x. M ) + N ) ) -> ( M gcd ( ( K x. M ) + N ) ) || ( ( -u K x. M ) + ( 1 x. ( ( K x. M ) + N ) ) ) ) )
38 33 2 23 37 mp3an 
 |-  ( ( ( M gcd ( ( K x. M ) + N ) ) || M /\ ( M gcd ( ( K x. M ) + N ) ) || ( ( K x. M ) + N ) ) -> ( M gcd ( ( K x. M ) + N ) ) || ( ( -u K x. M ) + ( 1 x. ( ( K x. M ) + N ) ) ) )
39 29 38 ax-mp 
 |-  ( M gcd ( ( K x. M ) + N ) ) || ( ( -u K x. M ) + ( 1 x. ( ( K x. M ) + N ) ) )
40 zcn 
 |-  ( K e. ZZ -> K e. CC )
41 1 40 ax-mp 
 |-  K e. CC
42 zcn 
 |-  ( M e. ZZ -> M e. CC )
43 2 42 ax-mp 
 |-  M e. CC
44 41 43 mulneg1i 
 |-  ( -u K x. M ) = -u ( K x. M )
45 zcn 
 |-  ( ( ( K x. M ) + N ) e. ZZ -> ( ( K x. M ) + N ) e. CC )
46 23 45 ax-mp 
 |-  ( ( K x. M ) + N ) e. CC
47 46 mulid2i 
 |-  ( 1 x. ( ( K x. M ) + N ) ) = ( ( K x. M ) + N )
48 44 47 oveq12i 
 |-  ( ( -u K x. M ) + ( 1 x. ( ( K x. M ) + N ) ) ) = ( -u ( K x. M ) + ( ( K x. M ) + N ) )
49 41 43 mulcli 
 |-  ( K x. M ) e. CC
50 49 negcli 
 |-  -u ( K x. M ) e. CC
51 49 negidi 
 |-  ( ( K x. M ) + -u ( K x. M ) ) = 0
52 49 50 51 addcomli 
 |-  ( -u ( K x. M ) + ( K x. M ) ) = 0
53 52 oveq1i 
 |-  ( ( -u ( K x. M ) + ( K x. M ) ) + N ) = ( 0 + N )
54 50 49 16 addassi 
 |-  ( ( -u ( K x. M ) + ( K x. M ) ) + N ) = ( -u ( K x. M ) + ( ( K x. M ) + N ) )
55 16 addid2i 
 |-  ( 0 + N ) = N
56 53 54 55 3eqtr3i 
 |-  ( -u ( K x. M ) + ( ( K x. M ) + N ) ) = N
57 48 56 eqtri 
 |-  ( ( -u K x. M ) + ( 1 x. ( ( K x. M ) + N ) ) ) = N
58 39 57 breqtri 
 |-  ( M gcd ( ( K x. M ) + N ) ) || N
59 dvdslegcd 
 |-  ( ( ( ( M gcd ( ( K x. M ) + N ) ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( ( M gcd ( ( K x. M ) + N ) ) || M /\ ( M gcd ( ( K x. M ) + N ) ) || N ) -> ( M gcd ( ( K x. M ) + N ) ) <_ ( M gcd N ) ) )
60 59 ex 
 |-  ( ( ( M gcd ( ( K x. M ) + N ) ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ N = 0 ) -> ( ( ( M gcd ( ( K x. M ) + N ) ) || M /\ ( M gcd ( ( K x. M ) + N ) ) || N ) -> ( M gcd ( ( K x. M ) + N ) ) <_ ( M gcd N ) ) ) )
61 33 2 3 60 mp3an 
 |-  ( -. ( M = 0 /\ N = 0 ) -> ( ( ( M gcd ( ( K x. M ) + N ) ) || M /\ ( M gcd ( ( K x. M ) + N ) ) || N ) -> ( M gcd ( ( K x. M ) + N ) ) <_ ( M gcd N ) ) )
62 30 58 61 mp2ani 
 |-  ( -. ( M = 0 /\ N = 0 ) -> ( M gcd ( ( K x. M ) + N ) ) <_ ( M gcd N ) )
63 27 62 anim12i 
 |-  ( ( -. ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( M gcd N ) <_ ( M gcd ( ( K x. M ) + N ) ) /\ ( M gcd ( ( K x. M ) + N ) ) <_ ( M gcd N ) ) )
64 9 zrei 
 |-  ( M gcd N ) e. RR
65 33 zrei 
 |-  ( M gcd ( ( K x. M ) + N ) ) e. RR
66 64 65 letri3i 
 |-  ( ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) ) <-> ( ( M gcd N ) <_ ( M gcd ( ( K x. M ) + N ) ) /\ ( M gcd ( ( K x. M ) + N ) ) <_ ( M gcd N ) ) )
67 63 66 sylibr 
 |-  ( ( -. ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) ) )
68 pm4.57 
 |-  ( -. ( -. ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) /\ -. ( M = 0 /\ N = 0 ) ) <-> ( ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) \/ ( M = 0 /\ N = 0 ) ) )
69 oveq2 
 |-  ( M = 0 -> ( K x. M ) = ( K x. 0 ) )
70 41 mul01i 
 |-  ( K x. 0 ) = 0
71 69 70 eqtrdi 
 |-  ( M = 0 -> ( K x. M ) = 0 )
72 71 oveq1d 
 |-  ( M = 0 -> ( ( K x. M ) + N ) = ( 0 + N ) )
73 72 55 eqtrdi 
 |-  ( M = 0 -> ( ( K x. M ) + N ) = N )
74 73 eqeq1d 
 |-  ( M = 0 -> ( ( ( K x. M ) + N ) = 0 <-> N = 0 ) )
75 74 pm5.32i 
 |-  ( ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) <-> ( M = 0 /\ N = 0 ) )
76 oveq12 
 |-  ( ( M = 0 /\ N = 0 ) -> ( M gcd N ) = ( 0 gcd 0 ) )
77 oveq12 
 |-  ( ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) -> ( M gcd ( ( K x. M ) + N ) ) = ( 0 gcd 0 ) )
78 75 77 sylbir 
 |-  ( ( M = 0 /\ N = 0 ) -> ( M gcd ( ( K x. M ) + N ) ) = ( 0 gcd 0 ) )
79 76 78 eqtr4d 
 |-  ( ( M = 0 /\ N = 0 ) -> ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) ) )
80 75 79 sylbi 
 |-  ( ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) -> ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) ) )
81 80 79 jaoi 
 |-  ( ( ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) \/ ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) ) )
82 68 81 sylbi 
 |-  ( -. ( -. ( M = 0 /\ ( ( K x. M ) + N ) = 0 ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) ) )
83 67 82 pm2.61i 
 |-  ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) )