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

Metamath Proof Explorer

Theorem dvds0lem

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

Ref Expression
Assertion dvds0lem ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ K ⋅ M = N → M ∥ N

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ x = K → x ⋅ M = K ⋅ M
2 1 eqeq1d ⊢ x = K → x ⋅ M = N ↔ K ⋅ M = N
3 2 rspcev ⊢ K ∈ ℤ ∧ K ⋅ M = N → ∃ x ∈ ℤ x ⋅ M = N
4 3 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ K ⋅ M = N → ∃ x ∈ ℤ x ⋅ M = N
5 divides ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ ∃ x ∈ ℤ x ⋅ M = N
6 5 adantr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ K ⋅ M = N → M ∥ N ↔ ∃ x ∈ ℤ x ⋅ M = N
7 4 6 mpbird ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ K ⋅ M = N → M ∥ N
8 7 expr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → K ⋅ M = N → M ∥ N
9 8 3impa ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → K ⋅ M = N → M ∥ N
10 9 3comr ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ⋅ M = N → M ∥ N
11 10 imp ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ K ⋅ M = N → M ∥ N