Theorem mod2xi

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

	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$$
	mod2xi.9	$$⊢A^B\mathrm{mod}N=K\mathrm{mod}N$$
	mod2xi.7	$$⊢2B=E$$
	mod2xi.8	$$⊢D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=KK$$
Assertion	mod2xi	$$⊢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		mod2xi.9	$$⊢A^B\mathrm{mod}N=K\mathrm{mod}N$$
8		mod2xi.7	$$⊢2B=E$$
9		mod2xi.8	$$⊢D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=KK$$
10	3	nn0cni	$$⊢B\in ℂ$$
11	10	2timesi	$$⊢2B=B+B$$
12	11 8	eqtr3i	$$⊢B+B=E$$
13	1 2 3 4 5 6 3 5 7 7 12 9	modxai	$$⊢A^E\mathrm{mod}N=M\mathrm{mod}N$$