Theorem modxp1i

Description: Add one to an exponent 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$$
	modxp1i.9	$$⊢A^B\mathrm{mod}N=K\mathrm{mod}N$$
	modxp1i.7	$$⊢B+1=E$$
	modxp1i.8	$$⊢D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=KA$$
Assertion	modxp1i	$$⊢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		modxp1i.9	$$⊢A^B\mathrm{mod}N=K\mathrm{mod}N$$
8		modxp1i.7	$$⊢B+1=E$$
9		modxp1i.8	$$⊢D\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+M=KA$$
10		1nn0	$$⊢1\in {\mathbb{N}}_0$$
11	2	nnnn0i	$$⊢A\in {\mathbb{N}}_0$$
12	2	nncni	$$⊢A\in ℂ$$
13		exp1	$$⊢A\in ℂ\to A^1=A$$
14	12 13	ax-mp	$$⊢A^1=A$$
15	14	oveq1i	$$⊢A^1\mathrm{mod}N=A\mathrm{mod}N$$
16	1 2 3 4 5 6 10 11 7 15 8 9	modxai	$$⊢A^E\mathrm{mod}N=M\mathrm{mod}N$$