Metamath Proof Explorer


Theorem modgcd

Description: The gcd remains unchanged if one operand is replaced with its remainder modulo the other. (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Assertion modgcd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) gcd 𝑁 ) = ( 𝑀 gcd 𝑁 ) )

Proof

Step Hyp Ref Expression
1 zre ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
2 nnrp ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
3 modval ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( 𝑀 mod 𝑁 ) = ( 𝑀 − ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ) )
4 1 2 3 syl2an ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 mod 𝑁 ) = ( 𝑀 − ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ) )
5 zcn ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
6 5 adantr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℂ )
7 nncn ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
8 7 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
9 nnre ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
10 nnne0 ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
11 redivcl ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ≠ 0 ) → ( 𝑀 / 𝑁 ) ∈ ℝ )
12 1 9 10 11 syl3an ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / 𝑁 ) ∈ ℝ )
13 12 3anidm23 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / 𝑁 ) ∈ ℝ )
14 13 flcld ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℤ )
15 14 zcnd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ )
16 mulneg1 ( ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) = - ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) )
17 mulcom ( ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) = ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) )
18 17 negeqd ( ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → - ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) = - ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) )
19 16 18 eqtrd ( ( ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) = - ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) )
20 19 ancoms ( ( 𝑁 ∈ ℂ ∧ ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ ) → ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) = - ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) )
21 20 3adant1 ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ ) → ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) = - ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) )
22 21 oveq2d ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ ) → ( 𝑀 + ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) ) = ( 𝑀 + - ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ) )
23 mulcl ( ( 𝑁 ∈ ℂ ∧ ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ ) → ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ∈ ℂ )
24 negsub ( ( 𝑀 ∈ ℂ ∧ ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ∈ ℂ ) → ( 𝑀 + - ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ) = ( 𝑀 − ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ) )
25 23 24 sylan2 ( ( 𝑀 ∈ ℂ ∧ ( 𝑁 ∈ ℂ ∧ ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ ) ) → ( 𝑀 + - ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ) = ( 𝑀 − ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ) )
26 25 3impb ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ ) → ( 𝑀 + - ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ) = ( 𝑀 − ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ) )
27 22 26 eqtrd ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℂ ) → ( 𝑀 + ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) ) = ( 𝑀 − ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ) )
28 6 8 15 27 syl3anc ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) ) = ( 𝑀 − ( 𝑁 · ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) ) )
29 4 28 eqtr4d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 mod 𝑁 ) = ( 𝑀 + ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) ) )
30 29 oveq2d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 gcd ( 𝑀 mod 𝑁 ) ) = ( 𝑁 gcd ( 𝑀 + ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) ) ) )
31 14 znegcld ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℤ )
32 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
33 32 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
34 simpl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℤ )
35 gcdaddm ( ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 gcd 𝑀 ) = ( 𝑁 gcd ( 𝑀 + ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) ) ) )
36 31 33 34 35 syl3anc ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 gcd 𝑀 ) = ( 𝑁 gcd ( 𝑀 + ( - ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) · 𝑁 ) ) ) )
37 30 36 eqtr4d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 gcd ( 𝑀 mod 𝑁 ) ) = ( 𝑁 gcd 𝑀 ) )
38 zmodcl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 mod 𝑁 ) ∈ ℕ0 )
39 38 nn0zd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 mod 𝑁 ) ∈ ℤ )
40 33 39 gcdcomd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 gcd ( 𝑀 mod 𝑁 ) ) = ( ( 𝑀 mod 𝑁 ) gcd 𝑁 ) )
41 33 34 gcdcomd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
42 37 40 41 3eqtr3d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) gcd 𝑁 ) = ( 𝑀 gcd 𝑁 ) )