This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gcdaddmlem

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

Ref Expression
Hypotheses gcdaddmlem.1 ⊢ 𝐾 ∈ ℤ
gcdaddmlem.2 ⊢ 𝑀 ∈ ℤ
gcdaddmlem.3 ⊢ 𝑁 ∈ ℤ
Assertion gcdaddmlem ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) )

Proof

Step Hyp Ref Expression
1 gcdaddmlem.1 ⊢ 𝐾 ∈ ℤ
2 gcdaddmlem.2 ⊢ 𝑀 ∈ ℤ
3 gcdaddmlem.3 ⊢ 𝑁 ∈ ℤ
4 gcddvds ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
5 2 3 4 mp2an ⊢ ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 )
6 5 simpli ⊢ ( 𝑀 gcd 𝑁 ) ∥ 𝑀
7 gcdcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ0 )
8 2 3 7 mp2an ⊢ ( 𝑀 gcd 𝑁 ) ∈ ℕ0
9 8 nn0zi ⊢ ( 𝑀 gcd 𝑁 ) ∈ ℤ
10 1z ⊢ 1 ∈ ℤ
11 dvds2ln ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) → ( 𝑀 gcd 𝑁 ) ∥ ( ( 𝐾 · 𝑀 ) + ( 1 · 𝑁 ) ) ) )
12 1 10 11 mpanl12 ⊢ ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) → ( 𝑀 gcd 𝑁 ) ∥ ( ( 𝐾 · 𝑀 ) + ( 1 · 𝑁 ) ) ) )
13 9 2 3 12 mp3an ⊢ ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) → ( 𝑀 gcd 𝑁 ) ∥ ( ( 𝐾 · 𝑀 ) + ( 1 · 𝑁 ) ) )
14 5 13 ax-mp ⊢ ( 𝑀 gcd 𝑁 ) ∥ ( ( 𝐾 · 𝑀 ) + ( 1 · 𝑁 ) )
15 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
16 3 15 ax-mp ⊢ 𝑁 ∈ ℂ
17 16 mullidi ⊢ ( 1 · 𝑁 ) = 𝑁
18 17 oveq2i ⊢ ( ( 𝐾 · 𝑀 ) + ( 1 · 𝑁 ) ) = ( ( 𝐾 · 𝑀 ) + 𝑁 )
19 14 18 breqtri ⊢ ( 𝑀 gcd 𝑁 ) ∥ ( ( 𝐾 · 𝑀 ) + 𝑁 )
20 zmulcl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 · 𝑀 ) ∈ ℤ )
21 1 2 20 mp2an ⊢ ( 𝐾 · 𝑀 ) ∈ ℤ
22 zaddcl ⊢ ( ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) + 𝑁 ) ∈ ℤ )
23 21 3 22 mp2an ⊢ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ∈ ℤ
24 dvdslegcd ⊢ ( ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) → ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ) )
25 24 ex ⊢ ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) → ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ) ) )
26 9 2 23 25 mp3an ⊢ ( ¬ ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) → ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ) )
27 6 19 26 mp2ani ⊢ ( ¬ ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) → ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) )
28 gcddvds ⊢ ( ( 𝑀 ∈ ℤ ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ∈ ℤ ) → ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑀 ∧ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) )
29 2 23 28 mp2an ⊢ ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑀 ∧ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ ( ( 𝐾 · 𝑀 ) + 𝑁 ) )
30 29 simpli ⊢ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑀
31 gcdcl ⊢ ( ( 𝑀 ∈ ℤ ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ∈ ℤ ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∈ ℕ0 )
32 2 23 31 mp2an ⊢ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∈ ℕ0
33 32 nn0zi ⊢ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∈ ℤ
34 znegcl ⊢ ( 𝐾 ∈ ℤ → - 𝐾 ∈ ℤ )
35 1 34 ax-mp ⊢ - 𝐾 ∈ ℤ
36 dvds2ln ⊢ ( ( ( - 𝐾 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ∈ ℤ ) ) → ( ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑀 ∧ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ ( ( - 𝐾 · 𝑀 ) + ( 1 · ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ) ) )
37 35 10 36 mpanl12 ⊢ ( ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ∈ ℤ ) → ( ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑀 ∧ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ ( ( - 𝐾 · 𝑀 ) + ( 1 · ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ) ) )
38 33 2 23 37 mp3an ⊢ ( ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑀 ∧ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ ( ( - 𝐾 · 𝑀 ) + ( 1 · ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ) )
39 29 38 ax-mp ⊢ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ ( ( - 𝐾 · 𝑀 ) + ( 1 · ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) )
40 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
41 1 40 ax-mp ⊢ 𝐾 ∈ ℂ
42 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
43 2 42 ax-mp ⊢ 𝑀 ∈ ℂ
44 41 43 mulneg1i ⊢ ( - 𝐾 · 𝑀 ) = - ( 𝐾 · 𝑀 )
45 zcn ⊢ ( ( ( 𝐾 · 𝑀 ) + 𝑁 ) ∈ ℤ → ( ( 𝐾 · 𝑀 ) + 𝑁 ) ∈ ℂ )
46 23 45 ax-mp ⊢ ( ( 𝐾 · 𝑀 ) + 𝑁 ) ∈ ℂ
47 46 mullidi ⊢ ( 1 · ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) = ( ( 𝐾 · 𝑀 ) + 𝑁 )
48 44 47 oveq12i ⊢ ( ( - 𝐾 · 𝑀 ) + ( 1 · ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ) = ( - ( 𝐾 · 𝑀 ) + ( ( 𝐾 · 𝑀 ) + 𝑁 ) )
49 41 43 mulcli ⊢ ( 𝐾 · 𝑀 ) ∈ ℂ
50 49 negcli ⊢ - ( 𝐾 · 𝑀 ) ∈ ℂ
51 49 negidi ⊢ ( ( 𝐾 · 𝑀 ) + - ( 𝐾 · 𝑀 ) ) = 0
52 49 50 51 addcomli ⊢ ( - ( 𝐾 · 𝑀 ) + ( 𝐾 · 𝑀 ) ) = 0
53 52 oveq1i ⊢ ( ( - ( 𝐾 · 𝑀 ) + ( 𝐾 · 𝑀 ) ) + 𝑁 ) = ( 0 + 𝑁 )
54 50 49 16 addassi ⊢ ( ( - ( 𝐾 · 𝑀 ) + ( 𝐾 · 𝑀 ) ) + 𝑁 ) = ( - ( 𝐾 · 𝑀 ) + ( ( 𝐾 · 𝑀 ) + 𝑁 ) )
55 16 addlidi ⊢ ( 0 + 𝑁 ) = 𝑁
56 53 54 55 3eqtr3i ⊢ ( - ( 𝐾 · 𝑀 ) + ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) = 𝑁
57 48 56 eqtri ⊢ ( ( - 𝐾 · 𝑀 ) + ( 1 · ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ) = 𝑁
58 39 57 breqtri ⊢ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑁
59 dvdslegcd ⊢ ( ( ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑀 ∧ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑁 ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ≤ ( 𝑀 gcd 𝑁 ) ) )
60 59 ex ⊢ ( ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑀 ∧ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑁 ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ≤ ( 𝑀 gcd 𝑁 ) ) ) )
61 33 2 3 60 mp3an ⊢ ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑀 ∧ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∥ 𝑁 ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ≤ ( 𝑀 gcd 𝑁 ) ) )
62 30 58 61 mp2ani ⊢ ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ≤ ( 𝑀 gcd 𝑁 ) )
63 27 62 anim12i ⊢ ( ( ¬ ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∧ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ≤ ( 𝑀 gcd 𝑁 ) ) )
64 9 zrei ⊢ ( 𝑀 gcd 𝑁 ) ∈ ℝ
65 33 zrei ⊢ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∈ ℝ
66 64 65 letri3i ⊢ ( ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ↔ ( ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ∧ ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ≤ ( 𝑀 gcd 𝑁 ) ) )
67 63 66 sylibr ⊢ ( ( ¬ ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) )
68 pm4.57 ⊢ ( ¬ ( ¬ ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) ↔ ( ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) ∨ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) )
69 oveq2 ⊢ ( 𝑀 = 0 → ( 𝐾 · 𝑀 ) = ( 𝐾 · 0 ) )
70 41 mul01i ⊢ ( 𝐾 · 0 ) = 0
71 69 70 eqtrdi ⊢ ( 𝑀 = 0 → ( 𝐾 · 𝑀 ) = 0 )
72 71 oveq1d ⊢ ( 𝑀 = 0 → ( ( 𝐾 · 𝑀 ) + 𝑁 ) = ( 0 + 𝑁 ) )
73 72 55 eqtrdi ⊢ ( 𝑀 = 0 → ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 𝑁 )
74 73 eqeq1d ⊢ ( 𝑀 = 0 → ( ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ↔ 𝑁 = 0 ) )
75 74 pm5.32i ⊢ ( ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) ↔ ( 𝑀 = 0 ∧ 𝑁 = 0 ) )
76 oveq12 ⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd 𝑁 ) = ( 0 gcd 0 ) )
77 oveq12 ⊢ ( ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) = ( 0 gcd 0 ) )
78 75 77 sylbir ⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) = ( 0 gcd 0 ) )
79 76 78 eqtr4d ⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) )
80 75 79 sylbi ⊢ ( ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) )
81 80 79 jaoi ⊢ ( ( ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) ∨ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) )
82 68 81 sylbi ⊢ ( ¬ ( ¬ ( 𝑀 = 0 ∧ ( ( 𝐾 · 𝑀 ) + 𝑁 ) = 0 ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) )
83 67 82 pm2.61i ⊢ ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) )