dvds2lem

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

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

Proof

Step	Hyp	Ref	Expression
1		dvds2lem.1	$⊢ φ \to (I \in ℤ \land J \in ℤ)$
2		dvds2lem.2	$⊢ φ \to (K \in ℤ \land L \in ℤ)$
3		dvds2lem.3	$⊢ φ \to (M \in ℤ \land N \in ℤ)$
4		dvds2lem.4	$⊢ (φ \land (x \in ℤ \land y \in ℤ)) \to Z \in ℤ$
5		dvds2lem.5	$⊢ (φ \land (x \in ℤ \land y \in ℤ)) \to ((x \cdot I = J \land y K = L) \to Z \cdot M = N)$
6		divides	$⊢ (I \in ℤ \land J \in ℤ) \to (I ∥ J \leftrightarrow \exists x \in ℤ x \cdot I = J)$
7		divides	$⊢ (K \in ℤ \land L \in ℤ) \to (K ∥ L \leftrightarrow \exists y \in ℤ y K = L)$
8	6 7	bi2anan9	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land L \in ℤ)) \to ((I ∥ J \land K ∥ L) \leftrightarrow (\exists x \in ℤ x \cdot I = J \land \exists y \in ℤ y K = L))$
9	1 2 8	syl2anc	$⊢ φ \to ((I ∥ J \land K ∥ L) \leftrightarrow (\exists x \in ℤ x \cdot I = J \land \exists y \in ℤ y K = L))$
10	9	biimpd	$⊢ φ \to ((I ∥ J \land K ∥ L) \to (\exists x \in ℤ x \cdot I = J \land \exists y \in ℤ y K = L))$
11		reeanv	$⊢ \exists x \in ℤ \exists y \in ℤ (x \cdot I = J \land y K = L) \leftrightarrow (\exists x \in ℤ x \cdot I = J \land \exists y \in ℤ y K = L)$
12	10 11	syl6ibr	$⊢ φ \to ((I ∥ J \land K ∥ L) \to \exists x \in ℤ \exists y \in ℤ (x \cdot I = J \land y K = L))$
13		oveq1	$⊢ z = Z \to z \cdot M = Z \cdot M$
14	13	eqeq1d	$⊢ z = Z \to (z \cdot M = N \leftrightarrow Z \cdot M = N)$
15	14	rspcev	$⊢ (Z \in ℤ \land Z \cdot M = N) \to \exists z \in ℤ z \cdot M = N$
16	4 5 15	syl6an	$⊢ (φ \land (x \in ℤ \land y \in ℤ)) \to ((x \cdot I = J \land y K = L) \to \exists z \in ℤ z \cdot M = N)$
17	16	rexlimdvva	$⊢ φ \to (\exists x \in ℤ \exists y \in ℤ (x \cdot I = J \land y K = L) \to \exists z \in ℤ z \cdot M = N)$
18	12 17	syld	$⊢ φ \to ((I ∥ J \land K ∥ L) \to \exists z \in ℤ z \cdot M = N)$
19		divides	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ N \leftrightarrow \exists z \in ℤ z \cdot M = N)$
20	3 19	syl	$⊢ φ \to (M ∥ N \leftrightarrow \exists z \in ℤ z \cdot M = N)$
21	18 20	sylibrd	$⊢ φ \to ((I ∥ J \land K ∥ L) \to M ∥ N)$

Metamath Proof Explorer

Theorem dvds2lem

Proof