dvds1lem

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

	Ref	Expression
Hypotheses	dvds1lem.1	$⊢ φ \to (J \in ℤ \land K \in ℤ)$
	dvds1lem.2	$⊢ φ \to (M \in ℤ \land N \in ℤ)$
	dvds1lem.3	$⊢ (φ \land x \in ℤ) \to Z \in ℤ$
	dvds1lem.4	$⊢ (φ \land x \in ℤ) \to (x \cdot J = K \to Z \cdot M = N)$
Assertion	dvds1lem	$⊢ φ \to (J ∥ K \to M ∥ N)$

Step	Hyp	Ref	Expression
1		dvds1lem.1	$⊢ φ \to (J \in ℤ \land K \in ℤ)$
2		dvds1lem.2	$⊢ φ \to (M \in ℤ \land N \in ℤ)$
3		dvds1lem.3	$⊢ (φ \land x \in ℤ) \to Z \in ℤ$
4		dvds1lem.4	$⊢ (φ \land x \in ℤ) \to (x \cdot J = K \to Z \cdot M = N)$
5		oveq1	$⊢ z = Z \to z \cdot M = Z \cdot M$
6	5	eqeq1d	$⊢ z = Z \to (z \cdot M = N \leftrightarrow Z \cdot M = N)$
7	6	rspcev	$⊢ (Z \in ℤ \land Z \cdot M = N) \to \exists z \in ℤ z \cdot M = N$
8	3 4 7	syl6an	$⊢ (φ \land x \in ℤ) \to (x \cdot J = K \to \exists z \in ℤ z \cdot M = N)$
9	8	rexlimdva	$⊢ φ \to (\exists x \in ℤ x \cdot J = K \to \exists z \in ℤ z \cdot M = N)$
10		divides	$⊢ (J \in ℤ \land K \in ℤ) \to (J ∥ K \leftrightarrow \exists x \in ℤ x \cdot J = K)$
11	1 10	syl	$⊢ φ \to (J ∥ K \leftrightarrow \exists x \in ℤ x \cdot J = K)$
12		divides	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ N \leftrightarrow \exists z \in ℤ z \cdot M = N)$
13	2 12	syl	$⊢ φ \to (M ∥ N \leftrightarrow \exists z \in ℤ z \cdot M = N)$
14	9 11 13	3imtr4d	$⊢ φ \to (J ∥ K \to M ∥ N)$

Metamath Proof Explorer