Metamath Proof Explorer

Theorem root1cj

Description: Within the N -th roots of unity, the conjugate of the K -th root is the N - K -th root. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion root1cj ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) = ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ ( 𝑁 − 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 neg1cn ⊢ - 1 ∈ ℂ
2 2re ⊢ 2 ∈ ℝ
3 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℕ )
4 nndivre ⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 2 / 𝑁 ) ∈ ℝ )
5 2 3 4 sylancr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 2 / 𝑁 ) ∈ ℝ )
6 5 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 2 / 𝑁 ) ∈ ℂ )
7 cxpcl ⊢ ( ( - 1 ∈ ℂ ∧ ( 2 / 𝑁 ) ∈ ℂ ) → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ℂ )
8 1 6 7 sylancr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ℂ )
9 1 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → - 1 ∈ ℂ )
10 neg1ne0 ⊢ - 1 ≠ 0
11 10 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → - 1 ≠ 0 )
12 9 11 6 cxpne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ≠ 0 )
13 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℤ )
14 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
15 14 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℤ )
16 8 12 13 15 expsubd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ ( 𝑁 − 𝐾 ) ) = ( ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) / ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) )
17 root1id ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) = 1 )
18 17 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) = 1 )
19 18 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) / ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) = ( 1 / ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) )
20 8 12 13 expclzd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ∈ ℂ )
21 8 12 13 expne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ≠ 0 )
22 recval ⊢ ( ( ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ∈ ℂ ∧ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ≠ 0 ) → ( 1 / ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) = ( ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) / ( ( abs ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) ↑ 2 ) ) )
23 20 21 22 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 1 / ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) = ( ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) / ( ( abs ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) ↑ 2 ) ) )
24 absexpz ⊢ ( ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ℂ ∧ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ≠ 0 ∧ 𝐾 ∈ ℤ ) → ( abs ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) = ( ( abs ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) ↑ 𝐾 ) )
25 8 12 13 24 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( abs ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) = ( ( abs ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) ↑ 𝐾 ) )
26 abscxp2 ⊢ ( ( - 1 ∈ ℂ ∧ ( 2 / 𝑁 ) ∈ ℝ ) → ( abs ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = ( ( abs ‘ - 1 ) ↑𝑐 ( 2 / 𝑁 ) ) )
27 1 5 26 sylancr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( abs ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = ( ( abs ‘ - 1 ) ↑𝑐 ( 2 / 𝑁 ) ) )
28 ax-1cn ⊢ 1 ∈ ℂ
29 28 absnegi ⊢ ( abs ‘ - 1 ) = ( abs ‘ 1 )
30 abs1 ⊢ ( abs ‘ 1 ) = 1
31 29 30 eqtri ⊢ ( abs ‘ - 1 ) = 1
32 31 oveq1i ⊢ ( ( abs ‘ - 1 ) ↑𝑐 ( 2 / 𝑁 ) ) = ( 1 ↑𝑐 ( 2 / 𝑁 ) )
33 27 32 eqtrdi ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( abs ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = ( 1 ↑𝑐 ( 2 / 𝑁 ) ) )
34 6 1cxpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 1 ↑𝑐 ( 2 / 𝑁 ) ) = 1 )
35 33 34 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( abs ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = 1 )
36 35 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( abs ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) ↑ 𝐾 ) = ( 1 ↑ 𝐾 ) )
37 1exp ⊢ ( 𝐾 ∈ ℤ → ( 1 ↑ 𝐾 ) = 1 )
38 37 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 1 ↑ 𝐾 ) = 1 )
39 25 36 38 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( abs ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) = 1 )
40 39 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( abs ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
41 sq1 ⊢ ( 1 ↑ 2 ) = 1
42 40 41 eqtrdi ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( abs ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) ↑ 2 ) = 1 )
43 42 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) / ( ( abs ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) ↑ 2 ) ) = ( ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) / 1 ) )
44 20 cjcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) ∈ ℂ )
45 44 div1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) / 1 ) = ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) )
46 23 43 45 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 1 / ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) = ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) )
47 16 19 46 3eqtrrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) ) = ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ ( 𝑁 − 𝐾 ) ) )