Metamath Proof Explorer


Theorem explog

Description: Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008)

Ref Expression
Assertion explog A A 0 N A N = e N log A

Proof

Step Hyp Ref Expression
1 logcl A A 0 log A
2 efexp log A N e N log A = e log A N
3 1 2 stoic3 A A 0 N e N log A = e log A N
4 eflog A A 0 e log A = A
5 4 3adant3 A A 0 N e log A = A
6 5 oveq1d A A 0 N e log A N = A N
7 3 6 eqtr2d A A 0 N A N = e N log A