Proof of Theorem modgcd
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zre 12617 | . . . . . 6
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) | 
| 2 |  | nnrp 13046 | . . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) | 
| 3 |  | modval 13911 | . . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (𝑀 mod 𝑁) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) | 
| 4 | 1, 2, 3 | syl2an 596 | . . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 mod 𝑁) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) | 
| 5 |  | zcn 12618 | . . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) | 
| 6 | 5 | adantr 480 | . . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℂ) | 
| 7 |  | nncn 12274 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 8 | 7 | adantl 481 | . . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) | 
| 9 |  | nnre 12273 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 10 |  | nnne0 12300 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) | 
| 11 |  | redivcl 11986 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ≠ 0) → (𝑀 / 𝑁) ∈ ℝ) | 
| 12 | 1, 9, 10, 11 | syl3an 1161 | . . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ) | 
| 13 | 12 | 3anidm23 1423 | . . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ) | 
| 14 | 13 | flcld 13838 | . . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℤ) | 
| 15 | 14 | zcnd 12723 | . . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℂ) | 
| 16 |  | mulneg1 11699 | . . . . . . . . . . 11
⊢
(((⌊‘(𝑀
/ 𝑁)) ∈ ℂ ∧
𝑁 ∈ ℂ) →
(-(⌊‘(𝑀 / 𝑁)) · 𝑁) = -((⌊‘(𝑀 / 𝑁)) · 𝑁)) | 
| 17 |  | mulcom 11241 | . . . . . . . . . . . 12
⊢
(((⌊‘(𝑀
/ 𝑁)) ∈ ℂ ∧
𝑁 ∈ ℂ) →
((⌊‘(𝑀 / 𝑁)) · 𝑁) = (𝑁 · (⌊‘(𝑀 / 𝑁)))) | 
| 18 | 17 | negeqd 11502 | . . . . . . . . . . 11
⊢
(((⌊‘(𝑀
/ 𝑁)) ∈ ℂ ∧
𝑁 ∈ ℂ) →
-((⌊‘(𝑀 / 𝑁)) · 𝑁) = -(𝑁 · (⌊‘(𝑀 / 𝑁)))) | 
| 19 | 16, 18 | eqtrd 2777 | . . . . . . . . . 10
⊢
(((⌊‘(𝑀
/ 𝑁)) ∈ ℂ ∧
𝑁 ∈ ℂ) →
(-(⌊‘(𝑀 / 𝑁)) · 𝑁) = -(𝑁 · (⌊‘(𝑀 / 𝑁)))) | 
| 20 | 19 | ancoms 458 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) →
(-(⌊‘(𝑀 / 𝑁)) · 𝑁) = -(𝑁 · (⌊‘(𝑀 / 𝑁)))) | 
| 21 | 20 | 3adant1 1131 | . . . . . . . 8
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) →
(-(⌊‘(𝑀 / 𝑁)) · 𝑁) = -(𝑁 · (⌊‘(𝑀 / 𝑁)))) | 
| 22 | 21 | oveq2d 7447 | . . . . . . 7
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) → (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)) = (𝑀 + -(𝑁 · (⌊‘(𝑀 / 𝑁))))) | 
| 23 |  | mulcl 11239 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) → (𝑁 · (⌊‘(𝑀 / 𝑁))) ∈ ℂ) | 
| 24 |  | negsub 11557 | . . . . . . . . 9
⊢ ((𝑀 ∈ ℂ ∧ (𝑁 · (⌊‘(𝑀 / 𝑁))) ∈ ℂ) → (𝑀 + -(𝑁 · (⌊‘(𝑀 / 𝑁)))) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) | 
| 25 | 23, 24 | sylan2 593 | . . . . . . . 8
⊢ ((𝑀 ∈ ℂ ∧ (𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ)) →
(𝑀 + -(𝑁 · (⌊‘(𝑀 / 𝑁)))) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) | 
| 26 | 25 | 3impb 1115 | . . . . . . 7
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) → (𝑀 + -(𝑁 · (⌊‘(𝑀 / 𝑁)))) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) | 
| 27 | 22, 26 | eqtrd 2777 | . . . . . 6
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) → (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) | 
| 28 | 6, 8, 15, 27 | syl3anc 1373 | . . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) | 
| 29 | 4, 28 | eqtr4d 2780 | . . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 mod 𝑁) = (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁))) | 
| 30 | 29 | oveq2d 7447 | . . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 gcd (𝑀 mod 𝑁)) = (𝑁 gcd (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)))) | 
| 31 | 14 | znegcld 12724 | . . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
-(⌊‘(𝑀 / 𝑁)) ∈
ℤ) | 
| 32 |  | nnz 12634 | . . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) | 
| 33 | 32 | adantl 481 | . . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) | 
| 34 |  | simpl 482 | . . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℤ) | 
| 35 |  | gcdaddm 16562 | . . . 4
⊢
((-(⌊‘(𝑀
/ 𝑁)) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
𝑀 ∈ ℤ) →
(𝑁 gcd 𝑀) = (𝑁 gcd (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)))) | 
| 36 | 31, 33, 34, 35 | syl3anc 1373 | . . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 gcd 𝑀) = (𝑁 gcd (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)))) | 
| 37 | 30, 36 | eqtr4d 2780 | . 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 gcd (𝑀 mod 𝑁)) = (𝑁 gcd 𝑀)) | 
| 38 |  | zmodcl 13931 | . . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 mod 𝑁) ∈
ℕ0) | 
| 39 | 38 | nn0zd 12639 | . . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 mod 𝑁) ∈ ℤ) | 
| 40 | 33, 39 | gcdcomd 16551 | . 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 gcd (𝑀 mod 𝑁)) = ((𝑀 mod 𝑁) gcd 𝑁)) | 
| 41 | 33, 34 | gcdcomd 16551 | . 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁)) | 
| 42 | 37, 40, 41 | 3eqtr3d 2785 | 1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) gcd 𝑁) = (𝑀 gcd 𝑁)) |