Metamath Proof Explorer

Theorem modeqmodmin

Description: A real number equals the difference of the real number and a positive real number modulo the positive real number. (Contributed by AV, 3-Nov-2018)

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

Proof

Step	Hyp	Ref	Expression
1		modid0	$⊢ M \in ℝ^{+} \to M \mod M = 0$
2	1	adantl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to M \mod M = 0$
3		modge0	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to 0 \leq A \mod M$
4	2 3	eqbrtrd	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to M \mod M \leq A \mod M$
5		simpl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \in ℝ$
6		rpre	$⊢ M \in ℝ^{+} \to M \in ℝ$
7	6	adantl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to M \in ℝ$
8		simpr	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to M \in ℝ^{+}$
9		modsubdir	$⊢ (A \in ℝ \land M \in ℝ \land M \in ℝ^{+}) \to (M \mod M \leq A \mod M \leftrightarrow (A - M) \mod M = (A \mod M) - (M \mod M))$
10	5 7 8 9	syl3anc	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (M \mod M \leq A \mod M \leftrightarrow (A - M) \mod M = (A \mod M) - (M \mod M))$
11	4 10	mpbid	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A - M) \mod M = (A \mod M) - (M \mod M)$
12	2	eqcomd	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to 0 = M \mod M$
13	12	oveq2d	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A \mod M) - 0 = (A \mod M) - (M \mod M)$
14		modcl	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \mod M \in ℝ$
15	14	recnd	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \mod M \in ℂ$
16	15	subid1d	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to (A \mod M) - 0 = A \mod M$
17	11 13 16	3eqtr2rd	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \mod M = (A - M) \mod M$