Theorem dvds2lem

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

	Ref	Expression
Hypotheses	dvds2lem.1	⊢ ( 𝜑 → ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) )
	dvds2lem.2	⊢ ( 𝜑 → ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
	dvds2lem.3	⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
	dvds2lem.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑍 ∈ ℤ )
	dvds2lem.5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑥 · 𝐼 ) = 𝐽 ∧ ( 𝑦 · 𝐾 ) = 𝐿 ) → ( 𝑍 · 𝑀 ) = 𝑁 ) )
Assertion	dvds2lem	⊢ ( 𝜑 → ( ( 𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿 ) → 𝑀 ∥ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		dvds2lem.1	⊢ ( 𝜑 → ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) )
2		dvds2lem.2	⊢ ( 𝜑 → ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
3		dvds2lem.3	⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
4		dvds2lem.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑍 ∈ ℤ )
5		dvds2lem.5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑥 · 𝐼 ) = 𝐽 ∧ ( 𝑦 · 𝐾 ) = 𝐿 ) → ( 𝑍 · 𝑀 ) = 𝑁 ) )
6		divides	⊢ ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐼 ∥ 𝐽 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐼 ) = 𝐽 ) )
7		divides	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐾 ∥ 𝐿 ↔ ∃ 𝑦 ∈ ℤ ( 𝑦 · 𝐾 ) = 𝐿 ) )
8	6 7	bi2anan9	⊢ ( ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿 ) ↔ ( ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐼 ) = 𝐽 ∧ ∃ 𝑦 ∈ ℤ ( 𝑦 · 𝐾 ) = 𝐿 ) ) )
9	1 2 8	syl2anc	⊢ ( 𝜑 → ( ( 𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿 ) ↔ ( ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐼 ) = 𝐽 ∧ ∃ 𝑦 ∈ ℤ ( 𝑦 · 𝐾 ) = 𝐿 ) ) )
10	9	biimpd	⊢ ( 𝜑 → ( ( 𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿 ) → ( ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐼 ) = 𝐽 ∧ ∃ 𝑦 ∈ ℤ ( 𝑦 · 𝐾 ) = 𝐿 ) ) )
11		reeanv	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 · 𝐼 ) = 𝐽 ∧ ( 𝑦 · 𝐾 ) = 𝐿 ) ↔ ( ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐼 ) = 𝐽 ∧ ∃ 𝑦 ∈ ℤ ( 𝑦 · 𝐾 ) = 𝐿 ) )
12	10 11	imbitrrdi	⊢ ( 𝜑 → ( ( 𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 · 𝐼 ) = 𝐽 ∧ ( 𝑦 · 𝐾 ) = 𝐿 ) ) )
13		oveq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 · 𝑀 ) = ( 𝑍 · 𝑀 ) )
14	13	eqeq1d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑧 · 𝑀 ) = 𝑁 ↔ ( 𝑍 · 𝑀 ) = 𝑁 ) )
15	14	rspcev	⊢ ( ( 𝑍 ∈ ℤ ∧ ( 𝑍 · 𝑀 ) = 𝑁 ) → ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑀 ) = 𝑁 )
16	4 5 15	syl6an	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑥 · 𝐼 ) = 𝐽 ∧ ( 𝑦 · 𝐾 ) = 𝐿 ) → ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑀 ) = 𝑁 ) )
17	16	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 · 𝐼 ) = 𝐽 ∧ ( 𝑦 · 𝐾 ) = 𝐿 ) → ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑀 ) = 𝑁 ) )
18	12 17	syld	⊢ ( 𝜑 → ( ( 𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿 ) → ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑀 ) = 𝑁 ) )
19		divides	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑀 ) = 𝑁 ) )
20	3 19	syl	⊢ ( 𝜑 → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑀 ) = 𝑁 ) )
21	18 20	sylibrd	⊢ ( 𝜑 → ( ( 𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿 ) → 𝑀 ∥ 𝑁 ) )