1cxp

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

		Ref	Expression
	Assertion	1cxp	$⊢ A \in ℂ \to 1^{A} = 1$

Step	Hyp	Ref	Expression
1		ax-1cn	$⊢ 1 \in ℂ$
2		ax-1ne0	$⊢ 1 \neq 0$
3		cxpef	$⊢ (1 \in ℂ \land 1 \neq 0 \land A \in ℂ) \to 1^{A} = e^{A \log 1}$
4	1 2 3	mp3an12	$⊢ A \in ℂ \to 1^{A} = e^{A \log 1}$
5		log1	$⊢ \log 1 = 0$
6	5	oveq2i	$⊢ A \log 1 = A \cdot 0$
7		mul01	$⊢ A \in ℂ \to A \cdot 0 = 0$
8	6 7	eqtrid	$⊢ A \in ℂ \to A \log 1 = 0$
9	8	fveq2d	$⊢ A \in ℂ \to e^{A \log 1} = e^{0}$
10		ef0	$⊢ e^{0} = 1$
11	9 10	eqtrdi	$⊢ A \in ℂ \to e^{A \log 1} = 1$
12	4 11	eqtrd	$⊢ A \in ℂ \to 1^{A} = 1$

Metamath Proof Explorer