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 gcdcom ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 mod 𝑁 ) ∈ ℤ ) → ( 𝑁 gcd ( 𝑀 mod 𝑁 ) ) = ( ( 𝑀 mod 𝑁 ) gcd 𝑁 ) )
41 33 39 40 syl2anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 gcd ( 𝑀 mod 𝑁 ) ) = ( ( 𝑀 mod 𝑁 ) gcd 𝑁 ) )
42 gcdcom ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
43 33 34 42 syl2anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
44 37 41 43 3eqtr3d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) gcd 𝑁 ) = ( 𝑀 gcd 𝑁 ) )