cxproot

Description: The complex power function allows to write n-th roots via the idiom A ^c ( 1 / N ) . (Contributed by Mario Carneiro, 6-May-2015)

		Ref	Expression
	Assertion	cxproot	$⊢ (A \in ℂ \land N \in ℕ) \to {(A^{\frac{1}{N}})}^{N} = A$

Step	Hyp	Ref	Expression
1		nncn	$⊢ N \in ℕ \to N \in ℂ$
2	1	adantl	$⊢ (A \in ℂ \land N \in ℕ) \to N \in ℂ$
3		nnne0	$⊢ N \in ℕ \to N \neq 0$
4	3	adantl	$⊢ (A \in ℂ \land N \in ℕ) \to N \neq 0$
5	2 4	recid2d	$⊢ (A \in ℂ \land N \in ℕ) \to (\frac{1}{N}) \cdot N = 1$
6	5	oveq2d	$⊢ (A \in ℂ \land N \in ℕ) \to A^{(\frac{1}{N}) \cdot N} = A^{1}$
7		simpl	$⊢ (A \in ℂ \land N \in ℕ) \to A \in ℂ$
8		nnrecre	$⊢ N \in ℕ \to \frac{1}{N} \in ℝ$
9	8	adantl	$⊢ (A \in ℂ \land N \in ℕ) \to \frac{1}{N} \in ℝ$
10	9	recnd	$⊢ (A \in ℂ \land N \in ℕ) \to \frac{1}{N} \in ℂ$
11		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
12	11	adantl	$⊢ (A \in ℂ \land N \in ℕ) \to N \in ℕ_{0}$
13		cxpmul2	$⊢ (A \in ℂ \land \frac{1}{N} \in ℂ \land N \in ℕ_{0}) \to A^{(\frac{1}{N}) \cdot N} = {(A^{\frac{1}{N}})}^{N}$
14	7 10 12 13	syl3anc	$⊢ (A \in ℂ \land N \in ℕ) \to A^{(\frac{1}{N}) \cdot N} = {(A^{\frac{1}{N}})}^{N}$
15		cxp1	$⊢ A \in ℂ \to A^{1} = A$
16	15	adantr	$⊢ (A \in ℂ \land N \in ℕ) \to A^{1} = A$
17	6 14 16	3eqtr3d	$⊢ (A \in ℂ \land N \in ℕ) \to {(A^{\frac{1}{N}})}^{N} = A$

Metamath Proof Explorer