Theorem numexp2x

Description: Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015)

	Ref	Expression
Hypotheses	numexp.1	⊢ 𝐴 ∈ ℕ0
	numexpp1.2	⊢ 𝑀 ∈ ℕ0
	numexp2x.3	⊢ ( 2 · 𝑀 ) = 𝑁
	numexp2x.4	⊢ ( 𝐴 ↑ 𝑀 ) = 𝐷
	numexp2x.5	⊢ ( 𝐷 · 𝐷 ) = 𝐶
Assertion	numexp2x	⊢ ( 𝐴 ↑ 𝑁 ) = 𝐶

Proof

Step	Hyp	Ref	Expression
1		numexp.1	⊢ 𝐴 ∈ ℕ0
2		numexpp1.2	⊢ 𝑀 ∈ ℕ0
3		numexp2x.3	⊢ ( 2 · 𝑀 ) = 𝑁
4		numexp2x.4	⊢ ( 𝐴 ↑ 𝑀 ) = 𝐷
5		numexp2x.5	⊢ ( 𝐷 · 𝐷 ) = 𝐶
6	2	nn0cni	⊢ 𝑀 ∈ ℂ
7	6	2timesi	⊢ ( 2 · 𝑀 ) = ( 𝑀 + 𝑀 )
8	3 7	eqtr3i	⊢ 𝑁 = ( 𝑀 + 𝑀 )
9	8	oveq2i	⊢ ( 𝐴 ↑ 𝑁 ) = ( 𝐴 ↑ ( 𝑀 + 𝑀 ) )
10	1	nn0cni	⊢ 𝐴 ∈ ℂ
11		expadd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑀 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑀 ) ) )
12	10 2 2 11	mp3an	⊢ ( 𝐴 ↑ ( 𝑀 + 𝑀 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑀 ) )
13	9 12	eqtri	⊢ ( 𝐴 ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑀 ) )
14	4 4	oveq12i	⊢ ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑀 ) ) = ( 𝐷 · 𝐷 )
15	14 5	eqtri	⊢ ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑀 ) ) = 𝐶
16	13 15	eqtri	⊢ ( 𝐴 ↑ 𝑁 ) = 𝐶