Metamath Proof Explorer


Theorem cxpp1

Description: Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpp1 A A 0 B A B + 1 = A B A

Proof

Step Hyp Ref Expression
1 ax-1cn 1
2 cxpadd A A 0 B 1 A B + 1 = A B A 1
3 1 2 mp3an3 A A 0 B A B + 1 = A B A 1
4 3 3impa A A 0 B A B + 1 = A B A 1
5 cxp1 A A 1 = A
6 5 3ad2ant1 A A 0 B A 1 = A
7 6 oveq2d A A 0 B A B A 1 = A B A
8 4 7 eqtrd A A 0 B A B + 1 = A B A