Metamath Proof Explorer

Theorem modsubmod

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

		Ref	Expression
	Assertion	modsubmod	$⊢ (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	1	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to A \mod M \in ℝ$
3		simp1	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to A \in ℝ$
4		simp2	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to B \in ℝ$
5		simp3	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to 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		eqidd	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to B \mod M = B \mod M$
9	2 3 4 4 5 7 8	modsub12d	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to ((A \mod M) - B) \mod M = (A - B) \mod M$