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 ⊢MgcdN=MgcdK⋅ M+N

Proof

Step Hyp Ref Expression
1 gcdaddmlem.1 ⊢K∈ℤ
2 gcdaddmlem.2 ⊢M∈ℤ
3 gcdaddmlem.3 ⊢N∈ℤ
4 gcddvds ⊢M∈ℤ∧N∈ℤ→MgcdN∥M∧MgcdN∥N
5 2 3 4 mp2an ⊢MgcdN∥M∧MgcdN∥N
6 5 simpli ⊢MgcdN∥M
7 gcdcl ⊢M∈ℤ∧N∈ℤ→MgcdN∈ℕ0
8 2 3 7 mp2an ⊢MgcdN∈ℕ0
9 8 nn0zi ⊢MgcdN∈ℤ
10 1z ⊢1∈ℤ
11 dvds2ln ⊢K∈ℤ∧1∈ℤ∧MgcdN∈ℤ∧M∈ℤ∧N∈ℤ→MgcdN∥M∧MgcdN∥N→MgcdN∥K⋅ M+1⋅ N
12 1 10 11 mpanl12 ⊢MgcdN∈ℤ∧M∈ℤ∧N∈ℤ→MgcdN∥M∧MgcdN∥N→MgcdN∥K⋅ M+1⋅ N
13 9 2 3 12 mp3an ⊢MgcdN∥M∧MgcdN∥N→MgcdN∥K⋅ M+1⋅ N
14 5 13 ax-mp ⊢MgcdN∥K⋅ M+1⋅ N
15 zcn ⊢N∈ℤ→N∈ℂ
16 3 15 ax-mp ⊢N∈ℂ
17 16 mullidi ⊢1⋅ N=N
18 17 oveq2i ⊢K⋅ M+1⋅ N=K⋅ M+N
19 14 18 breqtri ⊢MgcdN∥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 ⊢MgcdN∈ℤ∧M∈ℤ∧K⋅ M+N∈ℤ∧¬M=0∧K⋅ M+N=0→MgcdN∥M∧MgcdN∥K⋅ M+N→MgcdN≤MgcdK⋅ M+N
25 24 ex ⊢MgcdN∈ℤ∧M∈ℤ∧K⋅ M+N∈ℤ→¬M=0∧K⋅ M+N=0→MgcdN∥M∧MgcdN∥K⋅ M+N→MgcdN≤MgcdK⋅ M+N
26 9 2 23 25 mp3an ⊢¬M=0∧K⋅ M+N=0→MgcdN∥M∧MgcdN∥K⋅ M+N→MgcdN≤MgcdK⋅ M+N
27 6 19 26 mp2ani ⊢¬M=0∧K⋅ M+N=0→MgcdN≤MgcdK⋅ M+N
28 gcddvds ⊢M∈ℤ∧K⋅ M+N∈ℤ→MgcdK⋅ M+N∥M∧MgcdK⋅ M+N∥K⋅ M+N
29 2 23 28 mp2an ⊢MgcdK⋅ M+N∥M∧MgcdK⋅ M+N∥K⋅ M+N
30 29 simpli ⊢MgcdK⋅ M+N∥M
31 gcdcl ⊢M∈ℤ∧K⋅ M+N∈ℤ→MgcdK⋅ M+N∈ℕ0
32 2 23 31 mp2an ⊢MgcdK⋅ M+N∈ℕ0
33 32 nn0zi ⊢MgcdK⋅ M+N∈ℤ
34 znegcl ⊢K∈ℤ→−K∈ℤ
35 1 34 ax-mp ⊢−K∈ℤ
36 dvds2ln ⊢−K∈ℤ∧1∈ℤ∧MgcdK⋅ M+N∈ℤ∧M∈ℤ∧K⋅ M+N∈ℤ→MgcdK⋅ M+N∥M∧MgcdK⋅ M+N∥K⋅ M+N→MgcdK⋅ M+N∥−K⋅ M+1⁢K⋅ M+N
37 35 10 36 mpanl12 ⊢MgcdK⋅ M+N∈ℤ∧M∈ℤ∧K⋅ M+N∈ℤ→MgcdK⋅ M+N∥M∧MgcdK⋅ M+N∥K⋅ M+N→MgcdK⋅ M+N∥−K⋅ M+1⁢K⋅ M+N
38 33 2 23 37 mp3an ⊢MgcdK⋅ M+N∥M∧MgcdK⋅ M+N∥K⋅ M+N→MgcdK⋅ M+N∥−K⋅ M+1⁢K⋅ M+N
39 29 38 ax-mp ⊢MgcdK⋅ 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 mullidi ⊢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 addlidi ⊢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 ⊢MgcdK⋅ M+N∥N
59 dvdslegcd ⊢MgcdK⋅ M+N∈ℤ∧M∈ℤ∧N∈ℤ∧¬M=0∧N=0→MgcdK⋅ M+N∥M∧MgcdK⋅ M+N∥N→MgcdK⋅ M+N≤MgcdN
60 59 ex ⊢MgcdK⋅ M+N∈ℤ∧M∈ℤ∧N∈ℤ→¬M=0∧N=0→MgcdK⋅ M+N∥M∧MgcdK⋅ M+N∥N→MgcdK⋅ M+N≤MgcdN
61 33 2 3 60 mp3an ⊢¬M=0∧N=0→MgcdK⋅ M+N∥M∧MgcdK⋅ M+N∥N→MgcdK⋅ M+N≤MgcdN
62 30 58 61 mp2ani ⊢¬M=0∧N=0→MgcdK⋅ M+N≤MgcdN
63 27 62 anim12i ⊢¬M=0∧K⋅ M+N=0∧¬M=0∧N=0→MgcdN≤MgcdK⋅ M+N∧MgcdK⋅ M+N≤MgcdN
64 9 zrei ⊢MgcdN∈ℝ
65 33 zrei ⊢MgcdK⋅ M+N∈ℝ
66 64 65 letri3i ⊢MgcdN=MgcdK⋅ M+N↔MgcdN≤MgcdK⋅ M+N∧MgcdK⋅ M+N≤MgcdN
67 63 66 sylibr ⊢¬M=0∧K⋅ M+N=0∧¬M=0∧N=0→MgcdN=MgcdK⋅ 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 eqtrdi ⊢M=0→K⋅ M=0
72 71 oveq1d ⊢M=0→K⋅ M+N=0+N
73 72 55 eqtrdi ⊢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→MgcdN=0gcd0
77 oveq12 ⊢M=0∧K⋅ M+N=0→MgcdK⋅ M+N=0gcd0
78 75 77 sylbir ⊢M=0∧N=0→MgcdK⋅ M+N=0gcd0
79 76 78 eqtr4d ⊢M=0∧N=0→MgcdN=MgcdK⋅ M+N
80 75 79 sylbi ⊢M=0∧K⋅ M+N=0→MgcdN=MgcdK⋅ M+N
81 80 79 jaoi ⊢M=0∧K⋅ M+N=0∨M=0∧N=0→MgcdN=MgcdK⋅ M+N
82 68 81 sylbi ⊢¬¬M=0∧K⋅ M+N=0∧¬M=0∧N=0→MgcdN=MgcdK⋅ M+N
83 67 82 pm2.61i ⊢MgcdN=MgcdK⋅ M+N