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 ≤ π

Proof

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