gcdmultipleOLD

Description: Obsolete proof of gcdmultiple as of 12-Jan-2024. The GCD of a multiple of a number is the number itself. (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ k = 1 \to M k = M \cdot 1$
2	1	oveq2d	$⊢ k = 1 \to M \gcd M k = M \gcd M \cdot 1$
3	2	eqeq1d	$⊢ k = 1 \to (M \gcd M k = M \leftrightarrow M \gcd M \cdot 1 = M)$
4	3	imbi2d	$⊢ k = 1 \to ((M \in ℕ \to M \gcd M k = M) \leftrightarrow (M \in ℕ \to M \gcd M \cdot 1 = M))$
5		oveq2	$⊢ k = n \to M k = M n$
6	5	oveq2d	$⊢ k = n \to M \gcd M k = M \gcd M n$
7	6	eqeq1d	$⊢ k = n \to (M \gcd M k = M \leftrightarrow M \gcd M n = M)$
8	7	imbi2d	$⊢ k = n \to ((M \in ℕ \to M \gcd M k = M) \leftrightarrow (M \in ℕ \to M \gcd M n = M))$
9		oveq2	$⊢ k = n + 1 \to M k = M (n + 1)$
10	9	oveq2d	$⊢ k = n + 1 \to M \gcd M k = M \gcd M (n + 1)$
11	10	eqeq1d	$⊢ k = n + 1 \to (M \gcd M k = M \leftrightarrow M \gcd M (n + 1) = M)$
12	11	imbi2d	$⊢ k = n + 1 \to ((M \in ℕ \to M \gcd M k = M) \leftrightarrow (M \in ℕ \to M \gcd M (n + 1) = M))$
13		oveq2	$⊢ k = N \to M k = M \cdot N$
14	13	oveq2d	$⊢ k = N \to M \gcd M k = M \gcd M \cdot N$
15	14	eqeq1d	$⊢ k = N \to (M \gcd M k = M \leftrightarrow M \gcd M \cdot N = M)$
16	15	imbi2d	$⊢ k = N \to ((M \in ℕ \to M \gcd M k = M) \leftrightarrow (M \in ℕ \to M \gcd M \cdot N = M))$
17		nncn	$⊢ M \in ℕ \to M \in ℂ$
18	17	mulid1d	$⊢ M \in ℕ \to M \cdot 1 = M$
19	18	oveq2d	$⊢ M \in ℕ \to M \gcd M \cdot 1 = M \gcd M$
20		nnz	$⊢ M \in ℕ \to M \in ℤ$
21		gcdid	$⊢ M \in ℤ \to M \gcd M = \|M\|$
22	20 21	syl	$⊢ M \in ℕ \to M \gcd M = \|M\|$
23		nnre	$⊢ M \in ℕ \to M \in ℝ$
24		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
25	24	nn0ge0d	$⊢ M \in ℕ \to 0 \leq M$
26	23 25	absidd	$⊢ M \in ℕ \to \|M\| = M$
27	22 26	eqtrd	$⊢ M \in ℕ \to M \gcd M = M$
28	19 27	eqtrd	$⊢ M \in ℕ \to M \gcd M \cdot 1 = M$
29		1z	$⊢ 1 \in ℤ$
30		nnz	$⊢ n \in ℕ \to n \in ℤ$
31		zmulcl	$⊢ (M \in ℤ \land n \in ℤ) \to M n \in ℤ$
32	20 30 31	syl2an	$⊢ (M \in ℕ \land n \in ℕ) \to M n \in ℤ$
33		gcdaddm	$⊢ (1 \in ℤ \land M \in ℤ \land M n \in ℤ) \to M \gcd M n = M \gcd (M n + 1 \cdot M)$
34	29 20 32 33	mp3an2ani	$⊢ (M \in ℕ \land n \in ℕ) \to M \gcd M n = M \gcd (M n + 1 \cdot M)$
35		nncn	$⊢ n \in ℕ \to n \in ℂ$
36		ax-1cn	$⊢ 1 \in ℂ$
37		adddi	$⊢ (M \in ℂ \land n \in ℂ \land 1 \in ℂ) \to M (n + 1) = M n + M \cdot 1$
38	36 37	mp3an3	$⊢ (M \in ℂ \land n \in ℂ) \to M (n + 1) = M n + M \cdot 1$
39		mulcom	$⊢ (M \in ℂ \land 1 \in ℂ) \to M \cdot 1 = 1 \cdot M$
40	36 39	mpan2	$⊢ M \in ℂ \to M \cdot 1 = 1 \cdot M$
41	40	adantr	$⊢ (M \in ℂ \land n \in ℂ) \to M \cdot 1 = 1 \cdot M$
42	41	oveq2d	$⊢ (M \in ℂ \land n \in ℂ) \to M n + M \cdot 1 = M n + 1 \cdot M$
43	38 42	eqtrd	$⊢ (M \in ℂ \land n \in ℂ) \to M (n + 1) = M n + 1 \cdot M$
44	17 35 43	syl2an	$⊢ (M \in ℕ \land n \in ℕ) \to M (n + 1) = M n + 1 \cdot M$
45	44	oveq2d	$⊢ (M \in ℕ \land n \in ℕ) \to M \gcd M (n + 1) = M \gcd (M n + 1 \cdot M)$
46	34 45	eqtr4d	$⊢ (M \in ℕ \land n \in ℕ) \to M \gcd M n = M \gcd M (n + 1)$
47	46	eqeq1d	$⊢ (M \in ℕ \land n \in ℕ) \to (M \gcd M n = M \leftrightarrow M \gcd M (n + 1) = M)$
48	47	biimpd	$⊢ (M \in ℕ \land n \in ℕ) \to (M \gcd M n = M \to M \gcd M (n + 1) = M)$
49	48	expcom	$⊢ n \in ℕ \to (M \in ℕ \to (M \gcd M n = M \to M \gcd M (n + 1) = M))$
50	49	a2d	$⊢ n \in ℕ \to ((M \in ℕ \to M \gcd M n = M) \to (M \in ℕ \to M \gcd M (n + 1) = M))$
51	4 8 12 16 28 50	nnind	$⊢ N \in ℕ \to (M \in ℕ \to M \gcd M \cdot N = M)$
52	51	impcom	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd M \cdot N = M$

Metamath Proof Explorer

Theorem gcdmultipleOLD

Proof