Proof of Theorem modgcd
Step | Hyp | Ref
| Expression |
1 | | zq 9585 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℚ) |
2 | 1 | adantr 274 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℚ) |
3 | | nnq 9592 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℚ) |
4 | 3 | adantl 275 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℚ) |
5 | | nngt0 8903 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
6 | 5 | adantl 275 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 <
𝑁) |
7 | | modqval 10280 |
. . . . . 6
⊢ ((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 <
𝑁) → (𝑀 mod 𝑁) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) |
8 | 2, 4, 6, 7 | syl3anc 1233 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 mod 𝑁) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) |
9 | | zcn 9217 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
10 | 9 | adantr 274 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℂ) |
11 | | nncn 8886 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
12 | 11 | adantl 275 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
13 | | znq 9583 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℚ) |
14 | 13 | flqcld 10233 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℤ) |
15 | 14 | zcnd 9335 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℂ) |
16 | | mulneg1 8314 |
. . . . . . . . . . 11
⊢
(((⌊‘(𝑀
/ 𝑁)) ∈ ℂ ∧
𝑁 ∈ ℂ) →
(-(⌊‘(𝑀 / 𝑁)) · 𝑁) = -((⌊‘(𝑀 / 𝑁)) · 𝑁)) |
17 | | mulcom 7903 |
. . . . . . . . . . . 12
⊢
(((⌊‘(𝑀
/ 𝑁)) ∈ ℂ ∧
𝑁 ∈ ℂ) →
((⌊‘(𝑀 / 𝑁)) · 𝑁) = (𝑁 · (⌊‘(𝑀 / 𝑁)))) |
18 | 17 | negeqd 8114 |
. . . . . . . . . . 11
⊢
(((⌊‘(𝑀
/ 𝑁)) ∈ ℂ ∧
𝑁 ∈ ℂ) →
-((⌊‘(𝑀 / 𝑁)) · 𝑁) = -(𝑁 · (⌊‘(𝑀 / 𝑁)))) |
19 | 16, 18 | eqtrd 2203 |
. . . . . . . . . 10
⊢
(((⌊‘(𝑀
/ 𝑁)) ∈ ℂ ∧
𝑁 ∈ ℂ) →
(-(⌊‘(𝑀 / 𝑁)) · 𝑁) = -(𝑁 · (⌊‘(𝑀 / 𝑁)))) |
20 | 19 | ancoms 266 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) →
(-(⌊‘(𝑀 / 𝑁)) · 𝑁) = -(𝑁 · (⌊‘(𝑀 / 𝑁)))) |
21 | 20 | 3adant1 1010 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) →
(-(⌊‘(𝑀 / 𝑁)) · 𝑁) = -(𝑁 · (⌊‘(𝑀 / 𝑁)))) |
22 | 21 | oveq2d 5869 |
. . . . . . 7
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) → (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)) = (𝑀 + -(𝑁 · (⌊‘(𝑀 / 𝑁))))) |
23 | | mulcl 7901 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) → (𝑁 · (⌊‘(𝑀 / 𝑁))) ∈ ℂ) |
24 | | negsub 8167 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℂ ∧ (𝑁 · (⌊‘(𝑀 / 𝑁))) ∈ ℂ) → (𝑀 + -(𝑁 · (⌊‘(𝑀 / 𝑁)))) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) |
25 | 23, 24 | sylan2 284 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℂ ∧ (𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ)) →
(𝑀 + -(𝑁 · (⌊‘(𝑀 / 𝑁)))) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) |
26 | 25 | 3impb 1194 |
. . . . . . 7
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) → (𝑀 + -(𝑁 · (⌊‘(𝑀 / 𝑁)))) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) |
27 | 22, 26 | eqtrd 2203 |
. . . . . 6
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧
(⌊‘(𝑀 / 𝑁)) ∈ ℂ) → (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) |
28 | 10, 12, 15, 27 | syl3anc 1233 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)) = (𝑀 − (𝑁 · (⌊‘(𝑀 / 𝑁))))) |
29 | 8, 28 | eqtr4d 2206 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 mod 𝑁) = (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁))) |
30 | 29 | oveq2d 5869 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 gcd (𝑀 mod 𝑁)) = (𝑁 gcd (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)))) |
31 | 14 | znegcld 9336 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
-(⌊‘(𝑀 / 𝑁)) ∈
ℤ) |
32 | | nnz 9231 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
33 | 32 | adantl 275 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) |
34 | | simpl 108 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℤ) |
35 | | gcdaddm 11939 |
. . . 4
⊢
((-(⌊‘(𝑀
/ 𝑁)) ∈ ℤ ∧
𝑁 ∈ ℤ ∧
𝑀 ∈ ℤ) →
(𝑁 gcd 𝑀) = (𝑁 gcd (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)))) |
36 | 31, 33, 34, 35 | syl3anc 1233 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 gcd 𝑀) = (𝑁 gcd (𝑀 + (-(⌊‘(𝑀 / 𝑁)) · 𝑁)))) |
37 | 30, 36 | eqtr4d 2206 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 gcd (𝑀 mod 𝑁)) = (𝑁 gcd 𝑀)) |
38 | | zmodcl 10300 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 mod 𝑁) ∈
ℕ0) |
39 | 38 | nn0zd 9332 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 mod 𝑁) ∈ ℤ) |
40 | | gcdcom 11928 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 mod 𝑁) ∈ ℤ) → (𝑁 gcd (𝑀 mod 𝑁)) = ((𝑀 mod 𝑁) gcd 𝑁)) |
41 | 33, 39, 40 | syl2anc 409 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 gcd (𝑀 mod 𝑁)) = ((𝑀 mod 𝑁) gcd 𝑁)) |
42 | | gcdcom 11928 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁)) |
43 | 33, 34, 42 | syl2anc 409 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁)) |
44 | 37, 41, 43 | 3eqtr3d 2211 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) gcd 𝑁) = (𝑀 gcd 𝑁)) |