This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvds1lem

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

Ref Expression
Hypotheses dvds1lem.1 ⊢ φ → J ∈ ℤ ∧ K ∈ ℤ
dvds1lem.2 ⊢ φ → M ∈ ℤ ∧ N ∈ ℤ
dvds1lem.3 ⊢ φ ∧ x ∈ ℤ → Z ∈ ℤ
dvds1lem.4 ⊢ φ ∧ x ∈ ℤ → x ⋅ J = K → Z ⋅ M = N
Assertion dvds1lem ⊢ φ → J ∥ K → M ∥ N

Proof

Step Hyp Ref Expression
1 dvds1lem.1 ⊢ φ → J ∈ ℤ ∧ K ∈ ℤ
2 dvds1lem.2 ⊢ φ → M ∈ ℤ ∧ N ∈ ℤ
3 dvds1lem.3 ⊢ φ ∧ x ∈ ℤ → Z ∈ ℤ
4 dvds1lem.4 ⊢ φ ∧ x ∈ ℤ → x ⋅ J = K → Z ⋅ M = N
5 oveq1 ⊢ z = Z → z ⋅ M = Z ⋅ M
6 5 eqeq1d ⊢ z = Z → z ⋅ M = N ↔ Z ⋅ M = N
7 6 rspcev ⊢ Z ∈ ℤ ∧ Z ⋅ M = N → ∃ z ∈ ℤ z ⋅ M = N
8 3 4 7 syl6an ⊢ φ ∧ x ∈ ℤ → x ⋅ J = K → ∃ z ∈ ℤ z ⋅ M = N
9 8 rexlimdva ⊢ φ → ∃ x ∈ ℤ x ⋅ J = K → ∃ z ∈ ℤ z ⋅ M = N
10 divides ⊢ J ∈ ℤ ∧ K ∈ ℤ → J ∥ K ↔ ∃ x ∈ ℤ x ⋅ J = K
11 1 10 syl ⊢ φ → J ∥ K ↔ ∃ x ∈ ℤ x ⋅ J = K
12 divides ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ ∃ z ∈ ℤ z ⋅ M = N
13 2 12 syl ⊢ φ → M ∥ N ↔ ∃ z ∈ ℤ z ⋅ M = N
14 9 11 13 3imtr4d ⊢ φ → J ∥ K → M ∥ N