modsub12d

Description: Subtraction property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016)

Step	Hyp	Ref	Expression
1		modadd12d.1	$⊢ φ \to A \in ℝ$
2		modadd12d.2	$⊢ φ \to B \in ℝ$
3		modadd12d.3	$⊢ φ \to C \in ℝ$
4		modadd12d.4	$⊢ φ \to D \in ℝ$
5		modadd12d.5	$⊢ φ \to E \in ℝ^{+}$
6		modadd12d.6	$⊢ φ \to A \mod E = B \mod E$
7		modadd12d.7	$⊢ φ \to C \mod E = D \mod E$
8	3	renegcld	$⊢ φ \to - C \in ℝ$
9	4	renegcld	$⊢ φ \to - D \in ℝ$
10	3 4 5 7	modnegd	$⊢ φ \to (- C) \mod E = (- D) \mod E$
11	1 2 8 9 5 6 10	modadd12d	$⊢ φ \to (A + (- C)) \mod E = (B + (- D)) \mod E$
12	1	recnd	$⊢ φ \to A \in ℂ$
13	3	recnd	$⊢ φ \to C \in ℂ$
14	12 13	negsubd	$⊢ φ \to A + (- C) = A - C$
15	14	oveq1d	$⊢ φ \to (A + (- C)) \mod E = (A - C) \mod E$
16	2	recnd	$⊢ φ \to B \in ℂ$
17	4	recnd	$⊢ φ \to D \in ℂ$
18	16 17	negsubd	$⊢ φ \to B + (- D) = B - D$
19	18	oveq1d	$⊢ φ \to (B + (- D)) \mod E = (B - D) \mod E$
20	11 15 19	3eqtr3d	$⊢ φ \to (A - C) \mod E = (B - D) \mod E$

Metamath Proof Explorer