This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 / 𝑁 ) ) ↑ 𝑁 ) = 𝐴 )