Metamath Proof Explorer

Theorem 1cubr

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

Ref Expression
Hypothesis 1cubr.r 
|- R = { 1 , ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) , ( ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) / 2 ) }
Assertion 1cubr 
|- ( A e. R <-> ( A e. CC /\ ( A ^ 3 ) = 1 ) )

Proof

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