Theorem mod2xi

Description: Double exponents 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
	mod2xi.9	|- ( ( A ^ B ) mod N ) = ( K mod N )
	mod2xi.7	|- ( 2 x. B ) = E
	mod2xi.8	|- ( ( D x. N ) + M ) = ( K x. K )
Assertion	mod2xi	|- ( ( 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		mod2xi.9	|- ( ( A ^ B ) mod N ) = ( K mod N )
8		mod2xi.7	|- ( 2 x. B ) = E
9		mod2xi.8	|- ( ( D x. N ) + M ) = ( K x. K )
10	3	nn0cni	|- B e. CC
11	10	2timesi	|- ( 2 x. B ) = ( 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 ) mod N ) = ( M mod N )