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 ⊢ N ∈ ℕ → -1 2 N N = 1

Proof

Step Hyp Ref Expression
1 neg1cn ⊢ − 1 ∈ ℂ
2 1 a1i ⊢ N ∈ ℕ → − 1 ∈ ℂ
3 2re ⊢ 2 ∈ ℝ
4 nndivre ⊢ 2 ∈ ℝ ∧ N ∈ ℕ → 2 N ∈ ℝ
5 3 4 mpan ⊢ N ∈ ℕ → 2 N ∈ ℝ
6 5 recnd ⊢ N ∈ ℕ → 2 N ∈ ℂ
7 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
8 2 6 7 cxpmul2d ⊢ N ∈ ℕ → − 1 2 N ⋅ N = -1 2 N N
9 2cnd ⊢ N ∈ ℕ → 2 ∈ ℂ
10 nncn ⊢ N ∈ ℕ → N ∈ ℂ
11 nnne0 ⊢ N ∈ ℕ → N ≠ 0
12 9 10 11 divcan1d ⊢ N ∈ ℕ → 2 N ⋅ N = 2
13 12 oveq2d ⊢ N ∈ ℕ → − 1 2 N ⋅ N = − 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 ⊢ N ∈ ℕ → − 1 2 N ⋅ N = 1
23 8 22 eqtr3d ⊢ N ∈ ℕ → -1 2 N N = 1