Metamath Proof Explorer


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 )