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 )