Metamath Proof Explorer

Theorem gcdaddmlem

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

Ref Expression
Hypotheses gcdaddmlem.1 ⊢ K ∈ ℤ
gcdaddmlem.2 ⊢ M ∈ ℤ
gcdaddmlem.3 ⊢ N ∈ ℤ
Assertion gcdaddmlem ⊢ M gcd N = M gcd K ⋅ M + N

Proof

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