Theorem dvds1lem

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

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

Proof

Step	Hyp	Ref	Expression
1		dvds1lem.1	⊢ ( 𝜑 → ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
2		dvds1lem.2	⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
3		dvds1lem.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝑍 ∈ ℤ )
4		dvds1lem.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝐽 ) = 𝐾 → ( 𝑍 · 𝑀 ) = 𝑁 ) )
5		oveq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 · 𝑀 ) = ( 𝑍 · 𝑀 ) )
6	5	eqeq1d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑧 · 𝑀 ) = 𝑁 ↔ ( 𝑍 · 𝑀 ) = 𝑁 ) )
7	6	rspcev	⊢ ( ( 𝑍 ∈ ℤ ∧ ( 𝑍 · 𝑀 ) = 𝑁 ) → ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑀 ) = 𝑁 )
8	3 4 7	syl6an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝐽 ) = 𝐾 → ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑀 ) = 𝑁 ) )
9	8	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐽 ) = 𝐾 → ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑀 ) = 𝑁 ) )
10		divides	⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 ∥ 𝐾 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐽 ) = 𝐾 ) )
11	1 10	syl	⊢ ( 𝜑 → ( 𝐽 ∥ 𝐾 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐽 ) = 𝐾 ) )
12		divides	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑀 ) = 𝑁 ) )
13	2 12	syl	⊢ ( 𝜑 → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑀 ) = 𝑁 ) )
14	9 11 13	3imtr4d	⊢ ( 𝜑 → ( 𝐽 ∥ 𝐾 → 𝑀 ∥ 𝑁 ) )