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

Metamath Proof Explorer

Theorem dvds2subd

Description: Deduction form of dvds2sub . (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses dvds2subd.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
dvds2subd.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
dvds2subd.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
dvds2subd.1 ⊢ ( 𝜑 → 𝐾 ∥ 𝑀 )
dvds2subd.2 ⊢ ( 𝜑 → 𝐾 ∥ 𝑁 )
Assertion dvds2subd ( 𝜑 → 𝐾 ∥ ( 𝑀 − 𝑁 ) )

Proof

Step Hyp Ref Expression
1 dvds2subd.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2 dvds2subd.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 dvds2subd.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 dvds2subd.1 ⊢ ( 𝜑 → 𝐾 ∥ 𝑀 )
5 dvds2subd.2 ⊢ ( 𝜑 → 𝐾 ∥ 𝑁 )
6 dvds2sub ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( 𝑀 − 𝑁 ) ) )
7 1 2 3 6 syl3anc ⊢ ( 𝜑 → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( 𝑀 − 𝑁 ) ) )
8 4 5 7 mp2and ⊢ ( 𝜑 → 𝐾 ∥ ( 𝑀 − 𝑁 ) )