cxpef

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

		Ref	Expression
	Assertion	cxpef	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to A^{B} = e^{B \log A}$

Step	Hyp	Ref	Expression
1		cxpval	$⊢ (A \in ℂ \land B \in ℂ) \to A^{B} = if (A = 0, if (B = 0, 1, 0), e^{B \log A})$
2	1	3adant2	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to A^{B} = if (A = 0, if (B = 0, 1, 0), e^{B \log A})$
3		simp2	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to A \neq 0$
4	3	neneqd	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to \neg A = 0$
5	4	iffalsed	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to if (A = 0, if (B = 0, 1, 0), e^{B \log A}) = e^{B \log A}$
6	2 5	eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to A^{B} = e^{B \log A}$

Metamath Proof Explorer