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 ⊢ A ∈ ℕ 0
numexpp1.2 ⊢ M ∈ ℕ 0
numexp2x.3 ⊢ 2 ⋅ M = N
numexp2x.4 ⊢ A M = D
numexp2x.5 ⊢ D ⁢ D = C
Assertion numexp2x ⊢ A N = C

Proof

Step Hyp Ref Expression
1 numexp.1 ⊢ A ∈ ℕ 0
2 numexpp1.2 ⊢ M ∈ ℕ 0
3 numexp2x.3 ⊢ 2 ⋅ M = N
4 numexp2x.4 ⊢ A M = D
5 numexp2x.5 ⊢ D ⁢ D = C
6 2 nn0cni ⊢ M ∈ ℂ
7 6 2timesi ⊢ 2 ⋅ M = M + M
8 3 7 eqtr3i ⊢ N = M + M
9 8 oveq2i ⊢ A N = A M + M
10 1 nn0cni ⊢ A ∈ ℂ
11 expadd ⊢ A ∈ ℂ ∧ M ∈ ℕ 0 ∧ M ∈ ℕ 0 → A M + M = A M ⁢ A M
12 10 2 2 11 mp3an ⊢ A M + M = A M ⁢ A M
13 9 12 eqtri ⊢ A N = A M ⁢ A M
14 4 4 oveq12i ⊢ A M ⁢ A M = D ⁢ D
15 14 5 eqtri ⊢ A M ⁢ A M = C
16 13 15 eqtri ⊢ A N = C