Metamath Proof Explorer

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 addid2i ⊢ ( 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 addid2i ⊢ ( 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 mulid2i ⊢ ( 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 mulid2i ⊢ ( 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 ) )