Theorem modsub12d

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

	Ref	Expression
Hypotheses	modadd12d.1	$$⊢\phi \to A\in ℝ$$
	modadd12d.2	$$⊢\phi \to B\in ℝ$$
	modadd12d.3	$$⊢\phi \to C\in ℝ$$
	modadd12d.4	$$⊢\phi \to D\in ℝ$$
	modadd12d.5	$$⊢\phi \to E\in {ℝ}^{+}$$
	modadd12d.6	$$⊢\phi \to A\mathrm{mod}E=B\mathrm{mod}E$$
	modadd12d.7	$$⊢\phi \to C\mathrm{mod}E=D\mathrm{mod}E$$
Assertion	modsub12d	$$⊢\phi \to \left(A-C\right)\mathrm{mod}E=\left(B-D\right)\mathrm{mod}E$$

Proof

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