gcdmultiplezOLD

Description: Obsolete proof of gcdmultiplez as of 12-Jan-2024. Extend gcdmultiple so N can be an integer. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	gcdmultiplezOLD	$⊢ (M \in ℕ \land N \in ℤ) \to M \gcd M \cdot N = M$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ N = 0 \to M \cdot N = M \cdot 0$
2	1	oveq2d	$⊢ N = 0 \to M \gcd M \cdot N = M \gcd M \cdot 0$
3	2	eqeq1d	$⊢ N = 0 \to (M \gcd M \cdot N = M \leftrightarrow M \gcd M \cdot 0 = M)$
4		nncn	$⊢ M \in ℕ \to M \in ℂ$
5		zcn	$⊢ N \in ℤ \to N \in ℂ$
6		absmul	$⊢ (M \in ℂ \land N \in ℂ) \to \|M \cdot N\| = \|M\| \|N\|$
7	4 5 6	syl2an	$⊢ (M \in ℕ \land N \in ℤ) \to \|M \cdot N\| = \|M\| \|N\|$
8		nnre	$⊢ M \in ℕ \to M \in ℝ$
9		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
10	9	nn0ge0d	$⊢ M \in ℕ \to 0 \leq M$
11	8 10	absidd	$⊢ M \in ℕ \to \|M\| = M$
12	11	oveq1d	$⊢ M \in ℕ \to \|M\| \|N\| = M \|N\|$
13	12	adantr	$⊢ (M \in ℕ \land N \in ℤ) \to \|M\| \|N\| = M \|N\|$
14	7 13	eqtrd	$⊢ (M \in ℕ \land N \in ℤ) \to \|M \cdot N\| = M \|N\|$
15	14	oveq2d	$⊢ (M \in ℕ \land N \in ℤ) \to M \gcd \|M \cdot N\| = M \gcd M \|N\|$
16	15	adantr	$⊢ ((M \in ℕ \land N \in ℤ) \land N \neq 0) \to M \gcd \|M \cdot N\| = M \gcd M \|N\|$
17		simpll	$⊢ ((M \in ℕ \land N \in ℤ) \land N \neq 0) \to M \in ℕ$
18	17	nnzd	$⊢ ((M \in ℕ \land N \in ℤ) \land N \neq 0) \to M \in ℤ$
19		nnz	$⊢ M \in ℕ \to M \in ℤ$
20		zmulcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
21	19 20	sylan	$⊢ (M \in ℕ \land N \in ℤ) \to M \cdot N \in ℤ$
22	21	adantr	$⊢ ((M \in ℕ \land N \in ℤ) \land N \neq 0) \to M \cdot N \in ℤ$
23		gcdabs2	$⊢ (M \in ℤ \land M \cdot N \in ℤ) \to M \gcd \|M \cdot N\| = M \gcd M \cdot N$
24	18 22 23	syl2anc	$⊢ ((M \in ℕ \land N \in ℤ) \land N \neq 0) \to M \gcd \|M \cdot N\| = M \gcd M \cdot N$
25		nnabscl	$⊢ (N \in ℤ \land N \neq 0) \to \|N\| \in ℕ$
26		gcdmultiple	$⊢ (M \in ℕ \land \|N\| \in ℕ) \to M \gcd M \|N\| = M$
27	25 26	sylan2	$⊢ (M \in ℕ \land (N \in ℤ \land N \neq 0)) \to M \gcd M \|N\| = M$
28	27	anassrs	$⊢ ((M \in ℕ \land N \in ℤ) \land N \neq 0) \to M \gcd M \|N\| = M$
29	16 24 28	3eqtr3d	$⊢ ((M \in ℕ \land N \in ℤ) \land N \neq 0) \to M \gcd M \cdot N = M$
30		mul01	$⊢ M \in ℂ \to M \cdot 0 = 0$
31	30	oveq2d	$⊢ M \in ℂ \to M \gcd M \cdot 0 = M \gcd 0$
32	4 31	syl	$⊢ M \in ℕ \to M \gcd M \cdot 0 = M \gcd 0$
33	32	adantr	$⊢ (M \in ℕ \land N \in ℤ) \to M \gcd M \cdot 0 = M \gcd 0$
34		nn0gcdid0	$⊢ M \in ℕ_{0} \to M \gcd 0 = M$
35	9 34	syl	$⊢ M \in ℕ \to M \gcd 0 = M$
36	35	adantr	$⊢ (M \in ℕ \land N \in ℤ) \to M \gcd 0 = M$
37	33 36	eqtrd	$⊢ (M \in ℕ \land N \in ℤ) \to M \gcd M \cdot 0 = M$
38	3 29 37	pm2.61ne	$⊢ (M \in ℕ \land N \in ℤ) \to M \gcd M \cdot N = M$

Metamath Proof Explorer

Theorem gcdmultiplezOLD

Proof