Theorem modxai

Description: Add exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014) (Revised by Mario Carneiro, 5-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		modxai.1	$$⊢N\in \mathbb{N}$$
2		modxai.2	$$⊢A\in \mathbb{N}$$
3		modxai.3	$$⊢B\in {\mathbb{N}}_0$$
4		modxai.4	$$⊢D\in \mathbb{Z}$$
5		modxai.5	$$⊢K\in {\mathbb{N}}_0$$
6		modxai.6	$$⊢M\in {\mathbb{N}}_0$$
7		modxai.7	$$⊢C\in {\mathbb{N}}_0$$
8		modxai.8	$$⊢L\in {\mathbb{N}}_0$$
9		modxai.11	$$⊢A^B\mathrm{mod}N=K\mathrm{mod}N$$
10		modxai.12	$$⊢A^C\mathrm{mod}N=L\mathrm{mod}N$$
11		modxai.9	$$⊢B+C=E$$
12		modxai.10	$$⊢D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=KL$$
13	11	oveq2i	$$⊢A^{B+C}=A^E$$
14	2	nncni	$$⊢A\in ℂ$$
15		expadd	$$⊢\left(A\in ℂ\wedge B\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to A^{B+C}=A^B{A}^C$$
16	14 3 7 15	mp3an	$$⊢A^{B+C}=A^B{A}^C$$
17	13 16	eqtr3i	$$⊢A^E=A^B{A}^C$$
18	17	oveq1i	$$⊢A^E\mathrm{mod}N=A^B{A}^C\mathrm{mod}N$$
19		nnexpcl	$$⊢\left(A\in \mathbb{N}\wedge B\in {\mathbb{N}}_0\right)\to A^B\in \mathbb{N}$$
20	2 3 19	mp2an	$$⊢A^B\in \mathbb{N}$$
21	20	nnzi	$$⊢A^B\in \mathbb{Z}$$
22	21	a1i	$$⊢\top \to A^B\in \mathbb{Z}$$
23	5	nn0zi	$$⊢K\in \mathbb{Z}$$
24	23	a1i	$$⊢\top \to K\in \mathbb{Z}$$
25		nnexpcl	$$⊢\left(A\in \mathbb{N}\wedge C\in {\mathbb{N}}_0\right)\to A^C\in \mathbb{N}$$
26	2 7 25	mp2an	$$⊢A^C\in \mathbb{N}$$
27	26	nnzi	$$⊢A^C\in \mathbb{Z}$$
28	27	a1i	$$⊢\top \to A^C\in \mathbb{Z}$$
29	8	nn0zi	$$⊢L\in \mathbb{Z}$$
30	29	a1i	$$⊢\top \to L\in \mathbb{Z}$$
31		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
32	1 31	ax-mp	$$⊢N\in {ℝ}^{+}$$
33	32	a1i	$$⊢\top \to N\in {ℝ}^{+}$$
34	9	a1i	$$⊢\top \to A^B\mathrm{mod}N=K\mathrm{mod}N$$
35	10	a1i	$$⊢\top \to A^C\mathrm{mod}N=L\mathrm{mod}N$$
36	22 24 28 30 33 34 35	modmul12d	$$⊢\top \to A^B{A}^C\mathrm{mod}N=KL\mathrm{mod}N$$
37	36	mptru	$$⊢A^B{A}^C\mathrm{mod}N=KL\mathrm{mod}N$$
38		zcn	$$⊢D\in \mathbb{Z}\to D\in ℂ$$
39	4 38	ax-mp	$$⊢D\in ℂ$$
40	1	nncni	$$⊢N\in ℂ$$
41	39 40	mulcli	$$⊢D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
42	6	nn0cni	$$⊢M\in ℂ$$
43	41 42	addcomi	$$⊢D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=M+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
44	12 43	eqtr3i	$$⊢KL=M+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
45	44	oveq1i	$$⊢KL\mathrm{mod}N=\left(M+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\mathrm{mod}N$$
46	37 45	eqtri	$$⊢A^B{A}^C\mathrm{mod}N=\left(M+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\mathrm{mod}N$$
47	6	nn0rei	$$⊢M\in ℝ$$
48		modcyc	$$⊢\left(M\in ℝ\wedge N\in {ℝ}^{+}\wedge D\in \mathbb{Z}\right)\to \left(M+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\mathrm{mod}N=M\mathrm{mod}N$$
49	47 32 4 48	mp3an	$$⊢\left(M+D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\mathrm{mod}N=M\mathrm{mod}N$$
50	46 49	eqtri	$$⊢A^B{A}^C\mathrm{mod}N=M\mathrm{mod}N$$
51	18 50	eqtri	$$⊢A^E\mathrm{mod}N=M\mathrm{mod}N$$