Metamath Proof Explorer


Theorem cxpp1d

Description: Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses cxp0d.1 φ A
cxpefd.2 φ A 0
cxpefd.3 φ B
Assertion cxpp1d φ A B + 1 = A B A

Proof

Step Hyp Ref Expression
1 cxp0d.1 φ A
2 cxpefd.2 φ A 0
3 cxpefd.3 φ B
4 cxpp1 A A 0 B A B + 1 = A B A
5 1 2 3 4 syl3anc φ A B + 1 = A B A