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 e. NN
	modxai.2	|- A e. NN
	modxai.3	|- B e. NN0
	modxai.4	|- D e. ZZ
	modxai.5	|- K e. NN0
	modxai.6	|- M e. NN0
	modxp1i.9	|- ( ( A ^ B ) mod N ) = ( K mod N )
	modxp1i.7	|- ( B + 1 ) = E
	modxp1i.8	|- ( ( D x. N ) + M ) = ( K x. A )
Assertion	modxp1i	|- ( ( A ^ E ) mod N ) = ( M mod N )

Proof

Step	Hyp	Ref	Expression
1		modxai.1	|- N e. NN
2		modxai.2	|- A e. NN
3		modxai.3	|- B e. NN0
4		modxai.4	|- D e. ZZ
5		modxai.5	|- K e. NN0
6		modxai.6	|- M e. NN0
7		modxp1i.9	|- ( ( A ^ B ) mod N ) = ( K mod N )
8		modxp1i.7	|- ( B + 1 ) = E
9		modxp1i.8	|- ( ( D x. N ) + M ) = ( K x. A )
10		1nn0	|- 1 e. NN0
11	2	nnnn0i	|- A e. NN0
12	2	nncni	|- A e. CC
13		exp1	|- ( A e. CC -> ( A ^ 1 ) = A )
14	12 13	ax-mp	|- ( A ^ 1 ) = A
15	14	oveq1i	|- ( ( A ^ 1 ) mod N ) = ( A mod N )
16	1 2 3 4 5 6 10 11 7 15 8 9	modxai	|- ( ( A ^ E ) mod N ) = ( M mod N )