0cxp

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

		Ref	Expression
	Assertion	0cxp	$⊢ (A \in ℂ \land A \neq 0) \to 0^{A} = 0$

Step	Hyp	Ref	Expression
1		0cn	$⊢ 0 \in ℂ$
2		cxpval	$⊢ (0 \in ℂ \land A \in ℂ) \to 0^{A} = if (0 = 0, if (A = 0, 1, 0), e^{A \log 0})$
3	1 2	mpan	$⊢ A \in ℂ \to 0^{A} = if (0 = 0, if (A = 0, 1, 0), e^{A \log 0})$
4		eqid	$⊢ 0 = 0$
5	4	iftruei	$⊢ if (0 = 0, if (A = 0, 1, 0), e^{A \log 0}) = if (A = 0, 1, 0)$
6	3 5	eqtrdi	$⊢ A \in ℂ \to 0^{A} = if (A = 0, 1, 0)$
7		ifnefalse	$⊢ A \neq 0 \to if (A = 0, 1, 0) = 0$
8	6 7	sylan9eq	$⊢ (A \in ℂ \land A \neq 0) \to 0^{A} = 0$

Metamath Proof Explorer