Theorem mod2xnegi

Description: Version of mod2xi with a negative mod value. (Contributed by Mario Carneiro, 21-Feb-2014)

	Ref	Expression
Hypotheses	mod2xnegi.1	$$⊢A\in \mathbb{N}$$
	mod2xnegi.2	$$⊢B\in {\mathbb{N}}_0$$
	mod2xnegi.3	$$⊢D\in \mathbb{Z}$$
	mod2xnegi.4	$$⊢K\in \mathbb{N}$$
	mod2xnegi.5	$$⊢M\in {\mathbb{N}}_0$$
	mod2xnegi.6	$$⊢L\in {\mathbb{N}}_0$$
	mod2xnegi.10	$$⊢A^B\mathrm{mod}N=L\mathrm{mod}N$$
	mod2xnegi.7	$$⊢2B=E$$
	mod2xnegi.8	$$⊢L+K=N$$
	mod2xnegi.9	$$⊢D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=KK$$
Assertion	mod2xnegi	$$⊢A^E\mathrm{mod}N=M\mathrm{mod}N$$

Proof

Step	Hyp	Ref	Expression
1		mod2xnegi.1	$$⊢A\in \mathbb{N}$$
2		mod2xnegi.2	$$⊢B\in {\mathbb{N}}_0$$
3		mod2xnegi.3	$$⊢D\in \mathbb{Z}$$
4		mod2xnegi.4	$$⊢K\in \mathbb{N}$$
5		mod2xnegi.5	$$⊢M\in {\mathbb{N}}_0$$
6		mod2xnegi.6	$$⊢L\in {\mathbb{N}}_0$$
7		mod2xnegi.10	$$⊢A^B\mathrm{mod}N=L\mathrm{mod}N$$
8		mod2xnegi.7	$$⊢2B=E$$
9		mod2xnegi.8	$$⊢L+K=N$$
10		mod2xnegi.9	$$⊢D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=KK$$
11		nn0nnaddcl	$$⊢\left(L\in {\mathbb{N}}_0\wedge K\in \mathbb{N}\right)\to L+K\in \mathbb{N}$$
12	6 4 11	mp2an	$$⊢L+K\in \mathbb{N}$$
13	9 12	eqeltrri	$$⊢N\in \mathbb{N}$$
14	13	nnzi	$$⊢N\in \mathbb{Z}$$
15		zaddcl	$$⊢\left(N\in \mathbb{Z}\wedge D\in \mathbb{Z}\right)\to N+D\in \mathbb{Z}$$
16	14 3 15	mp2an	$$⊢N+D\in \mathbb{Z}$$
17	4	nnnn0i	$$⊢K\in {\mathbb{N}}_0$$
18	17 17	nn0addcli	$$⊢K+K\in {\mathbb{N}}_0$$
19	18	nn0zi	$$⊢K+K\in \mathbb{Z}$$
20		zsubcl	$$⊢\left(N+D\in \mathbb{Z}\wedge K+K\in \mathbb{Z}\right)\to N+D-\left(K+K\right)\in \mathbb{Z}$$
21	16 19 20	mp2an	$$⊢N+D-\left(K+K\right)\in \mathbb{Z}$$
22	13	nncni	$$⊢N\in ℂ$$
23		zcn	$$⊢D\in \mathbb{Z}\to D\in ℂ$$
24	3 23	ax-mp	$$⊢D\in ℂ$$
25	22 24	addcli	$$⊢N+D\in ℂ$$
26	4	nncni	$$⊢K\in ℂ$$
27	26 26	addcli	$$⊢K+K\in ℂ$$
28	25 27 22	subdiri	$$⊢\left(N+D-\left(K+K\right)\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\left(N+D\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-\left(K+K\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
29	28	oveq1i	$$⊢\left(N+D-\left(K+K\right)\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=\left(N+D\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-\left(K+K\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M$$
30	25 22	mulcli	$$⊢\left(N+D\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
31	5	nn0cni	$$⊢M\in ℂ$$
32	27 22	mulcli	$$⊢\left(K+K\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
33	30 31 32	addsubi	$$⊢\left(N+D\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M-\left(K+K\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\left(N+D\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-\left(K+K\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M$$
34	10	oveq2i	$$⊢\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+KK$$
35	22 26 26	adddii	$$⊢N\left(K+K\right)=NK+NK$$
36	34 35	oveq12i	$$⊢\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M\right)-N\left(K+K\right)=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+KK-\left(NK+NK\right)$$
37	22 24 22	adddiri	$$⊢\left(N+D\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
38	37	oveq1i	$$⊢\left(N+D\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M$$
39	22 22	mulcli	$$⊢\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
40	24 22	mulcli	$$⊢D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
41	39 40 31	addassi	$$⊢\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M$$
42	38 41	eqtr2i	$$⊢\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=\left(N+D\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M$$
43	22 27	mulcomi	$$⊢N\left(K+K\right)=\left(K+K\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
44	42 43	oveq12i	$$⊢\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+\left(D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M\right)-N\left(K+K\right)=\left(N+D\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M-\left(K+K\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
45	36 44	eqtr3i	$$⊢\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+KK-\left(NK+NK\right)=\left(N+D\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M-\left(K+K\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
46		mulsub	$$⊢\left(\left(N\in ℂ\wedge K\in ℂ\right)\wedge \left(N\in ℂ\wedge K\in ℂ\right)\right)\to \left(N-K\right)\left(N-K\right)=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+KK-\left(NK+NK\right)$$
47	22 26 22 26 46	mp4an	$$⊢\left(N-K\right)\left(N-K\right)=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+KK-\left(NK+NK\right)$$
48	6	nn0cni	$$⊢L\in ℂ$$
49	22 26 48	subadd2i	$$⊢N-K=L\leftrightarrow L+K=N$$
50	9 49	mpbir	$$⊢N-K=L$$
51	50 50	oveq12i	$$⊢\left(N-K\right)\left(N-K\right)=LL$$
52	47 51	eqtr3i	$$⊢\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+KK-\left(NK+NK\right)=LL$$
53	45 52	eqtr3i	$$⊢\left(N+D\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M-\left(K+K\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=LL$$
54	29 33 53	3eqtr2i	$$⊢\left(N+D-\left(K+K\right)\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=LL$$
55	13 1 2 21 6 5 7 8 54	mod2xi	$$⊢A^E\mathrm{mod}N=M\mathrm{mod}N$$