dvds0lem

Description: A lemma to assist theorems of || with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	dvds0lem	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \cdot M = N) \to M ∥ N$

Step	Hyp	Ref	Expression
1		oveq1	$⊢ x = K \to x \cdot M = K \cdot M$
2	1	eqeq1d	$⊢ x = K \to (x \cdot M = N \leftrightarrow K \cdot M = N)$
3	2	rspcev	$⊢ (K \in ℤ \land K \cdot M = N) \to \exists x \in ℤ x \cdot M = N$
4	3	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land K \cdot M = N)) \to \exists x \in ℤ x \cdot M = N$
5		divides	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ N \leftrightarrow \exists x \in ℤ x \cdot M = N)$
6	5	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land K \cdot M = N)) \to (M ∥ N \leftrightarrow \exists x \in ℤ x \cdot M = N)$
7	4 6	mpbird	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land K \cdot M = N)) \to M ∥ N$
8	7	expr	$⊢ ((M \in ℤ \land N \in ℤ) \land K \in ℤ) \to (K \cdot M = N \to M ∥ N)$
9	8	3impa	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (K \cdot M = N \to M ∥ N)$
10	9	3comr	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \cdot M = N \to M ∥ N)$
11	10	imp	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \cdot M = N) \to M ∥ N$

Metamath Proof Explorer