Theorem modsubi

Description: Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	modsubi.1	$$⊢N\in \mathbb{N}$$
	modsubi.2	$$⊢A\in \mathbb{N}$$
	modsubi.3	$$⊢B\in {\mathbb{N}}_0$$
	modsubi.4	$$⊢M\in {\mathbb{N}}_0$$
	modsubi.6	$$⊢A\mathrm{mod}N=K\mathrm{mod}N$$
	modsubi.5	$$⊢M+B=K$$
Assertion	modsubi	$$⊢\left(A-B\right)\mathrm{mod}N=M\mathrm{mod}N$$

Proof

Step	Hyp	Ref	Expression
1		modsubi.1	$$⊢N\in \mathbb{N}$$
2		modsubi.2	$$⊢A\in \mathbb{N}$$
3		modsubi.3	$$⊢B\in {\mathbb{N}}_0$$
4		modsubi.4	$$⊢M\in {\mathbb{N}}_0$$
5		modsubi.6	$$⊢A\mathrm{mod}N=K\mathrm{mod}N$$
6		modsubi.5	$$⊢M+B=K$$
7	2	nnrei	$$⊢A\in ℝ$$
8	4 3	nn0addcli	$$⊢M+B\in {\mathbb{N}}_0$$
9	8	nn0rei	$$⊢M+B\in ℝ$$
10	6 9	eqeltrri	$$⊢K\in ℝ$$
11	7 10	pm3.2i	$$⊢\left(A\in ℝ\wedge K\in ℝ\right)$$
12	3	nn0rei	$$⊢B\in ℝ$$
13	12	renegcli	$$⊢-B\in ℝ$$
14		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
15	1 14	ax-mp	$$⊢N\in {ℝ}^{+}$$
16	13 15	pm3.2i	$$⊢\left(-B\in ℝ\wedge N\in {ℝ}^{+}\right)$$
17		modadd1	$$⊢\left(\left(A\in ℝ\wedge K\in ℝ\right)\wedge \left(-B\in ℝ\wedge N\in {ℝ}^{+}\right)\wedge A\mathrm{mod}N=K\mathrm{mod}N\right)\to \left(A+\left(-B\right)\right)\mathrm{mod}N=\left(K+\left(-B\right)\right)\mathrm{mod}N$$
18	11 16 5 17	mp3an	$$⊢\left(A+\left(-B\right)\right)\mathrm{mod}N=\left(K+\left(-B\right)\right)\mathrm{mod}N$$
19	2	nncni	$$⊢A\in ℂ$$
20	3	nn0cni	$$⊢B\in ℂ$$
21	19 20	negsubi	$$⊢A+\left(-B\right)=A-B$$
22	21	oveq1i	$$⊢\left(A+\left(-B\right)\right)\mathrm{mod}N=\left(A-B\right)\mathrm{mod}N$$
23	10	recni	$$⊢K\in ℂ$$
24	23 20	negsubi	$$⊢K+\left(-B\right)=K-B$$
25	4	nn0cni	$$⊢M\in ℂ$$
26	23 20 25	subadd2i	$$⊢K-B=M\leftrightarrow M+B=K$$
27	6 26	mpbir	$$⊢K-B=M$$
28	24 27	eqtri	$$⊢K+\left(-B\right)=M$$
29	28	oveq1i	$$⊢\left(K+\left(-B\right)\right)\mathrm{mod}N=M\mathrm{mod}N$$
30	18 22 29	3eqtr3i	$$⊢\left(A-B\right)\mathrm{mod}N=M\mathrm{mod}N$$