Proof of Theorem gcdaddmlem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | gcdaddmlem.2 | . . . . . . 7
⊢ 𝑀 ∈ ℤ | 
| 2 |  | gcdaddmlem.3 | . . . . . . 7
⊢ 𝑁 ∈ ℤ | 
| 3 |  | gcddvds 16540 | . . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) | 
| 4 | 1, 2, 3 | mp2an 692 | . . . . . 6
⊢ ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) | 
| 5 | 4 | simpli 483 | . . . . 5
⊢ (𝑀 gcd 𝑁) ∥ 𝑀 | 
| 6 |  | gcdcl 16543 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈
ℕ0) | 
| 7 | 1, 2, 6 | mp2an 692 | . . . . . . . . 9
⊢ (𝑀 gcd 𝑁) ∈
ℕ0 | 
| 8 | 7 | nn0zi 12642 | . . . . . . . 8
⊢ (𝑀 gcd 𝑁) ∈ ℤ | 
| 9 |  | gcdaddmlem.1 | . . . . . . . . 9
⊢ 𝐾 ∈ ℤ | 
| 10 |  | 1z 12647 | . . . . . . . . 9
⊢ 1 ∈
ℤ | 
| 11 |  | dvds2ln 16326 | . . . . . . . . 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 1463 | . . . . . . 7
⊢ (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁) → (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + (1 · 𝑁))) | 
| 14 | 4, 13 | ax-mp 5 | . . . . . 6
⊢ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + (1 · 𝑁)) | 
| 15 |  | zcn 12618 | . . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) | 
| 16 | 2, 15 | ax-mp 5 | . . . . . . . 8
⊢ 𝑁 ∈ ℂ | 
| 17 | 16 | mullidi 11266 | . . . . . . 7
⊢ (1
· 𝑁) = 𝑁 | 
| 18 | 17 | oveq2i 7442 | . . . . . 6
⊢ ((𝐾 · 𝑀) + (1 · 𝑁)) = ((𝐾 · 𝑀) + 𝑁) | 
| 19 | 14, 18 | breqtri 5168 | . . . . 5
⊢ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁) | 
| 20 |  | zmulcl 12666 | . . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐾 · 𝑀) ∈ ℤ) | 
| 21 | 9, 1, 20 | mp2an 692 | . . . . . . 7
⊢ (𝐾 · 𝑀) ∈ ℤ | 
| 22 |  | zaddcl 12657 | . . . . . . 7
⊢ (((𝐾 · 𝑀) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) | 
| 23 | 21, 2, 22 | mp2an 692 | . . . . . 6
⊢ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ | 
| 24 |  | dvdslegcd 16541 | . . . . . . 7
⊢ ((((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0)) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)))) | 
| 25 | 24 | ex 412 | . . . . . 6
⊢ (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) → (¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))))) | 
| 26 | 8, 1, 23, 25 | mp3an 1463 | . . . . 5
⊢ (¬
(𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)))) | 
| 27 | 5, 19, 26 | mp2ani 698 | . . . 4
⊢ (¬
(𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) | 
| 28 |  | gcddvds 16540 | . . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) → ((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁))) | 
| 29 | 1, 23, 28 | mp2an 692 | . . . . . 6
⊢ ((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁)) | 
| 30 | 29 | simpli 483 | . . . . 5
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 | 
| 31 |  | gcdcl 16543 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ ((𝐾 · 𝑀) + 𝑁) ∈ ℤ) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈
ℕ0) | 
| 32 | 1, 23, 31 | mp2an 692 | . . . . . . . . 9
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈
ℕ0 | 
| 33 | 32 | nn0zi 12642 | . . . . . . . 8
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℤ | 
| 34 |  | znegcl 12652 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → -𝐾 ∈
ℤ) | 
| 35 | 9, 34 | ax-mp 5 | . . . . . . . . 9
⊢ -𝐾 ∈ ℤ | 
| 36 |  | dvds2ln 16326 | . . . . . . . . 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 1463 | . . . . . . 7
⊢ (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((𝐾 · 𝑀) + 𝑁)) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁)))) | 
| 39 | 29, 38 | ax-mp 5 | . . . . . 6
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁))) | 
| 40 |  | zcn 12618 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) | 
| 41 | 9, 40 | ax-mp 5 | . . . . . . . . 9
⊢ 𝐾 ∈ ℂ | 
| 42 |  | zcn 12618 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) | 
| 43 | 1, 42 | ax-mp 5 | . . . . . . . . 9
⊢ 𝑀 ∈ ℂ | 
| 44 | 41, 43 | mulneg1i 11709 | . . . . . . . 8
⊢ (-𝐾 · 𝑀) = -(𝐾 · 𝑀) | 
| 45 |  | zcn 12618 | . . . . . . . . . 10
⊢ (((𝐾 · 𝑀) + 𝑁) ∈ ℤ → ((𝐾 · 𝑀) + 𝑁) ∈ ℂ) | 
| 46 | 23, 45 | ax-mp 5 | . . . . . . . . 9
⊢ ((𝐾 · 𝑀) + 𝑁) ∈ ℂ | 
| 47 | 46 | mullidi 11266 | . . . . . . . 8
⊢ (1
· ((𝐾 · 𝑀) + 𝑁)) = ((𝐾 · 𝑀) + 𝑁) | 
| 48 | 44, 47 | oveq12i 7443 | . . . . . . 7
⊢ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁))) = (-(𝐾 · 𝑀) + ((𝐾 · 𝑀) + 𝑁)) | 
| 49 | 41, 43 | mulcli 11268 | . . . . . . . . . 10
⊢ (𝐾 · 𝑀) ∈ ℂ | 
| 50 | 49 | negcli 11577 | . . . . . . . . . 10
⊢ -(𝐾 · 𝑀) ∈ ℂ | 
| 51 | 49 | negidi 11578 | . . . . . . . . . 10
⊢ ((𝐾 · 𝑀) + -(𝐾 · 𝑀)) = 0 | 
| 52 | 49, 50, 51 | addcomli 11453 | . . . . . . . . 9
⊢ (-(𝐾 · 𝑀) + (𝐾 · 𝑀)) = 0 | 
| 53 | 52 | oveq1i 7441 | . . . . . . . 8
⊢ ((-(𝐾 · 𝑀) + (𝐾 · 𝑀)) + 𝑁) = (0 + 𝑁) | 
| 54 | 50, 49, 16 | addassi 11271 | . . . . . . . 8
⊢ ((-(𝐾 · 𝑀) + (𝐾 · 𝑀)) + 𝑁) = (-(𝐾 · 𝑀) + ((𝐾 · 𝑀) + 𝑁)) | 
| 55 | 16 | addlidi 11449 | . . . . . . . 8
⊢ (0 +
𝑁) = 𝑁 | 
| 56 | 53, 54, 55 | 3eqtr3i 2773 | . . . . . . 7
⊢ (-(𝐾 · 𝑀) + ((𝐾 · 𝑀) + 𝑁)) = 𝑁 | 
| 57 | 48, 56 | eqtri 2765 | . . . . . 6
⊢ ((-𝐾 · 𝑀) + (1 · ((𝐾 · 𝑀) + 𝑁))) = 𝑁 | 
| 58 | 39, 57 | breqtri 5168 | . . . . 5
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁 | 
| 59 |  | dvdslegcd 16541 | . . . . . . 7
⊢ ((((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))) | 
| 60 | 59 | ex 412 | . . . . . 6
⊢ (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∧ 𝑁 = 0) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁)))) | 
| 61 | 33, 1, 2, 60 | mp3an 1463 | . . . . 5
⊢ (¬
(𝑀 = 0 ∧ 𝑁 = 0) → (((𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑀 ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∥ 𝑁) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))) | 
| 62 | 30, 58, 61 | mp2ani 698 | . . . 4
⊢ (¬
(𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁)) | 
| 63 | 27, 62 | anim12i 613 | . . 3
⊢ ((¬
(𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))) | 
| 64 | 8 | zrei 12619 | . . . 4
⊢ (𝑀 gcd 𝑁) ∈ ℝ | 
| 65 | 33 | zrei 12619 | . . . 4
⊢ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∈ ℝ | 
| 66 | 64, 65 | letri3i 11377 | . . 3
⊢ ((𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ↔ ((𝑀 gcd 𝑁) ≤ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ∧ (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) ≤ (𝑀 gcd 𝑁))) | 
| 67 | 63, 66 | sylibr 234 | . 2
⊢ ((¬
(𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) | 
| 68 |  | pm4.57 993 | . . 3
⊢ (¬
(¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) ↔ ((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∨ (𝑀 = 0 ∧ 𝑁 = 0))) | 
| 69 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑀 = 0 → (𝐾 · 𝑀) = (𝐾 · 0)) | 
| 70 | 41 | mul01i 11451 | . . . . . . . . . 10
⊢ (𝐾 · 0) =
0 | 
| 71 | 69, 70 | eqtrdi 2793 | . . . . . . . . 9
⊢ (𝑀 = 0 → (𝐾 · 𝑀) = 0) | 
| 72 | 71 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑀 = 0 → ((𝐾 · 𝑀) + 𝑁) = (0 + 𝑁)) | 
| 73 | 72, 55 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑀 = 0 → ((𝐾 · 𝑀) + 𝑁) = 𝑁) | 
| 74 | 73 | eqeq1d 2739 | . . . . . 6
⊢ (𝑀 = 0 → (((𝐾 · 𝑀) + 𝑁) = 0 ↔ 𝑁 = 0)) | 
| 75 | 74 | pm5.32i 574 | . . . . 5
⊢ ((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ↔ (𝑀 = 0 ∧ 𝑁 = 0)) | 
| 76 |  | oveq12 7440 | . . . . . 6
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd 𝑁) = (0 gcd 0)) | 
| 77 |  | oveq12 7440 | . . . . . . 7
⊢ ((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) = (0 gcd 0)) | 
| 78 | 75, 77 | sylbir 235 | . . . . . 6
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) = (0 gcd 0)) | 
| 79 | 76, 78 | eqtr4d 2780 | . . . . 5
⊢ ((𝑀 = 0 ∧ 𝑁 = 0) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) | 
| 80 | 75, 79 | sylbi 217 | . . . 4
⊢ ((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) | 
| 81 | 80, 79 | jaoi 858 | . . 3
⊢ (((𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∨ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) | 
| 82 | 68, 81 | sylbi 217 | . 2
⊢ (¬
(¬ (𝑀 = 0 ∧ ((𝐾 · 𝑀) + 𝑁) = 0) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))) | 
| 83 | 67, 82 | pm2.61i 182 | 1
⊢ (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) |