Metamath Proof Explorer

Theorem dvdsgcdb

Description: Biconditional form of dvdsgcd . (Contributed by Scott Fenton, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	dvdsgcdb	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \land K ∥ N) \leftrightarrow K ∥ (M \gcd N))$

Proof

Step	Hyp	Ref	Expression
1		dvdsgcd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \land K ∥ N) \to K ∥ (M \gcd N))$
2		gcddvds	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
3	2	simpld	$⊢ (M \in ℤ \land N \in ℤ) \to (M \gcd N) ∥ M$
4	3	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (M \gcd N) ∥ M$
5		simp1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \in ℤ$
6		gcdcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℕ_{0}$
7	6	nn0zd	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℤ$
8	7	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \gcd N \in ℤ$
9		simp2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \in ℤ$
10		dvdstr	$⊢ (K \in ℤ \land M \gcd N \in ℤ \land M \in ℤ) \to ((K ∥ (M \gcd N) \land (M \gcd N) ∥ M) \to K ∥ M)$
11	5 8 9 10	syl3anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ (M \gcd N) \land (M \gcd N) ∥ M) \to K ∥ M)$
12	4 11	mpan2d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K ∥ (M \gcd N) \to K ∥ M)$
13	2	simprd	$⊢ (M \in ℤ \land N \in ℤ) \to (M \gcd N) ∥ N$
14	13	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (M \gcd N) ∥ N$
15		dvdstr	$⊢ (K \in ℤ \land M \gcd N \in ℤ \land N \in ℤ) \to ((K ∥ (M \gcd N) \land (M \gcd N) ∥ N) \to K ∥ N)$
16	8 15	syld3an2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ (M \gcd N) \land (M \gcd N) ∥ N) \to K ∥ N)$
17	14 16	mpan2d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K ∥ (M \gcd N) \to K ∥ N)$
18	12 17	jcad	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K ∥ (M \gcd N) \to (K ∥ M \land K ∥ N))$
19	1 18	impbid	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \land K ∥ N) \leftrightarrow K ∥ (M \gcd N))$