Metamath Proof Explorer

Theorem pige3ALT

Description: Alternate proof of pige3 . This proof is based on the geometric observation that a hexagon of unit side length has perimeter 6, which is less than the unit-radius circumcircle, of perimeter 2pi . We translate this to algebra by looking at the function e ^ (i x ) as x goes from 0 to pi / 3 ; it moves at unit speed and travels distance 1 , hence 1 <_ _pi / 3 . (Contributed by Mario Carneiro, 21-May-2016) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion pige3ALT 
|- 3 <_ _pi

Proof

Step Hyp Ref Expression
1 3cn 
 |-  3 e. CC
2 1 mulid2i 
 |-  ( 1 x. 3 ) = 3
3 tru 
 |-  T.
4 0xr 
 |-  0 e. RR*
5 pirp 
 |-  _pi e. RR+
6 3rp 
 |-  3 e. RR+
7 rpdivcl 
 |-  ( ( _pi e. RR+ /\ 3 e. RR+ ) -> ( _pi / 3 ) e. RR+ )
8 5 6 7 mp2an 
 |-  ( _pi / 3 ) e. RR+
9 rpxr 
 |-  ( ( _pi / 3 ) e. RR+ -> ( _pi / 3 ) e. RR* )
10 8 9 ax-mp 
 |-  ( _pi / 3 ) e. RR*
11 rpge0 
 |-  ( ( _pi / 3 ) e. RR+ -> 0 <_ ( _pi / 3 ) )
12 8 11 ax-mp 
 |-  0 <_ ( _pi / 3 )
13 lbicc2 
 |-  ( ( 0 e. RR* /\ ( _pi / 3 ) e. RR* /\ 0 <_ ( _pi / 3 ) ) -> 0 e. ( 0 [,] ( _pi / 3 ) ) )
14 4 10 12 13 mp3an 
 |-  0 e. ( 0 [,] ( _pi / 3 ) )
15 ubicc2 
 |-  ( ( 0 e. RR* /\ ( _pi / 3 ) e. RR* /\ 0 <_ ( _pi / 3 ) ) -> ( _pi / 3 ) e. ( 0 [,] ( _pi / 3 ) ) )
16 4 10 12 15 mp3an 
 |-  ( _pi / 3 ) e. ( 0 [,] ( _pi / 3 ) )
17 14 16 pm3.2i 
 |-  ( 0 e. ( 0 [,] ( _pi / 3 ) ) /\ ( _pi / 3 ) e. ( 0 [,] ( _pi / 3 ) ) )
18 0re 
 |-  0 e. RR
19 18 a1i 
 |-  ( T. -> 0 e. RR )
20 pire 
 |-  _pi e. RR
21 3re 
 |-  3 e. RR
22 3ne0 
 |-  3 =/= 0
23 20 21 22 redivcli 
 |-  ( _pi / 3 ) e. RR
24 23 a1i 
 |-  ( T. -> ( _pi / 3 ) e. RR )
25 efcn 
 |-  exp e. ( CC -cn-> CC )
26 25 a1i 
 |-  ( T. -> exp e. ( CC -cn-> CC ) )
27 iccssre 
 |-  ( ( 0 e. RR /\ ( _pi / 3 ) e. RR ) -> ( 0 [,] ( _pi / 3 ) ) C_ RR )
28 18 23 27 mp2an 
 |-  ( 0 [,] ( _pi / 3 ) ) C_ RR
29 ax-resscn 
 |-  RR C_ CC
30 28 29 sstri 
 |-  ( 0 [,] ( _pi / 3 ) ) C_ CC
31 resmpt 
 |-  ( ( 0 [,] ( _pi / 3 ) ) C_ CC -> ( ( x e. CC |-> ( _i x. x ) ) |` ( 0 [,] ( _pi / 3 ) ) ) = ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( _i x. x ) ) )
32 30 31 mp1i 
 |-  ( T. -> ( ( x e. CC |-> ( _i x. x ) ) |` ( 0 [,] ( _pi / 3 ) ) ) = ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( _i x. x ) ) )
33 ssidd 
 |-  ( T. -> CC C_ CC )
34 ax-icn 
 |-  _i e. CC
35 simpr 
 |-  ( ( T. /\ x e. CC ) -> x e. CC )
36 mulcl 
 |-  ( ( _i e. CC /\ x e. CC ) -> ( _i x. x ) e. CC )
37 34 35 36 sylancr 
 |-  ( ( T. /\ x e. CC ) -> ( _i x. x ) e. CC )
38 37 fmpttd 
 |-  ( T. -> ( x e. CC |-> ( _i x. x ) ) : CC --> CC )
39 cnelprrecn 
 |-  CC e. { RR , CC }
40 39 a1i 
 |-  ( T. -> CC e. { RR , CC } )
41 ax-1cn 
 |-  1 e. CC
42 41 a1i 
 |-  ( ( T. /\ x e. CC ) -> 1 e. CC )
43 40 dvmptid 
 |-  ( T. -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
44 34 a1i 
 |-  ( T. -> _i e. CC )
45 40 35 42 43 44 dvmptcmul 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( _i x. x ) ) ) = ( x e. CC |-> ( _i x. 1 ) ) )
46 34 mulid1i 
 |-  ( _i x. 1 ) = _i
47 46 mpteq2i 
 |-  ( x e. CC |-> ( _i x. 1 ) ) = ( x e. CC |-> _i )
48 45 47 eqtrdi 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( _i x. x ) ) ) = ( x e. CC |-> _i ) )
49 48 dmeqd 
 |-  ( T. -> dom ( CC _D ( x e. CC |-> ( _i x. x ) ) ) = dom ( x e. CC |-> _i ) )
50 34 elexi 
 |-  _i e. _V
51 eqid 
 |-  ( x e. CC |-> _i ) = ( x e. CC |-> _i )
52 50 51 dmmpti 
 |-  dom ( x e. CC |-> _i ) = CC
53 49 52 eqtrdi 
 |-  ( T. -> dom ( CC _D ( x e. CC |-> ( _i x. x ) ) ) = CC )
54 dvcn 
 |-  ( ( ( CC C_ CC /\ ( x e. CC |-> ( _i x. x ) ) : CC --> CC /\ CC C_ CC ) /\ dom ( CC _D ( x e. CC |-> ( _i x. x ) ) ) = CC ) -> ( x e. CC |-> ( _i x. x ) ) e. ( CC -cn-> CC ) )
55 33 38 33 53 54 syl31anc 
 |-  ( T. -> ( x e. CC |-> ( _i x. x ) ) e. ( CC -cn-> CC ) )
56 rescncf 
 |-  ( ( 0 [,] ( _pi / 3 ) ) C_ CC -> ( ( x e. CC |-> ( _i x. x ) ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> ( _i x. x ) ) |` ( 0 [,] ( _pi / 3 ) ) ) e. ( ( 0 [,] ( _pi / 3 ) ) -cn-> CC ) ) )
57 30 55 56 mpsyl 
 |-  ( T. -> ( ( x e. CC |-> ( _i x. x ) ) |` ( 0 [,] ( _pi / 3 ) ) ) e. ( ( 0 [,] ( _pi / 3 ) ) -cn-> CC ) )
58 32 57 eqeltrrd 
 |-  ( T. -> ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( _i x. x ) ) e. ( ( 0 [,] ( _pi / 3 ) ) -cn-> CC ) )
59 26 58 cncfmpt1f 
 |-  ( T. -> ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) e. ( ( 0 [,] ( _pi / 3 ) ) -cn-> CC ) )
60 reelprrecn 
 |-  RR e. { RR , CC }
61 60 a1i 
 |-  ( T. -> RR e. { RR , CC } )
62 recn 
 |-  ( x e. RR -> x e. CC )
63 efcl 
 |-  ( ( _i x. x ) e. CC -> ( exp ` ( _i x. x ) ) e. CC )
64 37 63 syl 
 |-  ( ( T. /\ x e. CC ) -> ( exp ` ( _i x. x ) ) e. CC )
65 62 64 sylan2 
 |-  ( ( T. /\ x e. RR ) -> ( exp ` ( _i x. x ) ) e. CC )
66 mulcl 
 |-  ( ( ( exp ` ( _i x. x ) ) e. CC /\ _i e. CC ) -> ( ( exp ` ( _i x. x ) ) x. _i ) e. CC )
67 64 34 66 sylancl 
 |-  ( ( T. /\ x e. CC ) -> ( ( exp ` ( _i x. x ) ) x. _i ) e. CC )
68 62 67 sylan2 
 |-  ( ( T. /\ x e. RR ) -> ( ( exp ` ( _i x. x ) ) x. _i ) e. CC )
69 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
70 69 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
71 toponmax 
 |-  ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
72 70 71 mp1i 
 |-  ( T. -> CC e. ( TopOpen ` CCfld ) )
73 29 a1i 
 |-  ( T. -> RR C_ CC )
74 df-ss 
 |-  ( RR C_ CC <-> ( RR i^i CC ) = RR )
75 73 74 sylib 
 |-  ( T. -> ( RR i^i CC ) = RR )
76 34 a1i 
 |-  ( ( T. /\ x e. CC ) -> _i e. CC )
77 efcl 
 |-  ( y e. CC -> ( exp ` y ) e. CC )
78 77 adantl 
 |-  ( ( T. /\ y e. CC ) -> ( exp ` y ) e. CC )
79 dvef 
 |-  ( CC _D exp ) = exp
80 eff 
 |-  exp : CC --> CC
81 80 a1i 
 |-  ( T. -> exp : CC --> CC )
82 81 feqmptd 
 |-  ( T. -> exp = ( y e. CC |-> ( exp ` y ) ) )
83 82 oveq2d 
 |-  ( T. -> ( CC _D exp ) = ( CC _D ( y e. CC |-> ( exp ` y ) ) ) )
84 79 83 82 3eqtr3a 
 |-  ( T. -> ( CC _D ( y e. CC |-> ( exp ` y ) ) ) = ( y e. CC |-> ( exp ` y ) ) )
85 fveq2 
 |-  ( y = ( _i x. x ) -> ( exp ` y ) = ( exp ` ( _i x. x ) ) )
86 40 40 37 76 78 78 48 84 85 85 dvmptco 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( exp ` ( _i x. x ) ) ) ) = ( x e. CC |-> ( ( exp ` ( _i x. x ) ) x. _i ) ) )
87 69 61 72 75 64 67 86 dvmptres3 
 |-  ( T. -> ( RR _D ( x e. RR |-> ( exp ` ( _i x. x ) ) ) ) = ( x e. RR |-> ( ( exp ` ( _i x. x ) ) x. _i ) ) )
88 28 a1i 
 |-  ( T. -> ( 0 [,] ( _pi / 3 ) ) C_ RR )
89 69 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
90 iccntr 
 |-  ( ( 0 e. RR /\ ( _pi / 3 ) e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] ( _pi / 3 ) ) ) = ( 0 (,) ( _pi / 3 ) ) )
91 18 24 90 sylancr 
 |-  ( T. -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] ( _pi / 3 ) ) ) = ( 0 (,) ( _pi / 3 ) ) )
92 61 65 68 87 88 89 69 91 dvmptres2 
 |-  ( T. -> ( RR _D ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ) = ( x e. ( 0 (,) ( _pi / 3 ) ) |-> ( ( exp ` ( _i x. x ) ) x. _i ) ) )
93 92 dmeqd 
 |-  ( T. -> dom ( RR _D ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ) = dom ( x e. ( 0 (,) ( _pi / 3 ) ) |-> ( ( exp ` ( _i x. x ) ) x. _i ) ) )
94 ovex 
 |-  ( ( exp ` ( _i x. x ) ) x. _i ) e. _V
95 eqid 
 |-  ( x e. ( 0 (,) ( _pi / 3 ) ) |-> ( ( exp ` ( _i x. x ) ) x. _i ) ) = ( x e. ( 0 (,) ( _pi / 3 ) ) |-> ( ( exp ` ( _i x. x ) ) x. _i ) )
96 94 95 dmmpti 
 |-  dom ( x e. ( 0 (,) ( _pi / 3 ) ) |-> ( ( exp ` ( _i x. x ) ) x. _i ) ) = ( 0 (,) ( _pi / 3 ) )
97 93 96 eqtrdi 
 |-  ( T. -> dom ( RR _D ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ) = ( 0 (,) ( _pi / 3 ) ) )
98 1re 
 |-  1 e. RR
99 98 a1i 
 |-  ( T. -> 1 e. RR )
100 92 fveq1d 
 |-  ( T. -> ( ( RR _D ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ) ` y ) = ( ( x e. ( 0 (,) ( _pi / 3 ) ) |-> ( ( exp ` ( _i x. x ) ) x. _i ) ) ` y ) )
101 oveq2 
 |-  ( x = y -> ( _i x. x ) = ( _i x. y ) )
102 101 fveq2d 
 |-  ( x = y -> ( exp ` ( _i x. x ) ) = ( exp ` ( _i x. y ) ) )
103 102 oveq1d 
 |-  ( x = y -> ( ( exp ` ( _i x. x ) ) x. _i ) = ( ( exp ` ( _i x. y ) ) x. _i ) )
104 103 95 94 fvmpt3i 
 |-  ( y e. ( 0 (,) ( _pi / 3 ) ) -> ( ( x e. ( 0 (,) ( _pi / 3 ) ) |-> ( ( exp ` ( _i x. x ) ) x. _i ) ) ` y ) = ( ( exp ` ( _i x. y ) ) x. _i ) )
105 100 104 sylan9eq 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> ( ( RR _D ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ) ` y ) = ( ( exp ` ( _i x. y ) ) x. _i ) )
106 105 fveq2d 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> ( abs ` ( ( RR _D ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ) ` y ) ) = ( abs ` ( ( exp ` ( _i x. y ) ) x. _i ) ) )
107 ioossre 
 |-  ( 0 (,) ( _pi / 3 ) ) C_ RR
108 107 a1i 
 |-  ( T. -> ( 0 (,) ( _pi / 3 ) ) C_ RR )
109 108 sselda 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> y e. RR )
110 109 recnd 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> y e. CC )
111 mulcl 
 |-  ( ( _i e. CC /\ y e. CC ) -> ( _i x. y ) e. CC )
112 34 110 111 sylancr 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> ( _i x. y ) e. CC )
113 efcl 
 |-  ( ( _i x. y ) e. CC -> ( exp ` ( _i x. y ) ) e. CC )
114 112 113 syl 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> ( exp ` ( _i x. y ) ) e. CC )
115 absmul 
 |-  ( ( ( exp ` ( _i x. y ) ) e. CC /\ _i e. CC ) -> ( abs ` ( ( exp ` ( _i x. y ) ) x. _i ) ) = ( ( abs ` ( exp ` ( _i x. y ) ) ) x. ( abs ` _i ) ) )
116 114 34 115 sylancl 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> ( abs ` ( ( exp ` ( _i x. y ) ) x. _i ) ) = ( ( abs ` ( exp ` ( _i x. y ) ) ) x. ( abs ` _i ) ) )
117 absefi 
 |-  ( y e. RR -> ( abs ` ( exp ` ( _i x. y ) ) ) = 1 )
118 109 117 syl 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> ( abs ` ( exp ` ( _i x. y ) ) ) = 1 )
119 absi 
 |-  ( abs ` _i ) = 1
120 119 a1i 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> ( abs ` _i ) = 1 )
121 118 120 oveq12d 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> ( ( abs ` ( exp ` ( _i x. y ) ) ) x. ( abs ` _i ) ) = ( 1 x. 1 ) )
122 41 mulid1i 
 |-  ( 1 x. 1 ) = 1
123 121 122 eqtrdi 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> ( ( abs ` ( exp ` ( _i x. y ) ) ) x. ( abs ` _i ) ) = 1 )
124 106 116 123 3eqtrd 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> ( abs ` ( ( RR _D ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ) ` y ) ) = 1 )
125 1le1 
 |-  1 <_ 1
126 124 125 eqbrtrdi 
 |-  ( ( T. /\ y e. ( 0 (,) ( _pi / 3 ) ) ) -> ( abs ` ( ( RR _D ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ) ` y ) ) <_ 1 )
127 19 24 59 97 99 126 dvlip 
 |-  ( ( T. /\ ( 0 e. ( 0 [,] ( _pi / 3 ) ) /\ ( _pi / 3 ) e. ( 0 [,] ( _pi / 3 ) ) ) ) -> ( abs ` ( ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` 0 ) - ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` ( _pi / 3 ) ) ) ) <_ ( 1 x. ( abs ` ( 0 - ( _pi / 3 ) ) ) ) )
128 3 17 127 mp2an 
 |-  ( abs ` ( ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` 0 ) - ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` ( _pi / 3 ) ) ) ) <_ ( 1 x. ( abs ` ( 0 - ( _pi / 3 ) ) ) )
129 oveq2 
 |-  ( x = 0 -> ( _i x. x ) = ( _i x. 0 ) )
130 it0e0 
 |-  ( _i x. 0 ) = 0
131 129 130 eqtrdi 
 |-  ( x = 0 -> ( _i x. x ) = 0 )
132 131 fveq2d 
 |-  ( x = 0 -> ( exp ` ( _i x. x ) ) = ( exp ` 0 ) )
133 ef0 
 |-  ( exp ` 0 ) = 1
134 132 133 eqtrdi 
 |-  ( x = 0 -> ( exp ` ( _i x. x ) ) = 1 )
135 eqid 
 |-  ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) = ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) )
136 fvex 
 |-  ( exp ` ( _i x. x ) ) e. _V
137 134 135 136 fvmpt3i 
 |-  ( 0 e. ( 0 [,] ( _pi / 3 ) ) -> ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` 0 ) = 1 )
138 14 137 ax-mp 
 |-  ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` 0 ) = 1
139 oveq2 
 |-  ( x = ( _pi / 3 ) -> ( _i x. x ) = ( _i x. ( _pi / 3 ) ) )
140 139 fveq2d 
 |-  ( x = ( _pi / 3 ) -> ( exp ` ( _i x. x ) ) = ( exp ` ( _i x. ( _pi / 3 ) ) ) )
141 140 135 136 fvmpt3i 
 |-  ( ( _pi / 3 ) e. ( 0 [,] ( _pi / 3 ) ) -> ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` ( _pi / 3 ) ) = ( exp ` ( _i x. ( _pi / 3 ) ) ) )
142 16 141 ax-mp 
 |-  ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` ( _pi / 3 ) ) = ( exp ` ( _i x. ( _pi / 3 ) ) )
143 138 142 oveq12i 
 |-  ( ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` 0 ) - ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` ( _pi / 3 ) ) ) = ( 1 - ( exp ` ( _i x. ( _pi / 3 ) ) ) )
144 23 recni 
 |-  ( _pi / 3 ) e. CC
145 34 144 mulcli 
 |-  ( _i x. ( _pi / 3 ) ) e. CC
146 efcl 
 |-  ( ( _i x. ( _pi / 3 ) ) e. CC -> ( exp ` ( _i x. ( _pi / 3 ) ) ) e. CC )
147 145 146 ax-mp 
 |-  ( exp ` ( _i x. ( _pi / 3 ) ) ) e. CC
148 negicn 
 |-  -u _i e. CC
149 148 144 mulcli 
 |-  ( -u _i x. ( _pi / 3 ) ) e. CC
150 efcl 
 |-  ( ( -u _i x. ( _pi / 3 ) ) e. CC -> ( exp ` ( -u _i x. ( _pi / 3 ) ) ) e. CC )
151 149 150 ax-mp 
 |-  ( exp ` ( -u _i x. ( _pi / 3 ) ) ) e. CC
152 cosval 
 |-  ( ( _pi / 3 ) e. CC -> ( cos ` ( _pi / 3 ) ) = ( ( ( exp ` ( _i x. ( _pi / 3 ) ) ) + ( exp ` ( -u _i x. ( _pi / 3 ) ) ) ) / 2 ) )
153 144 152 ax-mp 
 |-  ( cos ` ( _pi / 3 ) ) = ( ( ( exp ` ( _i x. ( _pi / 3 ) ) ) + ( exp ` ( -u _i x. ( _pi / 3 ) ) ) ) / 2 )
154 sincos3rdpi 
 |-  ( ( sin ` ( _pi / 3 ) ) = ( ( sqrt ` 3 ) / 2 ) /\ ( cos ` ( _pi / 3 ) ) = ( 1 / 2 ) )
155 154 simpri 
 |-  ( cos ` ( _pi / 3 ) ) = ( 1 / 2 )
156 153 155 eqtr3i 
 |-  ( ( ( exp ` ( _i x. ( _pi / 3 ) ) ) + ( exp ` ( -u _i x. ( _pi / 3 ) ) ) ) / 2 ) = ( 1 / 2 )
157 147 151 addcli 
 |-  ( ( exp ` ( _i x. ( _pi / 3 ) ) ) + ( exp ` ( -u _i x. ( _pi / 3 ) ) ) ) e. CC
158 2cn 
 |-  2 e. CC
159 2ne0 
 |-  2 =/= 0
160 157 41 158 159 div11i 
 |-  ( ( ( ( exp ` ( _i x. ( _pi / 3 ) ) ) + ( exp ` ( -u _i x. ( _pi / 3 ) ) ) ) / 2 ) = ( 1 / 2 ) <-> ( ( exp ` ( _i x. ( _pi / 3 ) ) ) + ( exp ` ( -u _i x. ( _pi / 3 ) ) ) ) = 1 )
161 156 160 mpbi 
 |-  ( ( exp ` ( _i x. ( _pi / 3 ) ) ) + ( exp ` ( -u _i x. ( _pi / 3 ) ) ) ) = 1
162 41 147 151 161 subaddrii 
 |-  ( 1 - ( exp ` ( _i x. ( _pi / 3 ) ) ) ) = ( exp ` ( -u _i x. ( _pi / 3 ) ) )
163 mulneg12 
 |-  ( ( _i e. CC /\ ( _pi / 3 ) e. CC ) -> ( -u _i x. ( _pi / 3 ) ) = ( _i x. -u ( _pi / 3 ) ) )
164 34 144 163 mp2an 
 |-  ( -u _i x. ( _pi / 3 ) ) = ( _i x. -u ( _pi / 3 ) )
165 164 fveq2i 
 |-  ( exp ` ( -u _i x. ( _pi / 3 ) ) ) = ( exp ` ( _i x. -u ( _pi / 3 ) ) )
166 143 162 165 3eqtri 
 |-  ( ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` 0 ) - ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` ( _pi / 3 ) ) ) = ( exp ` ( _i x. -u ( _pi / 3 ) ) )
167 166 fveq2i 
 |-  ( abs ` ( ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` 0 ) - ( ( x e. ( 0 [,] ( _pi / 3 ) ) |-> ( exp ` ( _i x. x ) ) ) ` ( _pi / 3 ) ) ) ) = ( abs ` ( exp ` ( _i x. -u ( _pi / 3 ) ) ) )
168 144 absnegi 
 |-  ( abs ` -u ( _pi / 3 ) ) = ( abs ` ( _pi / 3 ) )
169 df-neg 
 |-  -u ( _pi / 3 ) = ( 0 - ( _pi / 3 ) )
170 169 fveq2i 
 |-  ( abs ` -u ( _pi / 3 ) ) = ( abs ` ( 0 - ( _pi / 3 ) ) )
171 168 170 eqtr3i 
 |-  ( abs ` ( _pi / 3 ) ) = ( abs ` ( 0 - ( _pi / 3 ) ) )
172 rprege0 
 |-  ( ( _pi / 3 ) e. RR+ -> ( ( _pi / 3 ) e. RR /\ 0 <_ ( _pi / 3 ) ) )
173 absid 
 |-  ( ( ( _pi / 3 ) e. RR /\ 0 <_ ( _pi / 3 ) ) -> ( abs ` ( _pi / 3 ) ) = ( _pi / 3 ) )
174 8 172 173 mp2b 
 |-  ( abs ` ( _pi / 3 ) ) = ( _pi / 3 )
175 171 174 eqtr3i 
 |-  ( abs ` ( 0 - ( _pi / 3 ) ) ) = ( _pi / 3 )
176 175 oveq2i 
 |-  ( 1 x. ( abs ` ( 0 - ( _pi / 3 ) ) ) ) = ( 1 x. ( _pi / 3 ) )
177 128 167 176 3brtr3i 
 |-  ( abs ` ( exp ` ( _i x. -u ( _pi / 3 ) ) ) ) <_ ( 1 x. ( _pi / 3 ) )
178 23 renegcli 
 |-  -u ( _pi / 3 ) e. RR
179 absefi 
 |-  ( -u ( _pi / 3 ) e. RR -> ( abs ` ( exp ` ( _i x. -u ( _pi / 3 ) ) ) ) = 1 )
180 178 179 ax-mp 
 |-  ( abs ` ( exp ` ( _i x. -u ( _pi / 3 ) ) ) ) = 1
181 144 mulid2i 
 |-  ( 1 x. ( _pi / 3 ) ) = ( _pi / 3 )
182 177 180 181 3brtr3i 
 |-  1 <_ ( _pi / 3 )
183 3pos 
 |-  0 < 3
184 21 183 pm3.2i 
 |-  ( 3 e. RR /\ 0 < 3 )
185 lemuldiv 
 |-  ( ( 1 e. RR /\ _pi e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( ( 1 x. 3 ) <_ _pi <-> 1 <_ ( _pi / 3 ) ) )
186 98 20 184 185 mp3an 
 |-  ( ( 1 x. 3 ) <_ _pi <-> 1 <_ ( _pi / 3 ) )
187 182 186 mpbir 
 |-  ( 1 x. 3 ) <_ _pi
188 2 187 eqbrtrri 
 |-  3 <_ _pi