addmodidr

Description: The sum of a positive integer and a nonnegative integer less than the positive integer is equal to the nonnegative integer modulo the positive integer. (Contributed by AV, 19-Mar-2021)

		Ref	Expression
	Assertion	addmodidr	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to (A + M) \mod M = A$

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$⊢ A \in ℕ_{0} \to A \in ℂ$
2		nncn	$⊢ M \in ℕ \to M \in ℂ$
3		addcom	$⊢ (A \in ℂ \land M \in ℂ) \to A + M = M + A$
4	1 2 3	syl2an	$⊢ (A \in ℕ_{0} \land M \in ℕ) \to A + M = M + A$
5	4	3adant3	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to A + M = M + A$
6	5	oveq1d	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to (A + M) \mod M = (M + A) \mod M$
7		addmodid	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to (M + A) \mod M = A$
8	6 7	eqtrd	$⊢ (A \in ℕ_{0} \land M \in ℕ \land A < M) \to (A + M) \mod M = A$

Metamath Proof Explorer

Theorem addmodidr

Proof