Metamath Proof Explorer


Theorem 1cxp

Description: Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion 1cxp A1A=1

Proof

Step Hyp Ref Expression
1 ax-1cn 1
2 ax-1ne0 10
3 cxpef 110A1A=eAlog1
4 1 2 3 mp3an12 A1A=eAlog1
5 log1 log1=0
6 5 oveq2i Alog1=A0
7 mul01 AA0=0
8 6 7 eqtrid AAlog1=0
9 8 fveq2d AeAlog1=e0
10 ef0 e0=1
11 9 10 eqtrdi AeAlog1=1
12 4 11 eqtrd A1A=1