Theorem 1cubr

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

	Ref	Expression
Hypothesis	1cubr.r	$$⊢R=\left\{1,\frac{-1+\mathrm{i}\sqrt{3}}{2},\frac{-1-\mathrm{i}\sqrt{3}}{2}\right\}$$
Assertion	1cubr	$$⊢A\in R\leftrightarrow \left(A\in ℂ\wedge A^3=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		1cubr.r	$$⊢R=\left\{1,\frac{-1+\mathrm{i}\sqrt{3}}{2},\frac{-1-\mathrm{i}\sqrt{3}}{2}\right\}$$
2		ax-1cn	$$⊢1\in ℂ$$
3		neg1cn	$$⊢-1\in ℂ$$
4		ax-icn	$$⊢\mathrm{i}\in ℂ$$
5		3cn	$$⊢3\in ℂ$$
6		sqrtcl	$$⊢3\in ℂ\to \sqrt{3}\in ℂ$$
7	5 6	ax-mp	$$⊢\sqrt{3}\in ℂ$$
8	4 7	mulcli	$$⊢\mathrm{i}\sqrt{3}\in ℂ$$
9	3 8	addcli	$$⊢-1+\mathrm{i}\sqrt{3}\in ℂ$$
10		halfcl	$$⊢-1+\mathrm{i}\sqrt{3}\in ℂ\to \frac{-1+\mathrm{i}\sqrt{3}}{2}\in ℂ$$
11	9 10	ax-mp	$$⊢\frac{-1+\mathrm{i}\sqrt{3}}{2}\in ℂ$$
12	3 8	subcli	$$⊢-1-\mathrm{i}\sqrt{3}\in ℂ$$
13		halfcl	$$⊢-1-\mathrm{i}\sqrt{3}\in ℂ\to \frac{-1-\mathrm{i}\sqrt{3}}{2}\in ℂ$$
14	12 13	ax-mp	$$⊢\frac{-1-\mathrm{i}\sqrt{3}}{2}\in ℂ$$
15	2 11 14	3pm3.2i	$$⊢\left(1\in ℂ\wedge \frac{-1+\mathrm{i}\sqrt{3}}{2}\in ℂ\wedge \frac{-1-\mathrm{i}\sqrt{3}}{2}\in ℂ\right)$$
16	2	elexi	$$⊢1\in \mathrm{V}$$
17		ovex	$$⊢\frac{-1+\mathrm{i}\sqrt{3}}{2}\in \mathrm{V}$$
18		ovex	$$⊢\frac{-1-\mathrm{i}\sqrt{3}}{2}\in \mathrm{V}$$
19	16 17 18	tpss	$$⊢\left(1\in ℂ\wedge \frac{-1+\mathrm{i}\sqrt{3}}{2}\in ℂ\wedge \frac{-1-\mathrm{i}\sqrt{3}}{2}\in ℂ\right)\leftrightarrow \left\{1,\frac{-1+\mathrm{i}\sqrt{3}}{2},\frac{-1-\mathrm{i}\sqrt{3}}{2}\right\}\subseteq ℂ$$
20	15 19	mpbi	$$⊢\left\{1,\frac{-1+\mathrm{i}\sqrt{3}}{2},\frac{-1-\mathrm{i}\sqrt{3}}{2}\right\}\subseteq ℂ$$
21	1 20	eqsstri	$$⊢R\subseteq ℂ$$
22	21	sseli	$$⊢A\in R\to A\in ℂ$$
23	22	pm4.71ri	$$⊢A\in R\leftrightarrow \left(A\in ℂ\wedge A\in R\right)$$
24		3nn	$$⊢3\in \mathbb{N}$$
25		cxpeq	$$⊢\left(A\in ℂ\wedge 3\in \mathbb{N}\wedge 1\in ℂ\right)\to \left(A^3=1\leftrightarrow \exists n\in \left(0\dots 3-1\right)A=1^{\frac{1}{3}}{\left({-1}^{\frac{2}{3}}\right)}^n\right)$$
26	24 2 25	mp3an23	$$⊢A\in ℂ\to \left(A^3=1\leftrightarrow \exists n\in \left(0\dots 3-1\right)A=1^{\frac{1}{3}}{\left({-1}^{\frac{2}{3}}\right)}^n\right)$$
27		eltpg	$$⊢A\in ℂ\to \left(A\in \left\{1,\frac{-1+\mathrm{i}\sqrt{3}}{2},\frac{-1-\mathrm{i}\sqrt{3}}{2}\right\}\leftrightarrow \left(A=1\vee A=\frac{-1+\mathrm{i}\sqrt{3}}{2}\vee A=\frac{-1-\mathrm{i}\sqrt{3}}{2}\right)\right)$$
28	1	eleq2i	$$⊢A\in R\leftrightarrow A\in \left\{1,\frac{-1+\mathrm{i}\sqrt{3}}{2},\frac{-1-\mathrm{i}\sqrt{3}}{2}\right\}$$
29		3m1e2	$$⊢3-1=2$$
30		2cn	$$⊢2\in ℂ$$
31	30	addid2i	$$⊢0+2=2$$
32	29 31	eqtr4i	$$⊢3-1=0+2$$
33	32	oveq2i	$$⊢\left(0\dots 3-1\right)=\left(0\dots 0+2\right)$$
34		0z	$$⊢0\in \mathbb{Z}$$
35		fztp	$$⊢0\in \mathbb{Z}\to \left(0\dots 0+2\right)=\left\{0,0+1,0+2\right\}$$
36	34 35	ax-mp	$$⊢\left(0\dots 0+2\right)=\left\{0,0+1,0+2\right\}$$
37	33 36	eqtri	$$⊢\left(0\dots 3-1\right)=\left\{0,0+1,0+2\right\}$$
38	37	rexeqi	$$⊢\exists n\in \left(0\dots 3-1\right)A=1^{\frac{1}{3}}{\left({-1}^{\frac{2}{3}}\right)}^n\leftrightarrow \exists n\in \left\{0,0+1,0+2\right\}A=1^{\frac{1}{3}}{\left({-1}^{\frac{2}{3}}\right)}^n$$
39		3ne0	$$⊢3\ne 0$$
40	5 39	reccli	$$⊢\frac{1}{3}\in ℂ$$
41		1cxp	$$⊢\frac{1}{3}\in ℂ\to 1^{\frac{1}{3}}=1$$
42	40 41	ax-mp	$$⊢1^{\frac{1}{3}}=1$$
43	42	oveq1i	$$⊢1^{\frac{1}{3}}{\left({-1}^{\frac{2}{3}}\right)}^n=1{\left({-1}^{\frac{2}{3}}\right)}^n$$
44	43	eqeq2i	$$⊢A=1^{\frac{1}{3}}{\left({-1}^{\frac{2}{3}}\right)}^n\leftrightarrow A=1{\left({-1}^{\frac{2}{3}}\right)}^n$$
45	44	rexbii	$$⊢\exists n\in \left\{0,0+1,0+2\right\}A=1^{\frac{1}{3}}{\left({-1}^{\frac{2}{3}}\right)}^n\leftrightarrow \exists n\in \left\{0,0+1,0+2\right\}A=1{\left({-1}^{\frac{2}{3}}\right)}^n$$
46	34	elexi	$$⊢0\in \mathrm{V}$$
47		ovex	$$⊢0+1\in \mathrm{V}$$
48		ovex	$$⊢0+2\in \mathrm{V}$$
49		oveq2	$$⊢n=0\to {\left({-1}^{\frac{2}{3}}\right)}^n={\left({-1}^{\frac{2}{3}}\right)}^0$$
50	30 5 39	divcli	$$⊢\frac{2}{3}\in ℂ$$
51		cxpcl	$$⊢\left(-1\in ℂ\wedge \frac{2}{3}\in ℂ\right)\to {\left(-1\right)}^{\frac{2}{3}}\in ℂ$$
52	3 50 51	mp2an	$$⊢{\left(-1\right)}^{\frac{2}{3}}\in ℂ$$
53		exp0	$$⊢{\left(-1\right)}^{\frac{2}{3}}\in ℂ\to {\left({-1}^{\frac{2}{3}}\right)}^0=1$$
54	52 53	ax-mp	$$⊢{\left({-1}^{\frac{2}{3}}\right)}^0=1$$
55	49 54	eqtrdi	$$⊢n=0\to {\left({-1}^{\frac{2}{3}}\right)}^n=1$$
56	55	oveq2d	$$⊢n=0\to 1{\left({-1}^{\frac{2}{3}}\right)}^n=1\cdot 1$$
57		1t1e1	$$⊢1\cdot 1=1$$
58	56 57	eqtrdi	$$⊢n=0\to 1{\left({-1}^{\frac{2}{3}}\right)}^n=1$$
59	58	eqeq2d	$$⊢n=0\to \left(A=1{\left({-1}^{\frac{2}{3}}\right)}^n\leftrightarrow A=1\right)$$
60		id	$$⊢n=0+1\to n=0+1$$
61	2	addid2i	$$⊢0+1=1$$
62	60 61	eqtrdi	$$⊢n=0+1\to n=1$$
63	62	oveq2d	$$⊢n=0+1\to {\left({-1}^{\frac{2}{3}}\right)}^n={\left({-1}^{\frac{2}{3}}\right)}^1$$
64		exp1	$$⊢{\left(-1\right)}^{\frac{2}{3}}\in ℂ\to {\left({-1}^{\frac{2}{3}}\right)}^1={\left(-1\right)}^{\frac{2}{3}}$$
65	52 64	ax-mp	$$⊢{\left({-1}^{\frac{2}{3}}\right)}^1={\left(-1\right)}^{\frac{2}{3}}$$
66	63 65	eqtrdi	$$⊢n=0+1\to {\left({-1}^{\frac{2}{3}}\right)}^n={\left(-1\right)}^{\frac{2}{3}}$$
67	66	oveq2d	$$⊢n=0+1\to 1{\left({-1}^{\frac{2}{3}}\right)}^n=1{\left(-1\right)}^{\frac{2}{3}}$$
68	52	mulid2i	$$⊢1{\left(-1\right)}^{\frac{2}{3}}={\left(-1\right)}^{\frac{2}{3}}$$
69		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)$$
70	69	simpli	$$⊢{\left(-1\right)}^{\frac{2}{3}}=\frac{-1+\mathrm{i}\sqrt{3}}{2}$$
71	68 70	eqtri	$$⊢1{\left(-1\right)}^{\frac{2}{3}}=\frac{-1+\mathrm{i}\sqrt{3}}{2}$$
72	67 71	eqtrdi	$$⊢n=0+1\to 1{\left({-1}^{\frac{2}{3}}\right)}^n=\frac{-1+\mathrm{i}\sqrt{3}}{2}$$
73	72	eqeq2d	$$⊢n=0+1\to \left(A=1{\left({-1}^{\frac{2}{3}}\right)}^n\leftrightarrow A=\frac{-1+\mathrm{i}\sqrt{3}}{2}\right)$$
74		id	$$⊢n=0+2\to n=0+2$$
75	74 31	eqtrdi	$$⊢n=0+2\to n=2$$
76	75	oveq2d	$$⊢n=0+2\to {\left({-1}^{\frac{2}{3}}\right)}^n={\left({-1}^{\frac{2}{3}}\right)}^2$$
77	76	oveq2d	$$⊢n=0+2\to 1{\left({-1}^{\frac{2}{3}}\right)}^n=1{\left({-1}^{\frac{2}{3}}\right)}^2$$
78	52	sqcli	$$⊢{\left({-1}^{\frac{2}{3}}\right)}^2\in ℂ$$
79	78	mulid2i	$$⊢1{\left({-1}^{\frac{2}{3}}\right)}^2={\left({-1}^{\frac{2}{3}}\right)}^2$$
80	69	simpri	$$⊢{\left({-1}^{\frac{2}{3}}\right)}^2=\frac{-1-\mathrm{i}\sqrt{3}}{2}$$
81	79 80	eqtri	$$⊢1{\left({-1}^{\frac{2}{3}}\right)}^2=\frac{-1-\mathrm{i}\sqrt{3}}{2}$$
82	77 81	eqtrdi	$$⊢n=0+2\to 1{\left({-1}^{\frac{2}{3}}\right)}^n=\frac{-1-\mathrm{i}\sqrt{3}}{2}$$
83	82	eqeq2d	$$⊢n=0+2\to \left(A=1{\left({-1}^{\frac{2}{3}}\right)}^n\leftrightarrow A=\frac{-1-\mathrm{i}\sqrt{3}}{2}\right)$$
84	46 47 48 59 73 83	rextp	$$⊢\exists n\in \left\{0,0+1,0+2\right\}A=1{\left({-1}^{\frac{2}{3}}\right)}^n\leftrightarrow \left(A=1\vee A=\frac{-1+\mathrm{i}\sqrt{3}}{2}\vee A=\frac{-1-\mathrm{i}\sqrt{3}}{2}\right)$$
85	38 45 84	3bitri	$$⊢\exists n\in \left(0\dots 3-1\right)A=1^{\frac{1}{3}}{\left({-1}^{\frac{2}{3}}\right)}^n\leftrightarrow \left(A=1\vee A=\frac{-1+\mathrm{i}\sqrt{3}}{2}\vee A=\frac{-1-\mathrm{i}\sqrt{3}}{2}\right)$$
86	27 28 85	3bitr4g	$$⊢A\in ℂ\to \left(A\in R\leftrightarrow \exists n\in \left(0\dots 3-1\right)A=1^{\frac{1}{3}}{\left({-1}^{\frac{2}{3}}\right)}^n\right)$$
87	26 86	bitr4d	$$⊢A\in ℂ\to \left(A^3=1\leftrightarrow A\in R\right)$$
88	87	pm5.32i	$$⊢\left(A\in ℂ\wedge A^3=1\right)\leftrightarrow \left(A\in ℂ\wedge A\in R\right)$$
89	23 88	bitr4i	$$⊢A\in R\leftrightarrow \left(A\in ℂ\wedge A^3=1\right)$$