absmulgcd

Description: Distribute absolute value of multiplication over gcd. Theorem 1.4(c) in ApostolNT p. 16. (Contributed by Paul Chapman, 22-Jun-2011)

		Ref	Expression
	Assertion	absmulgcd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \cdot M \gcd K \cdot N = \|K (M \gcd N)\|$

Proof

Step	Hyp	Ref	Expression
1		gcdcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℕ_{0}$
2		nn0re	$⊢ M \gcd N \in ℕ_{0} \to M \gcd N \in ℝ$
3		nn0ge0	$⊢ M \gcd N \in ℕ_{0} \to 0 \leq M \gcd N$
4	2 3	absidd	$⊢ M \gcd N \in ℕ_{0} \to \|M \gcd N\| = M \gcd N$
5	1 4	syl	$⊢ (M \in ℤ \land N \in ℤ) \to \|M \gcd N\| = M \gcd N$
6	5	oveq2d	$⊢ (M \in ℤ \land N \in ℤ) \to \|K\| \|M \gcd N\| = \|K\| (M \gcd N)$
7	6	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|K\| \|M \gcd N\| = \|K\| (M \gcd N)$
8		zcn	$⊢ K \in ℤ \to K \in ℂ$
9	1	nn0cnd	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℂ$
10		absmul	$⊢ (K \in ℂ \land M \gcd N \in ℂ) \to \|K (M \gcd N)\| = \|K\| \|M \gcd N\|$
11	8 9 10	syl2an	$⊢ (K \in ℤ \land (M \in ℤ \land N \in ℤ)) \to \|K (M \gcd N)\| = \|K\| \|M \gcd N\|$
12	11	3impb	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|K (M \gcd N)\| = \|K\| \|M \gcd N\|$
13		zcn	$⊢ M \in ℤ \to M \in ℂ$
14		zcn	$⊢ N \in ℤ \to N \in ℂ$
15		absmul	$⊢ (K \in ℂ \land M \in ℂ) \to \|K \cdot M\| = \|K\| \|M\|$
16		absmul	$⊢ (K \in ℂ \land N \in ℂ) \to \|K \cdot N\| = \|K\| \|N\|$
17	15 16	oveqan12d	$⊢ ((K \in ℂ \land M \in ℂ) \land (K \in ℂ \land N \in ℂ)) \to \|K \cdot M\| \gcd \|K \cdot N\| = \|K\| \|M\| \gcd \|K\| \|N\|$
18	17	3impdi	$⊢ (K \in ℂ \land M \in ℂ \land N \in ℂ) \to \|K \cdot M\| \gcd \|K \cdot N\| = \|K\| \|M\| \gcd \|K\| \|N\|$
19	8 13 14 18	syl3an	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|K \cdot M\| \gcd \|K \cdot N\| = \|K\| \|M\| \gcd \|K\| \|N\|$
20		zmulcl	$⊢ (K \in ℤ \land M \in ℤ) \to K \cdot M \in ℤ$
21		zmulcl	$⊢ (K \in ℤ \land N \in ℤ) \to K \cdot N \in ℤ$
22		gcdabs	$⊢ (K \cdot M \in ℤ \land K \cdot N \in ℤ) \to \|K \cdot M\| \gcd \|K \cdot N\| = K \cdot M \gcd K \cdot N$
23	20 21 22	syl2an	$⊢ ((K \in ℤ \land M \in ℤ) \land (K \in ℤ \land N \in ℤ)) \to \|K \cdot M\| \gcd \|K \cdot N\| = K \cdot M \gcd K \cdot N$
24	23	3impdi	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|K \cdot M\| \gcd \|K \cdot N\| = K \cdot M \gcd K \cdot N$
25		nn0abscl	$⊢ K \in ℤ \to \|K\| \in ℕ_{0}$
26		zabscl	$⊢ M \in ℤ \to \|M\| \in ℤ$
27		zabscl	$⊢ N \in ℤ \to \|N\| \in ℤ$
28		mulgcd	$⊢ (\|K\| \in ℕ_{0} \land \|M\| \in ℤ \land \|N\| \in ℤ) \to \|K\| \|M\| \gcd \|K\| \|N\| = \|K\| (\|M\| \gcd \|N\|)$
29	25 26 27 28	syl3an	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|K\| \|M\| \gcd \|K\| \|N\| = \|K\| (\|M\| \gcd \|N\|)$
30	19 24 29	3eqtr3d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \cdot M \gcd K \cdot N = \|K\| (\|M\| \gcd \|N\|)$
31		gcdabs	$⊢ (M \in ℤ \land N \in ℤ) \to \|M\| \gcd \|N\| = M \gcd N$
32	31	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|M\| \gcd \|N\| = M \gcd N$
33	32	oveq2d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \|K\| (\|M\| \gcd \|N\|) = \|K\| (M \gcd N)$
34	30 33	eqtrd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \cdot M \gcd K \cdot N = \|K\| (M \gcd N)$
35	7 12 34	3eqtr4rd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \cdot M \gcd K \cdot N = \|K (M \gcd N)\|$

Metamath Proof Explorer

Theorem absmulgcd

Proof