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