Theorem 1cubrlem

Description: The cube roots of unity. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Assertion	1cubrlem	$$⊢\left({\left(-1\right)}^{\frac{2}{3}}=\frac{-1+\mathrm{i}\sqrt{3}}{2}\wedge {\left({-1}^{\frac{2}{3}}\right)}^2=\frac{-1-\mathrm{i}\sqrt{3}}{2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		neg1cn	$$⊢-1\in ℂ$$
2		neg1ne0	$$⊢-1\ne 0$$
3		2re	$$⊢2\in ℝ$$
4		3nn	$$⊢3\in \mathbb{N}$$
5		nndivre	$$⊢\left(2\in ℝ\wedge 3\in \mathbb{N}\right)\to \frac{2}{3}\in ℝ$$
6	3 4 5	mp2an	$$⊢\frac{2}{3}\in ℝ$$
7	6	recni	$$⊢\frac{2}{3}\in ℂ$$
8		cxpef	$$⊢\left(-1\in ℂ\wedge -1\ne 0\wedge \frac{2}{3}\in ℂ\right)\to {\left(-1\right)}^{\frac{2}{3}}={\mathrm{e}}^{\left(\frac{2}{3}\right)\log -1}$$
9	1 2 7 8	mp3an	$$⊢{\left(-1\right)}^{\frac{2}{3}}={\mathrm{e}}^{\left(\frac{2}{3}\right)\log -1}$$
10		logm1	$$⊢\log -1=\mathrm{i}\mathrm{\pi }$$
11	10	oveq2i	$$⊢\left(\frac{2}{3}\right)\log -1=\left(\frac{2}{3}\right)\mathrm{i}\mathrm{\pi }$$
12		ax-icn	$$⊢\mathrm{i}\in ℂ$$
13		pire	$$⊢\mathrm{\pi }\in ℝ$$
14	13	recni	$$⊢\mathrm{\pi }\in ℂ$$
15	7 12 14	mul12i	$$⊢\left(\frac{2}{3}\right)\mathrm{i}\mathrm{\pi }=\mathrm{i}\left(\frac{2}{3}\right)\mathrm{\pi }$$
16	11 15	eqtri	$$⊢\left(\frac{2}{3}\right)\log -1=\mathrm{i}\left(\frac{2}{3}\right)\mathrm{\pi }$$
17	16	fveq2i	$$⊢{\mathrm{e}}^{\left(\frac{2}{3}\right)\log -1}={\mathrm{e}}^{\mathrm{i}\left(\frac{2}{3}\right)\mathrm{\pi }}$$
18		6nn	$$⊢6\in \mathbb{N}$$
19		nndivre	$$⊢\left(\mathrm{\pi }\in ℝ\wedge 6\in \mathbb{N}\right)\to \frac{\mathrm{\pi }}{6}\in ℝ$$
20	13 18 19	mp2an	$$⊢\frac{\mathrm{\pi }}{6}\in ℝ$$
21	20	recni	$$⊢\frac{\mathrm{\pi }}{6}\in ℂ$$
22		coshalfpip	$$⊢\frac{\mathrm{\pi }}{6}\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{6}\right)\right)=-\sin \left(\frac{\mathrm{\pi }}{6}\right)$$
23	21 22	ax-mp	$$⊢\cos \left(\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{6}\right)\right)=-\sin \left(\frac{\mathrm{\pi }}{6}\right)$$
24		2cn	$$⊢2\in ℂ$$
25		2ne0	$$⊢2\ne 0$$
26		divrec2	$$⊢\left(\mathrm{\pi }\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to \frac{\mathrm{\pi }}{2}=\left(\frac{1}{2}\right)\mathrm{\pi }$$
27	14 24 25 26	mp3an	$$⊢\frac{\mathrm{\pi }}{2}=\left(\frac{1}{2}\right)\mathrm{\pi }$$
28		6cn	$$⊢6\in ℂ$$
29	18	nnne0i	$$⊢6\ne 0$$
30		divrec2	$$⊢\left(\mathrm{\pi }\in ℂ\wedge 6\in ℂ\wedge 6\ne 0\right)\to \frac{\mathrm{\pi }}{6}=\left(\frac{1}{6}\right)\mathrm{\pi }$$
31	14 28 29 30	mp3an	$$⊢\frac{\mathrm{\pi }}{6}=\left(\frac{1}{6}\right)\mathrm{\pi }$$
32	27 31	oveq12i	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{6}\right)=\left(\frac{1}{2}\right)\mathrm{\pi }+\left(\frac{1}{6}\right)\mathrm{\pi }$$
33	24 25	reccli	$$⊢\frac{1}{2}\in ℂ$$
34	28 29	reccli	$$⊢\frac{1}{6}\in ℂ$$
35	33 34 14	adddiri	$$⊢\left(\left(\frac{1}{2}\right)+\left(\frac{1}{6}\right)\right)\mathrm{\pi }=\left(\frac{1}{2}\right)\mathrm{\pi }+\left(\frac{1}{6}\right)\mathrm{\pi }$$
36		halfpm6th	$$⊢\left(\left(\frac{1}{2}\right)-\left(\frac{1}{6}\right)=\frac{1}{3}\wedge \left(\frac{1}{2}\right)+\left(\frac{1}{6}\right)=\frac{2}{3}\right)$$
37	36	simpri	$$⊢\left(\frac{1}{2}\right)+\left(\frac{1}{6}\right)=\frac{2}{3}$$
38	37	oveq1i	$$⊢\left(\left(\frac{1}{2}\right)+\left(\frac{1}{6}\right)\right)\mathrm{\pi }=\left(\frac{2}{3}\right)\mathrm{\pi }$$
39	32 35 38	3eqtr2i	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{6}\right)=\left(\frac{2}{3}\right)\mathrm{\pi }$$
40	39	fveq2i	$$⊢\cos \left(\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{6}\right)\right)=\cos \left(\frac{2}{3}\right)\mathrm{\pi }$$
41		sincos6thpi	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{6}\right)=\frac{1}{2}\wedge \cos \left(\frac{\mathrm{\pi }}{6}\right)=\frac{\sqrt{3}}{2}\right)$$
42	41	simpli	$$⊢\sin \left(\frac{\mathrm{\pi }}{6}\right)=\frac{1}{2}$$
43	42	negeqi	$$⊢-\sin \left(\frac{\mathrm{\pi }}{6}\right)=-\frac{1}{2}$$
44		ax-1cn	$$⊢1\in ℂ$$
45		divneg	$$⊢\left(1\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to -\frac{1}{2}=\frac{-1}{2}$$
46	44 24 25 45	mp3an	$$⊢-\frac{1}{2}=\frac{-1}{2}$$
47	43 46	eqtri	$$⊢-\sin \left(\frac{\mathrm{\pi }}{6}\right)=\frac{-1}{2}$$
48	23 40 47	3eqtr3i	$$⊢\cos \left(\frac{2}{3}\right)\mathrm{\pi }=\frac{-1}{2}$$
49		sinhalfpip	$$⊢\frac{\mathrm{\pi }}{6}\in ℂ\to \sin \left(\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{6}\right)\right)=\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
50	21 49	ax-mp	$$⊢\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{6}\right)\right)=\cos \left(\frac{\mathrm{\pi }}{6}\right)$$
51	39	fveq2i	$$⊢\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{6}\right)\right)=\sin \left(\frac{2}{3}\right)\mathrm{\pi }$$
52	41	simpri	$$⊢\cos \left(\frac{\mathrm{\pi }}{6}\right)=\frac{\sqrt{3}}{2}$$
53	50 51 52	3eqtr3i	$$⊢\sin \left(\frac{2}{3}\right)\mathrm{\pi }=\frac{\sqrt{3}}{2}$$
54	53	oveq2i	$$⊢\mathrm{i}\sin \left(\frac{2}{3}\right)\mathrm{\pi }=\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)$$
55		3re	$$⊢3\in ℝ$$
56		3nn0	$$⊢3\in {\mathbb{N}}_0$$
57	56	nn0ge0i	$$⊢0\le 3$$
58		resqrtcl	$$⊢\left(3\in ℝ\wedge 0\le 3\right)\to \sqrt{3}\in ℝ$$
59	55 57 58	mp2an	$$⊢\sqrt{3}\in ℝ$$
60	59	recni	$$⊢\sqrt{3}\in ℂ$$
61	12 60 24 25	divassi	$$⊢\frac{\mathrm{i}\sqrt{3}}{2}=\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)$$
62	54 61	eqtr4i	$$⊢\mathrm{i}\sin \left(\frac{2}{3}\right)\mathrm{\pi }=\frac{\mathrm{i}\sqrt{3}}{2}$$
63	48 62	oveq12i	$$⊢\cos \left(\frac{2}{3}\right)\mathrm{\pi }+\mathrm{i}\sin \left(\frac{2}{3}\right)\mathrm{\pi }=\left(\frac{-1}{2}\right)+\left(\frac{\mathrm{i}\sqrt{3}}{2}\right)$$
64	7 14	mulcli	$$⊢\left(\frac{2}{3}\right)\mathrm{\pi }\in ℂ$$
65		efival	$$⊢\left(\frac{2}{3}\right)\mathrm{\pi }\in ℂ\to {\mathrm{e}}^{\mathrm{i}\left(\frac{2}{3}\right)\mathrm{\pi }}=\cos \left(\frac{2}{3}\right)\mathrm{\pi }+\mathrm{i}\sin \left(\frac{2}{3}\right)\mathrm{\pi }$$
66	64 65	ax-mp	$$⊢{\mathrm{e}}^{\mathrm{i}\left(\frac{2}{3}\right)\mathrm{\pi }}=\cos \left(\frac{2}{3}\right)\mathrm{\pi }+\mathrm{i}\sin \left(\frac{2}{3}\right)\mathrm{\pi }$$
67	12 60	mulcli	$$⊢\mathrm{i}\sqrt{3}\in ℂ$$
68	1 67 24 25	divdiri	$$⊢\frac{-1+\mathrm{i}\sqrt{3}}{2}=\left(\frac{-1}{2}\right)+\left(\frac{\mathrm{i}\sqrt{3}}{2}\right)$$
69	63 66 68	3eqtr4i	$$⊢{\mathrm{e}}^{\mathrm{i}\left(\frac{2}{3}\right)\mathrm{\pi }}=\frac{-1+\mathrm{i}\sqrt{3}}{2}$$
70	9 17 69	3eqtri	$$⊢{\left(-1\right)}^{\frac{2}{3}}=\frac{-1+\mathrm{i}\sqrt{3}}{2}$$
71		1z	$$⊢1\in \mathbb{Z}$$
72		root1cj	$$⊢\left(3\in \mathbb{N}\wedge 1\in \mathbb{Z}\right)\to \stackrel{‾}{{\left({-1}^{\frac{2}{3}}\right)}^1}={\left({-1}^{\frac{2}{3}}\right)}^{3-1}$$
73	4 71 72	mp2an	$$⊢\stackrel{‾}{{\left({-1}^{\frac{2}{3}}\right)}^1}={\left({-1}^{\frac{2}{3}}\right)}^{3-1}$$
74		cxpcl	$$⊢\left(-1\in ℂ\wedge \frac{2}{3}\in ℂ\right)\to {\left(-1\right)}^{\frac{2}{3}}\in ℂ$$
75	1 7 74	mp2an	$$⊢{\left(-1\right)}^{\frac{2}{3}}\in ℂ$$
76		exp1	$$⊢{\left(-1\right)}^{\frac{2}{3}}\in ℂ\to {\left({-1}^{\frac{2}{3}}\right)}^1={\left(-1\right)}^{\frac{2}{3}}$$
77	75 76	ax-mp	$$⊢{\left({-1}^{\frac{2}{3}}\right)}^1={\left(-1\right)}^{\frac{2}{3}}$$
78	77 70	eqtri	$$⊢{\left({-1}^{\frac{2}{3}}\right)}^1=\frac{-1+\mathrm{i}\sqrt{3}}{2}$$
79	78	fveq2i	$$⊢\stackrel{‾}{{\left({-1}^{\frac{2}{3}}\right)}^1}=\overline{\frac{-1+\mathrm{i}\sqrt{3}}{2}}$$
80	1 67	addcli	$$⊢-1+\mathrm{i}\sqrt{3}\in ℂ$$
81	80 24	cjdivi	$$⊢2\ne 0\to \overline{\frac{-1+\mathrm{i}\sqrt{3}}{2}}=\frac{\overline{-1+\mathrm{i}\sqrt{3}}}{\bar{2}}$$
82	25 81	ax-mp	$$⊢\overline{\frac{-1+\mathrm{i}\sqrt{3}}{2}}=\frac{\overline{-1+\mathrm{i}\sqrt{3}}}{\bar{2}}$$
83	1 67	cjaddi	$$⊢\overline{-1+\mathrm{i}\sqrt{3}}=\overline{-1}+\overline{\mathrm{i}\sqrt{3}}$$
84		neg1rr	$$⊢-1\in ℝ$$
85		cjre	$$⊢-1\in ℝ\to \overline{-1}=-1$$
86	84 85	ax-mp	$$⊢\overline{-1}=-1$$
87	12 60	cjmuli	$$⊢\overline{\mathrm{i}\sqrt{3}}=\bar{\mathrm{i}}\bar{\sqrt{3}}$$
88		cji	$$⊢\bar{\mathrm{i}}=-\mathrm{i}$$
89		cjre	$$⊢\sqrt{3}\in ℝ\to \bar{\sqrt{3}}=\sqrt{3}$$
90	59 89	ax-mp	$$⊢\bar{\sqrt{3}}=\sqrt{3}$$
91	88 90	oveq12i	$$⊢\bar{\mathrm{i}}\bar{\sqrt{3}}=\left(-\mathrm{i}\right)\sqrt{3}$$
92	12 60	mulneg1i	$$⊢\left(-\mathrm{i}\right)\sqrt{3}=-\mathrm{i}\sqrt{3}$$
93	87 91 92	3eqtri	$$⊢\overline{\mathrm{i}\sqrt{3}}=-\mathrm{i}\sqrt{3}$$
94	86 93	oveq12i	$$⊢\overline{-1}+\overline{\mathrm{i}\sqrt{3}}=-1+\left(-\mathrm{i}\sqrt{3}\right)$$
95	1 67	negsubi	$$⊢-1+\left(-\mathrm{i}\sqrt{3}\right)=-1-\mathrm{i}\sqrt{3}$$
96	83 94 95	3eqtri	$$⊢\overline{-1+\mathrm{i}\sqrt{3}}=-1-\mathrm{i}\sqrt{3}$$
97		cjre	$$⊢2\in ℝ\to \bar{2}=2$$
98	3 97	ax-mp	$$⊢\bar{2}=2$$
99	96 98	oveq12i	$$⊢\frac{\overline{-1+\mathrm{i}\sqrt{3}}}{\bar{2}}=\frac{-1-\mathrm{i}\sqrt{3}}{2}$$
100	79 82 99	3eqtri	$$⊢\stackrel{‾}{{\left({-1}^{\frac{2}{3}}\right)}^1}=\frac{-1-\mathrm{i}\sqrt{3}}{2}$$
101		3m1e2	$$⊢3-1=2$$
102	101	oveq2i	$$⊢{\left({-1}^{\frac{2}{3}}\right)}^{3-1}={\left({-1}^{\frac{2}{3}}\right)}^2$$
103	73 100 102	3eqtr3ri	$$⊢{\left({-1}^{\frac{2}{3}}\right)}^2=\frac{-1-\mathrm{i}\sqrt{3}}{2}$$
104	70 103	pm3.2i	$$⊢\left({\left(-1\right)}^{\frac{2}{3}}=\frac{-1+\mathrm{i}\sqrt{3}}{2}\wedge {\left({-1}^{\frac{2}{3}}\right)}^2=\frac{-1-\mathrm{i}\sqrt{3}}{2}\right)$$