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	$⊢ (M \in ℤ \land N \in ℕ) \to (M \mod N) \gcd N = M \gcd N$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ M \in ℤ \to M \in ℝ$
2		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
3		modval	$⊢ (M \in ℝ \land N \in ℝ^{+}) \to M \mod N = M - N ⌊\frac{M}{N}⌋$
4	1 2 3	syl2an	$⊢ (M \in ℤ \land N \in ℕ) \to M \mod N = M - N ⌊\frac{M}{N}⌋$
5		zcn	$⊢ M \in ℤ \to M \in ℂ$
6	5	adantr	$⊢ (M \in ℤ \land N \in ℕ) \to M \in ℂ$
7		nncn	$⊢ N \in ℕ \to N \in ℂ$
8	7	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to N \in ℂ$
9		nnre	$⊢ N \in ℕ \to N \in ℝ$
10		nnne0	$⊢ N \in ℕ \to N \neq 0$
11		redivcl	$⊢ (M \in ℝ \land N \in ℝ \land N \neq 0) \to \frac{M}{N} \in ℝ$
12	1 9 10 11	syl3an	$⊢ (M \in ℤ \land N \in ℕ \land N \in ℕ) \to \frac{M}{N} \in ℝ$
13	12	3anidm23	$⊢ (M \in ℤ \land N \in ℕ) \to \frac{M}{N} \in ℝ$
14	13	flcld	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊\frac{M}{N}⌋ \in ℤ$
15	14	zcnd	$⊢ (M \in ℤ \land N \in ℕ) \to ⌊\frac{M}{N}⌋ \in ℂ$
16		mulneg1	$⊢ (⌊\frac{M}{N}⌋ \in ℂ \land N \in ℂ) \to (- ⌊\frac{M}{N}⌋) \cdot N = - ⌊\frac{M}{N}⌋ \cdot N$
17		mulcom	$⊢ (⌊\frac{M}{N}⌋ \in ℂ \land N \in ℂ) \to ⌊\frac{M}{N}⌋ \cdot N = N ⌊\frac{M}{N}⌋$
18	17	negeqd	$⊢ (⌊\frac{M}{N}⌋ \in ℂ \land N \in ℂ) \to - ⌊\frac{M}{N}⌋ \cdot N = - N ⌊\frac{M}{N}⌋$
19	16 18	eqtrd	$⊢ (⌊\frac{M}{N}⌋ \in ℂ \land N \in ℂ) \to (- ⌊\frac{M}{N}⌋) \cdot N = - N ⌊\frac{M}{N}⌋$
20	19	ancoms	$⊢ (N \in ℂ \land ⌊\frac{M}{N}⌋ \in ℂ) \to (- ⌊\frac{M}{N}⌋) \cdot N = - N ⌊\frac{M}{N}⌋$
21	20	3adant1	$⊢ (M \in ℂ \land N \in ℂ \land ⌊\frac{M}{N}⌋ \in ℂ) \to (- ⌊\frac{M}{N}⌋) \cdot N = - N ⌊\frac{M}{N}⌋$
22	21	oveq2d	$⊢ (M \in ℂ \land N \in ℂ \land ⌊\frac{M}{N}⌋ \in ℂ) \to M + (- ⌊\frac{M}{N}⌋) \cdot N = M + (- N ⌊\frac{M}{N}⌋)$
23		mulcl	$⊢ (N \in ℂ \land ⌊\frac{M}{N}⌋ \in ℂ) \to N ⌊\frac{M}{N}⌋ \in ℂ$
24		negsub	$⊢ (M \in ℂ \land N ⌊\frac{M}{N}⌋ \in ℂ) \to M + (- N ⌊\frac{M}{N}⌋) = M - N ⌊\frac{M}{N}⌋$
25	23 24	sylan2	$⊢ (M \in ℂ \land (N \in ℂ \land ⌊\frac{M}{N}⌋ \in ℂ)) \to M + (- N ⌊\frac{M}{N}⌋) = M - N ⌊\frac{M}{N}⌋$
26	25	3impb	$⊢ (M \in ℂ \land N \in ℂ \land ⌊\frac{M}{N}⌋ \in ℂ) \to M + (- N ⌊\frac{M}{N}⌋) = M - N ⌊\frac{M}{N}⌋$
27	22 26	eqtrd	$⊢ (M \in ℂ \land N \in ℂ \land ⌊\frac{M}{N}⌋ \in ℂ) \to M + (- ⌊\frac{M}{N}⌋) \cdot N = M - N ⌊\frac{M}{N}⌋$
28	6 8 15 27	syl3anc	$⊢ (M \in ℤ \land N \in ℕ) \to M + (- ⌊\frac{M}{N}⌋) \cdot N = M - N ⌊\frac{M}{N}⌋$
29	4 28	eqtr4d	$⊢ (M \in ℤ \land N \in ℕ) \to M \mod N = M + (- ⌊\frac{M}{N}⌋) \cdot N$
30	29	oveq2d	$⊢ (M \in ℤ \land N \in ℕ) \to N \gcd (M \mod N) = N \gcd (M + (- ⌊\frac{M}{N}⌋) \cdot N)$
31	14	znegcld	$⊢ (M \in ℤ \land N \in ℕ) \to - ⌊\frac{M}{N}⌋ \in ℤ$
32		nnz	$⊢ N \in ℕ \to N \in ℤ$
33	32	adantl	$⊢ (M \in ℤ \land N \in ℕ) \to N \in ℤ$
34		simpl	$⊢ (M \in ℤ \land N \in ℕ) \to M \in ℤ$
35		gcdaddm	$⊢ (- ⌊\frac{M}{N}⌋ \in ℤ \land N \in ℤ \land M \in ℤ) \to N \gcd M = N \gcd (M + (- ⌊\frac{M}{N}⌋) \cdot N)$
36	31 33 34 35	syl3anc	$⊢ (M \in ℤ \land N \in ℕ) \to N \gcd M = N \gcd (M + (- ⌊\frac{M}{N}⌋) \cdot N)$
37	30 36	eqtr4d	$⊢ (M \in ℤ \land N \in ℕ) \to N \gcd (M \mod N) = N \gcd M$
38		zmodcl	$⊢ (M \in ℤ \land N \in ℕ) \to M \mod N \in ℕ_{0}$
39	38	nn0zd	$⊢ (M \in ℤ \land N \in ℕ) \to M \mod N \in ℤ$
40	33 39	gcdcomd	$⊢ (M \in ℤ \land N \in ℕ) \to N \gcd (M \mod N) = (M \mod N) \gcd N$
41	33 34	gcdcomd	$⊢ (M \in ℤ \land N \in ℕ) \to N \gcd M = M \gcd N$
42	37 40 41	3eqtr3d	$⊢ (M \in ℤ \land N \in ℕ) \to (M \mod N) \gcd N = M \gcd N$

Metamath Proof Explorer

Theorem modgcd

Proof