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	$⊢ (M \in ℕ \land M ∥ N) \to N \mod M = 0$

Step	Hyp	Ref	Expression
1		dvdszrcl	$⊢ M ∥ N \to (M \in ℤ \land N \in ℤ)$
2	1	adantl	$⊢ (M \in ℕ \land M ∥ N) \to (M \in ℤ \land N \in ℤ)$
3		dvdsval3	$⊢ (M \in ℕ \land N \in ℤ) \to (M ∥ N \leftrightarrow N \mod M = 0)$
4	3	biimpd	$⊢ (M \in ℕ \land N \in ℤ) \to (M ∥ N \to N \mod M = 0)$
5	4	expcom	$⊢ N \in ℤ \to (M \in ℕ \to (M ∥ N \to N \mod M = 0))$
6	5	impd	$⊢ N \in ℤ \to ((M \in ℕ \land M ∥ N) \to N \mod M = 0)$
7	6	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \in ℕ \land M ∥ N) \to N \mod M = 0)$
8	2 7	mpcom	$⊢ (M \in ℕ \land M ∥ N) \to N \mod M = 0$

Metamath Proof Explorer