rpdvds

Description: If K is relatively prime to N then it is also relatively prime to any divisor M of N . (Contributed by Mario Carneiro, 19-Jun-2015)

		Ref	Expression
	Assertion	rpdvds	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to K \gcd M = 1$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to K \in ℤ$
2		simpl2	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to M \in ℤ$
3		gcddvds	$⊢ (K \in ℤ \land M \in ℤ) \to ((K \gcd M) ∥ K \land (K \gcd M) ∥ M)$
4	1 2 3	syl2anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to ((K \gcd M) ∥ K \land (K \gcd M) ∥ M)$
5	4	simpld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to (K \gcd M) ∥ K$
6		ax-1ne0	$⊢ 1 \neq 0$
7		simprl	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to K \gcd N = 1$
8	7	neeq1d	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to (K \gcd N \neq 0 \leftrightarrow 1 \neq 0)$
9	6 8	mpbiri	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to K \gcd N \neq 0$
10	9	neneqd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to \neg K \gcd N = 0$
11		simprl	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \land (K = 0 \land M = 0)) \to K = 0$
12		simprr	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \land (K = 0 \land M = 0)) \to M = 0$
13		simplrr	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \land (K = 0 \land M = 0)) \to M ∥ N$
14	12 13	eqbrtrrd	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \land (K = 0 \land M = 0)) \to 0 ∥ N$
15		simpll3	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \land (K = 0 \land M = 0)) \to N \in ℤ$
16		0dvds	$⊢ N \in ℤ \to (0 ∥ N \leftrightarrow N = 0)$
17	15 16	syl	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \land (K = 0 \land M = 0)) \to (0 ∥ N \leftrightarrow N = 0)$
18	14 17	mpbid	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \land (K = 0 \land M = 0)) \to N = 0$
19	11 18	jca	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \land (K = 0 \land M = 0)) \to (K = 0 \land N = 0)$
20	19	ex	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to ((K = 0 \land M = 0) \to (K = 0 \land N = 0))$
21		simpl3	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to N \in ℤ$
22		gcdeq0	$⊢ (K \in ℤ \land N \in ℤ) \to (K \gcd N = 0 \leftrightarrow (K = 0 \land N = 0))$
23	1 21 22	syl2anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to (K \gcd N = 0 \leftrightarrow (K = 0 \land N = 0))$
24	20 23	sylibrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to ((K = 0 \land M = 0) \to K \gcd N = 0)$
25	10 24	mtod	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to \neg (K = 0 \land M = 0)$
26		gcdn0cl	$⊢ ((K \in ℤ \land M \in ℤ) \land \neg (K = 0 \land M = 0)) \to K \gcd M \in ℕ$
27	1 2 25 26	syl21anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to K \gcd M \in ℕ$
28	27	nnzd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to K \gcd M \in ℤ$
29	4	simprd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to (K \gcd M) ∥ M$
30		simprr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to M ∥ N$
31	28 2 21 29 30	dvdstrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to (K \gcd M) ∥ N$
32	10 23	mtbid	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to \neg (K = 0 \land N = 0)$
33		dvdslegcd	$⊢ ((K \gcd M \in ℤ \land K \in ℤ \land N \in ℤ) \land \neg (K = 0 \land N = 0)) \to (((K \gcd M) ∥ K \land (K \gcd M) ∥ N) \to K \gcd M \leq K \gcd N)$
34	28 1 21 32 33	syl31anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to (((K \gcd M) ∥ K \land (K \gcd M) ∥ N) \to K \gcd M \leq K \gcd N)$
35	5 31 34	mp2and	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to K \gcd M \leq K \gcd N$
36	35 7	breqtrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to K \gcd M \leq 1$
37		nnle1eq1	$⊢ K \gcd M \in ℕ \to (K \gcd M \leq 1 \leftrightarrow K \gcd M = 1)$
38	27 37	syl	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to (K \gcd M \leq 1 \leftrightarrow K \gcd M = 1)$
39	36 38	mpbid	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \gcd N = 1 \land M ∥ N)) \to K \gcd M = 1$

Metamath Proof Explorer

Theorem rpdvds

Proof