Theorem mod2xi

Description: Double exponents 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
	mod2xi.9	⊢ ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐾 mod 𝑁 )
	mod2xi.7	⊢ ( 2 · 𝐵 ) = 𝐸
	mod2xi.8	⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝐾 · 𝐾 )
Assertion	mod2xi	⊢ ( ( 𝐴 ↑ 𝐸 ) 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		mod2xi.9	⊢ ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐾 mod 𝑁 )
8		mod2xi.7	⊢ ( 2 · 𝐵 ) = 𝐸
9		mod2xi.8	⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝐾 · 𝐾 )
10	3	nn0cni	⊢ 𝐵 ∈ ℂ
11	10	2timesi	⊢ ( 2 · 𝐵 ) = ( 𝐵 + 𝐵 )
12	11 8	eqtr3i	⊢ ( 𝐵 + 𝐵 ) = 𝐸
13	1 2 3 4 5 6 3 5 7 7 12 9	modxai	⊢ ( ( 𝐴 ↑ 𝐸 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )