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 ⊢ 𝑁 ∈ ℕ
modxai.2 ⊢ 𝐴 ∈ ℕ
modxai.3 ⊢ 𝐵 ∈ ℕ0
modxai.4 ⊢ 𝐷 ∈ ℤ
modxai.5 ⊢ 𝐾 ∈ ℕ0
modxai.6 ⊢ 𝑀 ∈ ℕ0
modxp1i.9 ⊢ ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐾 mod 𝑁 )
modxp1i.7 ⊢ ( 𝐵 + 1 ) = 𝐸
modxp1i.8 ⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝐾 · 𝐴 )
Assertion modxp1i ( ( 𝐴 ↑ 𝐸 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )

Proof

Step Hyp Ref Expression
1 modxai.1 ⊢ 𝑁 ∈ ℕ
2 modxai.2 ⊢ 𝐴 ∈ ℕ
3 modxai.3 ⊢ 𝐵 ∈ ℕ0
4 modxai.4 ⊢ 𝐷 ∈ ℤ
5 modxai.5 ⊢ 𝐾 ∈ ℕ0
6 modxai.6 ⊢ 𝑀 ∈ ℕ0
7 modxp1i.9 ⊢ ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐾 mod 𝑁 )
8 modxp1i.7 ⊢ ( 𝐵 + 1 ) = 𝐸
9 modxp1i.8 ⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝐾 · 𝐴 )
10 1nn0 ⊢ 1 ∈ ℕ0
11 2 nnnn0i ⊢ 𝐴 ∈ ℕ0
12 2 nncni ⊢ 𝐴 ∈ ℂ
13 exp1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 )
14 12 13 ax-mp ⊢ ( 𝐴 ↑ 1 ) = 𝐴
15 14 oveq1i ⊢ ( ( 𝐴 ↑ 1 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 )
16 1 2 3 4 5 6 10 11 7 15 8 9 modxai ⊢ ( ( 𝐴 ↑ 𝐸 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )