Proof of Theorem gcdaddmlem
Step | Hyp | Ref
| Expression |
1 | | gcdaddmlem.2 |
. . . . . . 7
⊢ 𝑀 ∈ ℤ |
2 | | gcdaddmlem.3 |
. . . . . . 7
⊢ 𝑁 ∈ ℤ |
3 | | gcddvds 15939 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
4 | 1, 2, 3 | mp2an 692 |
. . . . . 6
⊢ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) |
5 | 4 | simpli 487 |
. . . . 5
⊢ (𝑀 gcd 𝑁) ∥ 𝑀 |
6 | | gcdcl 15942 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈
ℕ0) |
7 | 1, 2, 6 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑀 gcd 𝑁) ∈
ℕ0 |
8 | 7 | nn0zi 12081 |
. . . . . . . 8
⊢ (𝑀 gcd 𝑁) ∈ ℤ |
9 | | gcdaddmlem.1 |
. . . . . . . . 9
⊢ 𝐾 ∈ ℤ |
10 | | 1z 12086 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
11 | | dvds2ln 15727 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℤ ∧ 1 ∈
ℤ) ∧ ((𝑀 gcd
𝑁) ∈ ℤ ∧
𝑀 ∈ ℤ ∧
𝑁 ∈ ℤ)) →
(((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) → (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + (1 · 𝑁)))) |
12 | 9, 10, 11 | mpanl12 702 |
. . . . . . . 8
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) → (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + (1 · 𝑁)))) |
13 | 8, 1, 2, 12 | mp3an 1462 |
. . . . . . 7
⊢ (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) → (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + (1 · 𝑁))) |
14 | 4, 13 | ax-mp 5 |
. . . . . 6
⊢ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + (1 · 𝑁)) |
15 | | zcn 12060 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
16 | 2, 15 | ax-mp 5 |
. . . . . . . 8
⊢ 𝑁 ∈ ℂ |
17 | 16 | mulid2i 10717 |
. . . . . . 7
⊢ (1
· 𝑁) = 𝑁 |
18 | 17 | oveq2i 7175 |
. . . . . 6
⊢ ((𝐾 · 𝑀) + (1 · 𝑁)) = ((𝐾 · 𝑀) + 𝑁) |
19 | 14, 18 | breqtri 5052 |
. . . . 5
⊢ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁) |
20 | | zmulcl 12105 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐾 · 𝑀) ∈ ℤ) |
21 | 9, 1, 20 | mp2an 692 |
. . . . . . 7
⊢ (𝐾 · 𝑀) ∈ ℤ |
22 | | zaddcl 12096 |
. . . . . . 7
⊢ (((𝐾 · 𝑀) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) |
23 | 21, 2, 22 | mp2an 692 |
. . . . . 6
⊢ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ |
24 | | dvdslegcd 15940 |
. . . . . . 7
⊢ ((((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0)) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)))) |
25 | 24 | ex 416 |
. . . . . 6
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) → (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))))) |
26 | 8, 1, 23, 25 | mp3an 1462 |
. . . . 5
⊢ (¬
(𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)))) |
27 | 5, 19, 26 | mp2ani 698 |
. . . 4
⊢ (¬
(𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) |
28 | | gcddvds 15939 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) → ((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁))) |
29 | 1, 23, 28 | mp2an 692 |
. . . . . 6
⊢ ((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁)) |
30 | 29 | simpli 487 |
. . . . 5
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 |
31 | | gcdcl 15942 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈
ℕ0) |
32 | 1, 23, 31 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈
ℕ0 |
33 | 32 | nn0zi 12081 |
. . . . . . . 8
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℤ |
34 | | znegcl 12091 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → -𝐾 ∈
ℤ) |
35 | 9, 34 | ax-mp 5 |
. . . . . . . . 9
⊢ -𝐾 ∈ ℤ |
36 | | dvds2ln 15727 |
. . . . . . . . 9
⊢ (((-𝐾 ∈ ℤ ∧ 1 ∈
ℤ) ∧ ((𝑀 gcd
((𝐾 · 𝑀) + 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ)) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁))))) |
37 | 35, 10, 36 | mpanl12 702 |
. . . . . . . 8
⊢ (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁))))) |
38 | 33, 1, 23, 37 | mp3an 1462 |
. . . . . . 7
⊢ (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁)))) |
39 | 29, 38 | ax-mp 5 |
. . . . . 6
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁))) |
40 | | zcn 12060 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) |
41 | 9, 40 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝐾 ∈ ℂ |
42 | | zcn 12060 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
43 | 1, 42 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝑀 ∈ ℂ |
44 | 41, 43 | mulneg1i 11157 |
. . . . . . . 8
⊢ (-𝐾 · 𝑀) = -(𝐾 · 𝑀) |
45 | | zcn 12060 |
. . . . . . . . . 10
⊢ (((𝐾 · 𝑀) + 𝑁) ∈ ℤ → ((𝐾 · 𝑀) + 𝑁) ∈ ℂ) |
46 | 23, 45 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝐾 · 𝑀) + 𝑁) ∈ ℂ |
47 | 46 | mulid2i 10717 |
. . . . . . . 8
⊢ (1
· ((𝐾 · 𝑀) + 𝑁)) = ((𝐾 · 𝑀) + 𝑁) |
48 | 44, 47 | oveq12i 7176 |
. . . . . . 7
⊢ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁))) = (-(𝐾 · 𝑀) + ((𝐾 · 𝑀) + 𝑁)) |
49 | 41, 43 | mulcli 10719 |
. . . . . . . . . 10
⊢ (𝐾 · 𝑀) ∈ ℂ |
50 | 49 | negcli 11025 |
. . . . . . . . . 10
⊢ -(𝐾 · 𝑀) ∈ ℂ |
51 | 49 | negidi 11026 |
. . . . . . . . . 10
⊢ ((𝐾 · 𝑀) + -(𝐾 · 𝑀)) = 0 |
52 | 49, 50, 51 | addcomli 10903 |
. . . . . . . . 9
⊢ (-(𝐾 · 𝑀) + (𝐾 · 𝑀)) = 0 |
53 | 52 | oveq1i 7174 |
. . . . . . . 8
⊢ ((-(𝐾 · 𝑀) + (𝐾 · 𝑀)) + 𝑁) = (0 + 𝑁) |
54 | 50, 49, 16 | addassi 10722 |
. . . . . . . 8
⊢ ((-(𝐾 · 𝑀) + (𝐾 · 𝑀)) + 𝑁) = (-(𝐾 · 𝑀) + ((𝐾 · 𝑀) + 𝑁)) |
55 | 16 | addid2i 10899 |
. . . . . . . 8
⊢ (0 +
𝑁) = 𝑁 |
56 | 53, 54, 55 | 3eqtr3i 2769 |
. . . . . . 7
⊢ (-(𝐾 · 𝑀) + ((𝐾 · 𝑀) + 𝑁)) = 𝑁 |
57 | 48, 56 | eqtri 2761 |
. . . . . 6
⊢ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁))) = 𝑁 |
58 | 39, 57 | breqtri 5052 |
. . . . 5
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁 |
59 | | dvdslegcd 15940 |
. . . . . . 7
⊢ ((((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))) |
60 | 59 | ex 416 |
. . . . . 6
⊢ (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∧ 𝑁 = 0) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁)))) |
61 | 33, 1, 2, 60 | mp3an 1462 |
. . . . 5
⊢ (¬
(𝑀 = 0 ∧ 𝑁 = 0) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))) |
62 | 30, 58, 61 | mp2ani 698 |
. . . 4
⊢ (¬
(𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁)) |
63 | 27, 62 | anim12i 616 |
. . 3
⊢ ((¬
(𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))) |
64 | 8 | zrei 12061 |
. . . 4
⊢ (𝑀 gcd 𝑁) ∈ ℝ |
65 | 33 | zrei 12061 |
. . . 4
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℝ |
66 | 64, 65 | letri3i 10827 |
. . 3
⊢ ((𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ↔ ((𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))) |
67 | 63, 66 | sylibr 237 |
. 2
⊢ ((¬
(𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) |
68 | | pm4.57 990 |
. . 3
⊢ (¬
(¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ↔ ((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∨ (𝑀 = 0 ∧ 𝑁 = 0))) |
69 | | oveq2 7172 |
. . . . . . . . . 10
⊢ (𝑀 = 0 → (𝐾 · 𝑀) = (𝐾 · 0)) |
70 | 41 | mul01i 10901 |
. . . . . . . . . 10
⊢ (𝐾 · 0) =
0 |
71 | 69, 70 | eqtrdi 2789 |
. . . . . . . . 9
⊢ (𝑀 = 0 → (𝐾 · 𝑀) = 0) |
72 | 71 | oveq1d 7179 |
. . . . . . . 8
⊢ (𝑀 = 0 → ((𝐾 · 𝑀) + 𝑁) = (0 + 𝑁)) |
73 | 72, 55 | eqtrdi 2789 |
. . . . . . 7
⊢ (𝑀 = 0 → ((𝐾 · 𝑀) + 𝑁) = 𝑁) |
74 | 73 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑀 = 0 → (((𝐾 · 𝑀) + 𝑁) = 0 ↔ 𝑁 = 0)) |
75 | 74 | pm5.32i 578 |
. . . . 5
⊢ ((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ↔ (𝑀 = 0 ∧ 𝑁 = 0)) |
76 | | oveq12 7173 |
. . . . . 6
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd 𝑁) = (0 gcd 0)) |
77 | | oveq12 7173 |
. . . . . . 7
⊢ ((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) = (0 gcd 0)) |
78 | 75, 77 | sylbir 238 |
. . . . . 6
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) = (0 gcd 0)) |
79 | 76, 78 | eqtr4d 2776 |
. . . . 5
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) |
80 | 75, 79 | sylbi 220 |
. . . 4
⊢ ((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) |
81 | 80, 79 | jaoi 856 |
. . 3
⊢ (((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∨ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) |
82 | 68, 81 | sylbi 220 |
. 2
⊢ (¬
(¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) |
83 | 67, 82 | pm2.61i 185 |
1
⊢ (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) |