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

Metamath Proof Explorer

Theorem root1id

Description: Property of an N -th root of unity. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion root1id ( 𝑁 ∈ ℕ → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) = 1 )

Proof

Step Hyp Ref Expression
1 neg1cn ⊢ - 1 ∈ ℂ
2 1 a1i ⊢ ( 𝑁 ∈ ℕ → - 1 ∈ ℂ )
3 2re ⊢ 2 ∈ ℝ
4 nndivre ⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 2 / 𝑁 ) ∈ ℝ )
5 3 4 mpan ⊢ ( 𝑁 ∈ ℕ → ( 2 / 𝑁 ) ∈ ℝ )
6 5 recnd ⊢ ( 𝑁 ∈ ℕ → ( 2 / 𝑁 ) ∈ ℂ )
7 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
8 2 6 7 cxpmul2d ⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑁 ) ) = ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) )
9 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
10 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
11 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
12 9 10 11 divcan1d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 / 𝑁 ) · 𝑁 ) = 2 )
13 12 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑁 ) ) = ( - 1 ↑𝑐 2 ) )
14 2nn0 ⊢ 2 ∈ ℕ0
15 cxpexp ⊢ ( ( - 1 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( - 1 ↑𝑐 2 ) = ( - 1 ↑ 2 ) )
16 1 14 15 mp2an ⊢ ( - 1 ↑𝑐 2 ) = ( - 1 ↑ 2 )
17 ax-1cn ⊢ 1 ∈ ℂ
18 sqneg ⊢ ( 1 ∈ ℂ → ( - 1 ↑ 2 ) = ( 1 ↑ 2 ) )
19 17 18 ax-mp ⊢ ( - 1 ↑ 2 ) = ( 1 ↑ 2 )
20 sq1 ⊢ ( 1 ↑ 2 ) = 1
21 16 19 20 3eqtri ⊢ ( - 1 ↑𝑐 2 ) = 1
22 13 21 eqtrdi ⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑁 ) ) = 1 )
23 8 22 eqtr3d ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) = 1 )