modsubmodmod

Description: The difference of a real number modulo a positive real number and another real number modulo this positive 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	modsubmodmod	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to ((A \mod M) - (B \mod M)) \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		modcl	$⊢ (B \in ℝ \land M \in ℝ^{+}) \to B \mod M \in ℝ$
5	4	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to B \mod M \in ℝ$
6		simp2	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to B \in ℝ$
7		simp3	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to M \in ℝ^{+}$
8		modabs2	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A \mod M) \mod M = A \mod M$
9	8	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to (A \mod M) \mod M = A \mod M$
10		modabs2	$⊢ (B \in ℝ \land M \in ℝ^{+}) \to (B \mod M) \mod M = B \mod M$
11	10	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to (B \mod M) \mod M = B \mod M$
12	2 3 5 6 7 9 11	modsub12d	$⊢ (A \in ℝ \land B \in ℝ \land M \in ℝ^{+}) \to ((A \mod M) - (B \mod M)) \mod M = (A - B) \mod M$

Metamath Proof Explorer

Theorem modsubmodmod

Proof