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

Metamath Proof Explorer

Theorem modaddmod

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, 13-May-2018)

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

Proof

Step	Hyp	Ref	Expression
1		modcl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \mod M \in ℝ$
2		simpl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \in ℝ$
3	1 2	jca	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A \mod M \in ℝ \land A \in ℝ)$
4	3	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to (A \mod M \in ℝ \land A \in ℝ)$
5		3simpc	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to (B \in ℝ \land M \in ℝ^{+})$
6		modabs2	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A \mod M) \mod M = A \mod M$
7	6	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to (A \mod M) \mod M = A \mod M$
8		modadd1	$⊢ ((A \mod M \in ℝ \land A \in ℝ) \land (B \in ℝ \land M \in ℝ^{+}) \land (A \mod M) \mod M = A \mod M) \to ((A \mod M) + B) \mod M = (A + B) \mod M$
9	4 5 7 8	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to ((A \mod M) + B) \mod M = (A + B) \mod M$