Metamath Proof Explorer

Theorem modadd2mod

Description: The sum of a real number modulo a positive real number and another real number equals the sum of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018)

		Ref	Expression
	Assertion	modadd2mod	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to (B + (A \mod M)) \mod M = (B + A) \mod M$

Proof

Step	Hyp	Ref	Expression
1		recn	$⊢ B \in ℝ \to B \in ℂ$
2	1	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to B \in ℂ$
3		modcl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \mod M \in ℝ$
4	3	recnd	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \mod M \in ℂ$
5	4	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to A \mod M \in ℂ$
6	2 5	addcomd	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to B + (A \mod M) = (A \mod M) + B$
7	6	oveq1d	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to (B + (A \mod M)) \mod M = ((A \mod M) + B) \mod M$
8		modaddmod	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to ((A \mod M) + B) \mod M = (A + B) \mod M$
9		recn	$⊢ A \in ℝ \to A \in ℂ$
10		addcom	$⊢ (A \in ℂ \land B \in ℂ) \to A + B = B + A$
11	9 1 10	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to A + B = B + A$
12	11	oveq1d	$⊢ (A \in ℝ \land B \in ℝ) \to (A + B) \mod M = (B + A) \mod M$
13	12	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to (A + B) \mod M = (B + A) \mod M$
14	7 8 13	3eqtrd	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to (B + (A \mod M)) \mod M = (B + A) \mod M$