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 𝑁 ) )