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 ) |
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 ) |