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

Metamath Proof Explorer

Theorem dvdsmod0

Description: If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022)

Ref Expression
Assertion dvdsmod0 ( ( 𝑀 ∈ ℕ ∧ 𝑀 ∥ 𝑁 ) → ( 𝑁 mod 𝑀 ) = 0 )

Proof

Step Hyp Ref Expression
1 dvdszrcl ⊢ ( 𝑀 ∥ 𝑁 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
2 1 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑀 ∥ 𝑁 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
3 dvdsval3 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 mod 𝑀 ) = 0 ) )
4 3 biimpd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 → ( 𝑁 mod 𝑀 ) = 0 ) )
5 4 expcom ⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ℕ → ( 𝑀 ∥ 𝑁 → ( 𝑁 mod 𝑀 ) = 0 ) ) )
6 5 impd ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑀 ∈ ℕ ∧ 𝑀 ∥ 𝑁 ) → ( 𝑁 mod 𝑀 ) = 0 ) )
7 6 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∈ ℕ ∧ 𝑀 ∥ 𝑁 ) → ( 𝑁 mod 𝑀 ) = 0 ) )
8 2 7 mpcom ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑀 ∥ 𝑁 ) → ( 𝑁 mod 𝑀 ) = 0 )