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	$⊢ (N \in ℕ \land K \in ℤ) \to \overline{{({-1}^{\frac{2}{N}})}^{K}} = {({-1}^{\frac{2}{N}})}^{N - K}$

Proof

Step	Hyp	Ref	Expression
1		neg1cn	$⊢ - 1 \in ℂ$
2		2re	$⊢ 2 \in ℝ$
3		simpl	$⊢ (N \in ℕ \land K \in ℤ) \to N \in ℕ$
4		nndivre	$⊢ (2 \in ℝ \land N \in ℕ) \to \frac{2}{N} \in ℝ$
5	2 3 4	sylancr	$⊢ (N \in ℕ \land K \in ℤ) \to \frac{2}{N} \in ℝ$
6	5	recnd	$⊢ (N \in ℕ \land K \in ℤ) \to \frac{2}{N} \in ℂ$
7		cxpcl	$⊢ (- 1 \in ℂ \land \frac{2}{N} \in ℂ) \to {(- 1)}^{\frac{2}{N}} \in ℂ$
8	1 6 7	sylancr	$⊢ (N \in ℕ \land K \in ℤ) \to {(- 1)}^{\frac{2}{N}} \in ℂ$
9	1	a1i	$⊢ (N \in ℕ \land K \in ℤ) \to - 1 \in ℂ$
10		neg1ne0	$⊢ - 1 \neq 0$
11	10	a1i	$⊢ (N \in ℕ \land K \in ℤ) \to - 1 \neq 0$
12	9 11 6	cxpne0d	$⊢ (N \in ℕ \land K \in ℤ) \to {(- 1)}^{\frac{2}{N}} \neq 0$
13		simpr	$⊢ (N \in ℕ \land K \in ℤ) \to K \in ℤ$
14		nnz	$⊢ N \in ℕ \to N \in ℤ$
15	14	adantr	$⊢ (N \in ℕ \land K \in ℤ) \to N \in ℤ$
16	8 12 13 15	expsubd	$⊢ (N \in ℕ \land K \in ℤ) \to {({-1}^{\frac{2}{N}})}^{N - K} = \frac{{({-1}^{\frac{2}{N}})}^{N}}{{({-1}^{\frac{2}{N}})}^{K}}$
17		root1id	$⊢ N \in ℕ \to {({-1}^{\frac{2}{N}})}^{N} = 1$
18	17	adantr	$⊢ (N \in ℕ \land K \in ℤ) \to {({-1}^{\frac{2}{N}})}^{N} = 1$
19	18	oveq1d	$⊢ (N \in ℕ \land K \in ℤ) \to \frac{{({-1}^{\frac{2}{N}})}^{N}}{{({-1}^{\frac{2}{N}})}^{K}} = \frac{1}{{({-1}^{\frac{2}{N}})}^{K}}$
20	8 12 13	expclzd	$⊢ (N \in ℕ \land K \in ℤ) \to {({-1}^{\frac{2}{N}})}^{K} \in ℂ$
21	8 12 13	expne0d	$⊢ (N \in ℕ \land K \in ℤ) \to {({-1}^{\frac{2}{N}})}^{K} \neq 0$
22		recval	$⊢ ({({-1}^{\frac{2}{N}})}^{K} \in ℂ \land {({-1}^{\frac{2}{N}})}^{K} \neq 0) \to \frac{1}{{({-1}^{\frac{2}{N}})}^{K}} = \frac{\overline{{({-1}^{\frac{2}{N}})}^{K}}}{{\|{({-1}^{\frac{2}{N}})}^{K}\|}^{2}}$
23	20 21 22	syl2anc	$⊢ (N \in ℕ \land K \in ℤ) \to \frac{1}{{({-1}^{\frac{2}{N}})}^{K}} = \frac{\overline{{({-1}^{\frac{2}{N}})}^{K}}}{{\|{({-1}^{\frac{2}{N}})}^{K}\|}^{2}}$
24		absexpz	$⊢ ({(- 1)}^{\frac{2}{N}} \in ℂ \land {(- 1)}^{\frac{2}{N}} \neq 0 \land K \in ℤ) \to \|{({-1}^{\frac{2}{N}})}^{K}\| = {\|{(- 1)}^{\frac{2}{N}}\|}^{K}$
25	8 12 13 24	syl3anc	$⊢ (N \in ℕ \land K \in ℤ) \to \|{({-1}^{\frac{2}{N}})}^{K}\| = {\|{(- 1)}^{\frac{2}{N}}\|}^{K}$
26		abscxp2	$⊢ (- 1 \in ℂ \land \frac{2}{N} \in ℝ) \to \|{(- 1)}^{\frac{2}{N}}\| = {\|- 1\|}^{\frac{2}{N}}$
27	1 5 26	sylancr	$⊢ (N \in ℕ \land K \in ℤ) \to \|{(- 1)}^{\frac{2}{N}}\| = {\|- 1\|}^{\frac{2}{N}}$
28		ax-1cn	$⊢ 1 \in ℂ$
29	28	absnegi	$⊢ \|- 1\| = \|1\|$
30		abs1	$⊢ \|1\| = 1$
31	29 30	eqtri	$⊢ \|- 1\| = 1$
32	31	oveq1i	$⊢ {\|- 1\|}^{\frac{2}{N}} = 1^{\frac{2}{N}}$
33	27 32	eqtrdi	$⊢ (N \in ℕ \land K \in ℤ) \to \|{(- 1)}^{\frac{2}{N}}\| = 1^{\frac{2}{N}}$
34	6	1cxpd	$⊢ (N \in ℕ \land K \in ℤ) \to 1^{\frac{2}{N}} = 1$
35	33 34	eqtrd	$⊢ (N \in ℕ \land K \in ℤ) \to \|{(- 1)}^{\frac{2}{N}}\| = 1$
36	35	oveq1d	$⊢ (N \in ℕ \land K \in ℤ) \to {\|{(- 1)}^{\frac{2}{N}}\|}^{K} = 1^{K}$
37		1exp	$⊢ K \in ℤ \to 1^{K} = 1$
38	37	adantl	$⊢ (N \in ℕ \land K \in ℤ) \to 1^{K} = 1$
39	25 36 38	3eqtrd	$⊢ (N \in ℕ \land K \in ℤ) \to \|{({-1}^{\frac{2}{N}})}^{K}\| = 1$
40	39	oveq1d	$⊢ (N \in ℕ \land K \in ℤ) \to {\|{({-1}^{\frac{2}{N}})}^{K}\|}^{2} = 1^{2}$
41		sq1	$⊢ 1^{2} = 1$
42	40 41	eqtrdi	$⊢ (N \in ℕ \land K \in ℤ) \to {\|{({-1}^{\frac{2}{N}})}^{K}\|}^{2} = 1$
43	42	oveq2d	$⊢ (N \in ℕ \land K \in ℤ) \to \frac{\overline{{({-1}^{\frac{2}{N}})}^{K}}}{{\|{({-1}^{\frac{2}{N}})}^{K}\|}^{2}} = \frac{\overline{{({-1}^{\frac{2}{N}})}^{K}}}{1}$
44	20	cjcld	$⊢ (N \in ℕ \land K \in ℤ) \to \overline{{({-1}^{\frac{2}{N}})}^{K}} \in ℂ$
45	44	div1d	$⊢ (N \in ℕ \land K \in ℤ) \to \frac{\overline{{({-1}^{\frac{2}{N}})}^{K}}}{1} = \overline{{({-1}^{\frac{2}{N}})}^{K}}$
46	23 43 45	3eqtrd	$⊢ (N \in ℕ \land K \in ℤ) \to \frac{1}{{({-1}^{\frac{2}{N}})}^{K}} = \overline{{({-1}^{\frac{2}{N}})}^{K}}$
47	16 19 46	3eqtrrd	$⊢ (N \in ℕ \land K \in ℤ) \to \overline{{({-1}^{\frac{2}{N}})}^{K}} = {({-1}^{\frac{2}{N}})}^{N - K}$

Metamath Proof Explorer

Theorem root1cj

Proof