Theorem 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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
2	1	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
3		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
5	2 4	recid2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 1 / 𝑁 ) · 𝑁 ) = 1 )
6	5	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑𝑐 ( ( 1 / 𝑁 ) · 𝑁 ) ) = ( 𝐴 ↑𝑐 1 ) )
7		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℂ )
8		nnrecre	⊢ ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℝ )
9	8	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 1 / 𝑁 ) ∈ ℝ )
10	9	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 1 / 𝑁 ) ∈ ℂ )
11		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
12	11	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
13		cxpmul2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 / 𝑁 ) ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑𝑐 ( ( 1 / 𝑁 ) · 𝑁 ) ) = ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) )
14	7 10 12 13	syl3anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑𝑐 ( ( 1 / 𝑁 ) · 𝑁 ) ) = ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) )
15		cxp1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 1 ) = 𝐴 )
16	15	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑𝑐 1 ) = 𝐴 )
17	6 14 16	3eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = 𝐴 )