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

Metamath Proof Explorer

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 ⊢ ( 𝐴 ↑ 𝑁 ) = 𝐶