This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℕ
modxai.2 ⊢ A ∈ ℕ
modxai.3 ⊢ B ∈ ℕ 0
modxai.4 ⊢ D ∈ ℤ
modxai.5 ⊢ K ∈ ℕ 0
modxai.6 ⊢ M ∈ ℕ 0
modxp1i.9 ⊢ A B mod N = K mod N
modxp1i.7 ⊢ B + 1 = E
modxp1i.8 ⊢ D ⋅ N + M = K ⁢ A
Assertion modxp1i ⊢ A E mod N = M mod N

Proof

Step Hyp Ref Expression
1 modxai.1 ⊢ N ∈ ℕ
2 modxai.2 ⊢ A ∈ ℕ
3 modxai.3 ⊢ B ∈ ℕ 0
4 modxai.4 ⊢ D ∈ ℤ
5 modxai.5 ⊢ K ∈ ℕ 0
6 modxai.6 ⊢ M ∈ ℕ 0
7 modxp1i.9 ⊢ A B mod N = K mod N
8 modxp1i.7 ⊢ B + 1 = E
9 modxp1i.8 ⊢ D ⋅ N + M = K ⁢ A
10 1nn0 ⊢ 1 ∈ ℕ 0
11 2 nnnn0i ⊢ A ∈ ℕ 0
12 2 nncni ⊢ A ∈ ℂ
13 exp1 ⊢ A ∈ ℂ → 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