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 / 𝑁 ) ) ↑ ( 𝑁𝐾 ) ) )