Theorem modnegd

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

	Ref	Expression
Hypotheses	modnegd.1	$$⊢\phi \to A\in ℝ$$
	modnegd.2	$$⊢\phi \to B\in ℝ$$
	modnegd.3	$$⊢\phi \to C\in {ℝ}^{+}$$
	modnegd.4	$$⊢\phi \to A\mathrm{mod}C=B\mathrm{mod}C$$
Assertion	modnegd	$$⊢\phi \to \left(-A\right)\mathrm{mod}C=\left(-B\right)\mathrm{mod}C$$

Proof

Step	Hyp	Ref	Expression
1		modnegd.1	$$⊢\phi \to A\in ℝ$$
2		modnegd.2	$$⊢\phi \to B\in ℝ$$
3		modnegd.3	$$⊢\phi \to C\in {ℝ}^{+}$$
4		modnegd.4	$$⊢\phi \to A\mathrm{mod}C=B\mathrm{mod}C$$
5		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
6	5	znegcld	$$⊢\phi \to -1\in \mathbb{Z}$$
7		modmul1	$$⊢\left(\left(A\in ℝ\wedge B\in ℝ\right)\wedge \left(-1\in \mathbb{Z}\wedge C\in {ℝ}^{+}\right)\wedge A\mathrm{mod}C=B\mathrm{mod}C\right)\to A-1\mathrm{mod}C=B-1\mathrm{mod}C$$
8	1 2 6 3 4 7	syl221anc	$$⊢\phi \to A-1\mathrm{mod}C=B-1\mathrm{mod}C$$
9	1	recnd	$$⊢\phi \to A\in ℂ$$
10		1cnd	$$⊢\phi \to 1\in ℂ$$
11	10	negcld	$$⊢\phi \to -1\in ℂ$$
12	9 11	mulcomd	$$⊢\phi \to A-1=-1A$$
13	9	mulm1d	$$⊢\phi \to -1A=-A$$
14	12 13	eqtrd	$$⊢\phi \to A-1=-A$$
15	14	oveq1d	$$⊢\phi \to A-1\mathrm{mod}C=\left(-A\right)\mathrm{mod}C$$
16	2	recnd	$$⊢\phi \to B\in ℂ$$
17	16 11	mulcomd	$$⊢\phi \to B-1=-1B$$
18	16	mulm1d	$$⊢\phi \to -1B=-B$$
19	17 18	eqtrd	$$⊢\phi \to B-1=-B$$
20	19	oveq1d	$$⊢\phi \to B-1\mathrm{mod}C=\left(-B\right)\mathrm{mod}C$$
21	8 15 20	3eqtr3d	$$⊢\phi \to \left(-A\right)\mathrm{mod}C=\left(-B\right)\mathrm{mod}C$$