Theorem 1cubr

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

	Ref	Expression
Hypothesis	1cubr.r	⊢ 𝑅 = { 1 , ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) , ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) }
Assertion	1cubr	⊢ ( 𝐴 ∈ 𝑅 ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 3 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		1cubr.r	⊢ 𝑅 = { 1 , ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) , ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) }
2		ax-1cn	⊢ 1 ∈ ℂ
3		neg1cn	⊢ - 1 ∈ ℂ
4		ax-icn	⊢ i ∈ ℂ
5		3cn	⊢ 3 ∈ ℂ
6		sqrtcl	⊢ ( 3 ∈ ℂ → ( √ ‘ 3 ) ∈ ℂ )
7	5 6	ax-mp	⊢ ( √ ‘ 3 ) ∈ ℂ
8	4 7	mulcli	⊢ ( i · ( √ ‘ 3 ) ) ∈ ℂ
9	3 8	addcli	⊢ ( - 1 + ( i · ( √ ‘ 3 ) ) ) ∈ ℂ
10		halfcl	⊢ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) ∈ ℂ → ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ∈ ℂ )
11	9 10	ax-mp	⊢ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ∈ ℂ
12	3 8	subcli	⊢ ( - 1 − ( i · ( √ ‘ 3 ) ) ) ∈ ℂ
13		halfcl	⊢ ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) ∈ ℂ → ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) ∈ ℂ )
14	12 13	ax-mp	⊢ ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) ∈ ℂ
15	2 11 14	3pm3.2i	⊢ ( 1 ∈ ℂ ∧ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ∈ ℂ ∧ ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) ∈ ℂ )
16	2	elexi	⊢ 1 ∈ V
17		ovex	⊢ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ∈ V
18		ovex	⊢ ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) ∈ V
19	16 17 18	tpss	⊢ ( ( 1 ∈ ℂ ∧ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ∈ ℂ ∧ ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) ∈ ℂ ) ↔ { 1 , ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) , ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) } ⊆ ℂ )
20	15 19	mpbi	⊢ { 1 , ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) , ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) } ⊆ ℂ
21	1 20	eqsstri	⊢ 𝑅 ⊆ ℂ
22	21	sseli	⊢ ( 𝐴 ∈ 𝑅 → 𝐴 ∈ ℂ )
23	22	pm4.71ri	⊢ ( 𝐴 ∈ 𝑅 ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ 𝑅 ) )
24		3nn	⊢ 3 ∈ ℕ
25		cxpeq	⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℕ ∧ 1 ∈ ℂ ) → ( ( 𝐴 ↑ 3 ) = 1 ↔ ∃ 𝑛 ∈ ( 0 ... ( 3 − 1 ) ) 𝐴 = ( ( 1 ↑𝑐 ( 1 / 3 ) ) · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) ) )
26	24 2 25	mp3an23	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 3 ) = 1 ↔ ∃ 𝑛 ∈ ( 0 ... ( 3 − 1 ) ) 𝐴 = ( ( 1 ↑𝑐 ( 1 / 3 ) ) · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) ) )
27		eltpg	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ { 1 , ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) , ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) } ↔ ( 𝐴 = 1 ∨ 𝐴 = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ∨ 𝐴 = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) ) ) )
28	1	eleq2i	⊢ ( 𝐴 ∈ 𝑅 ↔ 𝐴 ∈ { 1 , ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) , ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) } )
29		3m1e2	⊢ ( 3 − 1 ) = 2
30		2cn	⊢ 2 ∈ ℂ
31	30	addlidi	⊢ ( 0 + 2 ) = 2
32	29 31	eqtr4i	⊢ ( 3 − 1 ) = ( 0 + 2 )
33	32	oveq2i	⊢ ( 0 ... ( 3 − 1 ) ) = ( 0 ... ( 0 + 2 ) )
34		0z	⊢ 0 ∈ ℤ
35		fztp	⊢ ( 0 ∈ ℤ → ( 0 ... ( 0 + 2 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) } )
36	34 35	ax-mp	⊢ ( 0 ... ( 0 + 2 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) }
37	33 36	eqtri	⊢ ( 0 ... ( 3 − 1 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) }
38	37	rexeqi	⊢ ( ∃ 𝑛 ∈ ( 0 ... ( 3 − 1 ) ) 𝐴 = ( ( 1 ↑𝑐 ( 1 / 3 ) ) · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) ↔ ∃ 𝑛 ∈ { 0 , ( 0 + 1 ) , ( 0 + 2 ) } 𝐴 = ( ( 1 ↑𝑐 ( 1 / 3 ) ) · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) )
39		3ne0	⊢ 3 ≠ 0
40	5 39	reccli	⊢ ( 1 / 3 ) ∈ ℂ
41		1cxp	⊢ ( ( 1 / 3 ) ∈ ℂ → ( 1 ↑𝑐 ( 1 / 3 ) ) = 1 )
42	40 41	ax-mp	⊢ ( 1 ↑𝑐 ( 1 / 3 ) ) = 1
43	42	oveq1i	⊢ ( ( 1 ↑𝑐 ( 1 / 3 ) ) · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) = ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) )
44	43	eqeq2i	⊢ ( 𝐴 = ( ( 1 ↑𝑐 ( 1 / 3 ) ) · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) ↔ 𝐴 = ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) )
45	44	rexbii	⊢ ( ∃ 𝑛 ∈ { 0 , ( 0 + 1 ) , ( 0 + 2 ) } 𝐴 = ( ( 1 ↑𝑐 ( 1 / 3 ) ) · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) ↔ ∃ 𝑛 ∈ { 0 , ( 0 + 1 ) , ( 0 + 2 ) } 𝐴 = ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) )
46	34	elexi	⊢ 0 ∈ V
47		ovex	⊢ ( 0 + 1 ) ∈ V
48		ovex	⊢ ( 0 + 2 ) ∈ V
49		oveq2	⊢ ( 𝑛 = 0 → ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) = ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 0 ) )
50	30 5 39	divcli	⊢ ( 2 / 3 ) ∈ ℂ
51		cxpcl	⊢ ( ( - 1 ∈ ℂ ∧ ( 2 / 3 ) ∈ ℂ ) → ( - 1 ↑𝑐 ( 2 / 3 ) ) ∈ ℂ )
52	3 50 51	mp2an	⊢ ( - 1 ↑𝑐 ( 2 / 3 ) ) ∈ ℂ
53		exp0	⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ∈ ℂ → ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 0 ) = 1 )
54	52 53	ax-mp	⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 0 ) = 1
55	49 54	eqtrdi	⊢ ( 𝑛 = 0 → ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) = 1 )
56	55	oveq2d	⊢ ( 𝑛 = 0 → ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) = ( 1 · 1 ) )
57		1t1e1	⊢ ( 1 · 1 ) = 1
58	56 57	eqtrdi	⊢ ( 𝑛 = 0 → ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) = 1 )
59	58	eqeq2d	⊢ ( 𝑛 = 0 → ( 𝐴 = ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) ↔ 𝐴 = 1 ) )
60		id	⊢ ( 𝑛 = ( 0 + 1 ) → 𝑛 = ( 0 + 1 ) )
61	2	addlidi	⊢ ( 0 + 1 ) = 1
62	60 61	eqtrdi	⊢ ( 𝑛 = ( 0 + 1 ) → 𝑛 = 1 )
63	62	oveq2d	⊢ ( 𝑛 = ( 0 + 1 ) → ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) = ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) )
64		exp1	⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ∈ ℂ → ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) = ( - 1 ↑𝑐 ( 2 / 3 ) ) )
65	52 64	ax-mp	⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) = ( - 1 ↑𝑐 ( 2 / 3 ) )
66	63 65	eqtrdi	⊢ ( 𝑛 = ( 0 + 1 ) → ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) = ( - 1 ↑𝑐 ( 2 / 3 ) ) )
67	66	oveq2d	⊢ ( 𝑛 = ( 0 + 1 ) → ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) = ( 1 · ( - 1 ↑𝑐 ( 2 / 3 ) ) ) )
68	52	mullidi	⊢ ( 1 · ( - 1 ↑𝑐 ( 2 / 3 ) ) ) = ( - 1 ↑𝑐 ( 2 / 3 ) )
69		1cubrlem	⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ∧ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 ) = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) )
70	69	simpli	⊢ ( - 1 ↑𝑐 ( 2 / 3 ) ) = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 )
71	68 70	eqtri	⊢ ( 1 · ( - 1 ↑𝑐 ( 2 / 3 ) ) ) = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 )
72	67 71	eqtrdi	⊢ ( 𝑛 = ( 0 + 1 ) → ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) )
73	72	eqeq2d	⊢ ( 𝑛 = ( 0 + 1 ) → ( 𝐴 = ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) ↔ 𝐴 = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ) )
74		id	⊢ ( 𝑛 = ( 0 + 2 ) → 𝑛 = ( 0 + 2 ) )
75	74 31	eqtrdi	⊢ ( 𝑛 = ( 0 + 2 ) → 𝑛 = 2 )
76	75	oveq2d	⊢ ( 𝑛 = ( 0 + 2 ) → ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) = ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 ) )
77	76	oveq2d	⊢ ( 𝑛 = ( 0 + 2 ) → ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) = ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 ) ) )
78	52	sqcli	⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 ) ∈ ℂ
79	78	mullidi	⊢ ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 ) ) = ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 )
80	69	simpri	⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 ) = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 )
81	79 80	eqtri	⊢ ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 ) ) = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 )
82	77 81	eqtrdi	⊢ ( 𝑛 = ( 0 + 2 ) → ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) )
83	82	eqeq2d	⊢ ( 𝑛 = ( 0 + 2 ) → ( 𝐴 = ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) ↔ 𝐴 = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) ) )
84	46 47 48 59 73 83	rextp	⊢ ( ∃ 𝑛 ∈ { 0 , ( 0 + 1 ) , ( 0 + 2 ) } 𝐴 = ( 1 · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) ↔ ( 𝐴 = 1 ∨ 𝐴 = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ∨ 𝐴 = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) ) )
85	38 45 84	3bitri	⊢ ( ∃ 𝑛 ∈ ( 0 ... ( 3 − 1 ) ) 𝐴 = ( ( 1 ↑𝑐 ( 1 / 3 ) ) · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) ↔ ( 𝐴 = 1 ∨ 𝐴 = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ∨ 𝐴 = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) ) )
86	27 28 85	3bitr4g	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ 𝑅 ↔ ∃ 𝑛 ∈ ( 0 ... ( 3 − 1 ) ) 𝐴 = ( ( 1 ↑𝑐 ( 1 / 3 ) ) · ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 𝑛 ) ) ) )
87	26 86	bitr4d	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 3 ) = 1 ↔ 𝐴 ∈ 𝑅 ) )
88	87	pm5.32i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 3 ) = 1 ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ 𝑅 ) )
89	23 88	bitr4i	⊢ ( 𝐴 ∈ 𝑅 ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 3 ) = 1 ) )