Step | Hyp | Ref
| Expression |
1 | | 3cn 12054 |
. . 3
⊢ 3 ∈
ℂ |
2 | 1 | mulid2i 10981 |
. 2
⊢ (1
· 3) = 3 |
3 | | tru 1546 |
. . . . . 6
⊢
⊤ |
4 | | 0xr 11023 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
5 | | pirp 25616 |
. . . . . . . . . 10
⊢ π
∈ ℝ+ |
6 | | 3rp 12735 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ+ |
7 | | rpdivcl 12754 |
. . . . . . . . . 10
⊢ ((π
∈ ℝ+ ∧ 3 ∈ ℝ+) → (π /
3) ∈ ℝ+) |
8 | 5, 6, 7 | mp2an 689 |
. . . . . . . . 9
⊢ (π /
3) ∈ ℝ+ |
9 | | rpxr 12738 |
. . . . . . . . 9
⊢ ((π /
3) ∈ ℝ+ → (π / 3) ∈
ℝ*) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢ (π /
3) ∈ ℝ* |
11 | | rpge0 12742 |
. . . . . . . . 9
⊢ ((π /
3) ∈ ℝ+ → 0 ≤ (π / 3)) |
12 | 8, 11 | ax-mp 5 |
. . . . . . . 8
⊢ 0 ≤
(π / 3) |
13 | | lbicc2 13195 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ (π / 3) ∈ ℝ* ∧ 0
≤ (π / 3)) → 0 ∈ (0[,](π / 3))) |
14 | 4, 10, 12, 13 | mp3an 1460 |
. . . . . . 7
⊢ 0 ∈
(0[,](π / 3)) |
15 | | ubicc2 13196 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ (π / 3) ∈ ℝ* ∧ 0
≤ (π / 3)) → (π / 3) ∈ (0[,](π / 3))) |
16 | 4, 10, 12, 15 | mp3an 1460 |
. . . . . . 7
⊢ (π /
3) ∈ (0[,](π / 3)) |
17 | 14, 16 | pm3.2i 471 |
. . . . . 6
⊢ (0 ∈
(0[,](π / 3)) ∧ (π / 3) ∈ (0[,](π / 3))) |
18 | | 0re 10978 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
19 | 18 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 0 ∈ ℝ) |
20 | | pire 25613 |
. . . . . . . . 9
⊢ π
∈ ℝ |
21 | | 3re 12053 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
22 | | 3ne0 12079 |
. . . . . . . . 9
⊢ 3 ≠
0 |
23 | 20, 21, 22 | redivcli 11742 |
. . . . . . . 8
⊢ (π /
3) ∈ ℝ |
24 | 23 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (π / 3) ∈ ℝ) |
25 | | efcn 25600 |
. . . . . . . . 9
⊢ exp
∈ (ℂ–cn→ℂ) |
26 | 25 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ exp ∈ (ℂ–cn→ℂ)) |
27 | | iccssre 13160 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ (π / 3) ∈ ℝ) → (0[,](π / 3)) ⊆
ℝ) |
28 | 18, 23, 27 | mp2an 689 |
. . . . . . . . . . 11
⊢
(0[,](π / 3)) ⊆ ℝ |
29 | | ax-resscn 10929 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
30 | 28, 29 | sstri 3935 |
. . . . . . . . . 10
⊢
(0[,](π / 3)) ⊆ ℂ |
31 | | resmpt 5944 |
. . . . . . . . . 10
⊢
((0[,](π / 3)) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ↾ (0[,](π / 3))) =
(𝑥 ∈ (0[,](π / 3))
↦ (i · 𝑥))) |
32 | 30, 31 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑥 ∈ ℂ
↦ (i · 𝑥))
↾ (0[,](π / 3))) = (𝑥 ∈ (0[,](π / 3)) ↦ (i ·
𝑥))) |
33 | | ssidd 3949 |
. . . . . . . . . . 11
⊢ (⊤
→ ℂ ⊆ ℂ) |
34 | | ax-icn 10931 |
. . . . . . . . . . . . 13
⊢ i ∈
ℂ |
35 | | simpr 485 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 𝑥
∈ ℂ) |
36 | | mulcl 10956 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
37 | 34, 35, 36 | sylancr 587 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
38 | 37 | fmpttd 6986 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ (i · 𝑥)):ℂ⟶ℂ) |
39 | | cnelprrecn 10965 |
. . . . . . . . . . . . . . . 16
⊢ ℂ
∈ {ℝ, ℂ} |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
41 | | ax-1cn 10930 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 1 ∈ ℂ) |
43 | 40 | dvmptid 25119 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 𝑥)) =
(𝑥 ∈ ℂ ↦
1)) |
44 | 34 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ i ∈ ℂ) |
45 | 40, 35, 42, 43, 44 | dvmptcmul 25126 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ (i ·
1))) |
46 | 34 | mulid1i 10980 |
. . . . . . . . . . . . . . 15
⊢ (i
· 1) = i |
47 | 46 | mpteq2i 5184 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ ↦ (i
· 1)) = (𝑥 ∈
ℂ ↦ i) |
48 | 45, 47 | eqtrdi 2796 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ i)) |
49 | 48 | dmeqd 5813 |
. . . . . . . . . . . 12
⊢ (⊤
→ dom (ℂ D (𝑥
∈ ℂ ↦ (i · 𝑥))) = dom (𝑥 ∈ ℂ ↦ i)) |
50 | 34 | elexi 3450 |
. . . . . . . . . . . . 13
⊢ i ∈
V |
51 | | eqid 2740 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ ↦ i) =
(𝑥 ∈ ℂ ↦
i) |
52 | 50, 51 | dmmpti 6575 |
. . . . . . . . . . . 12
⊢ dom
(𝑥 ∈ ℂ ↦
i) = ℂ |
53 | 49, 52 | eqtrdi 2796 |
. . . . . . . . . . 11
⊢ (⊤
→ dom (ℂ D (𝑥
∈ ℂ ↦ (i · 𝑥))) = ℂ) |
54 | | dvcn 25083 |
. . . . . . . . . . 11
⊢
(((ℂ ⊆ ℂ ∧ (𝑥 ∈ ℂ ↦ (i · 𝑥)):ℂ⟶ℂ ∧
ℂ ⊆ ℂ) ∧ dom (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = ℂ) → (𝑥 ∈ ℂ ↦ (i
· 𝑥)) ∈
(ℂ–cn→ℂ)) |
55 | 33, 38, 33, 53, 54 | syl31anc 1372 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ (i · 𝑥))
∈ (ℂ–cn→ℂ)) |
56 | | rescncf 24058 |
. . . . . . . . . 10
⊢
((0[,](π / 3)) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ↾ (0[,](π / 3)))
∈ ((0[,](π / 3))–cn→ℂ))) |
57 | 30, 55, 56 | mpsyl 68 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑥 ∈ ℂ
↦ (i · 𝑥))
↾ (0[,](π / 3))) ∈ ((0[,](π / 3))–cn→ℂ)) |
58 | 32, 57 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈ (0[,](π
/ 3)) ↦ (i · 𝑥)) ∈ ((0[,](π / 3))–cn→ℂ)) |
59 | 26, 58 | cncfmpt1f 24075 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈ (0[,](π
/ 3)) ↦ (exp‘(i · 𝑥))) ∈ ((0[,](π / 3))–cn→ℂ)) |
60 | | reelprrecn 10964 |
. . . . . . . . . . 11
⊢ ℝ
∈ {ℝ, ℂ} |
61 | 60 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
62 | | recn 10962 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
63 | | efcl 15790 |
. . . . . . . . . . . 12
⊢ ((i
· 𝑥) ∈ ℂ
→ (exp‘(i · 𝑥)) ∈ ℂ) |
64 | 37, 63 | syl 17 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (exp‘(i · 𝑥)) ∈ ℂ) |
65 | 62, 64 | sylan2 593 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (exp‘(i · 𝑥)) ∈ ℂ) |
66 | | mulcl 10956 |
. . . . . . . . . . . 12
⊢
(((exp‘(i · 𝑥)) ∈ ℂ ∧ i ∈ ℂ)
→ ((exp‘(i · 𝑥)) · i) ∈
ℂ) |
67 | 64, 34, 66 | sylancl 586 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → ((exp‘(i · 𝑥)) · i) ∈
ℂ) |
68 | 62, 67 | sylan2 593 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ) → ((exp‘(i · 𝑥)) · i) ∈
ℂ) |
69 | | eqid 2740 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
70 | 69 | cnfldtopon 23944 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
71 | | toponmax 22073 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) |
72 | 70, 71 | mp1i 13 |
. . . . . . . . . . 11
⊢ (⊤
→ ℂ ∈ (TopOpen‘ℂfld)) |
73 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ℝ ⊆ ℂ) |
74 | | df-ss 3909 |
. . . . . . . . . . . 12
⊢ (ℝ
⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ) |
75 | 73, 74 | sylib 217 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℝ ∩ ℂ) = ℝ) |
76 | 34 | a1i 11 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℂ) → i ∈ ℂ) |
77 | | efcl 15790 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ →
(exp‘𝑦) ∈
ℂ) |
78 | 77 | adantl 482 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑦
∈ ℂ) → (exp‘𝑦) ∈ ℂ) |
79 | | dvef 25142 |
. . . . . . . . . . . . 13
⊢ (ℂ
D exp) = exp |
80 | | eff 15789 |
. . . . . . . . . . . . . . . 16
⊢
exp:ℂ⟶ℂ |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ exp:ℂ⟶ℂ) |
82 | 81 | feqmptd 6834 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ exp = (𝑦 ∈
ℂ ↦ (exp‘𝑦))) |
83 | 82 | oveq2d 7287 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D exp) = (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦)))) |
84 | 79, 83, 82 | 3eqtr3a 2804 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦))) |
85 | | fveq2 6771 |
. . . . . . . . . . . 12
⊢ (𝑦 = (i · 𝑥) → (exp‘𝑦) = (exp‘(i · 𝑥))) |
86 | 40, 40, 37, 76, 78, 78, 48, 84, 85, 85 | dvmptco 25134 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((exp‘(i
· 𝑥)) ·
i))) |
87 | 69, 61, 72, 75, 64, 67, 86 | dvmptres3 25118 |
. . . . . . . . . 10
⊢ (⊤
→ (ℝ D (𝑥 ∈
ℝ ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ ℝ ↦ ((exp‘(i
· 𝑥)) ·
i))) |
88 | 28 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (0[,](π / 3)) ⊆ ℝ) |
89 | 69 | tgioo2 23964 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
90 | | iccntr 23982 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ (π / 3) ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(0[,](π / 3))) = (0(,)(π /
3))) |
91 | 18, 24, 90 | sylancr 587 |
. . . . . . . . . 10
⊢ (⊤
→ ((int‘(topGen‘ran (,)))‘(0[,](π / 3))) = (0(,)(π
/ 3))) |
92 | 61, 65, 68, 87, 88, 89, 69, 91 | dvmptres2 25124 |
. . . . . . . . 9
⊢ (⊤
→ (ℝ D (𝑥 ∈
(0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i))) |
93 | 92 | dmeqd 5813 |
. . . . . . . 8
⊢ (⊤
→ dom (ℝ D (𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = dom (𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i))) |
94 | | ovex 7304 |
. . . . . . . . 9
⊢
((exp‘(i · 𝑥)) · i) ∈ V |
95 | | eqid 2740 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i)) = (𝑥 ∈
(0(,)(π / 3)) ↦ ((exp‘(i · 𝑥)) · i)) |
96 | 94, 95 | dmmpti 6575 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ (0(,)(π / 3))
↦ ((exp‘(i · 𝑥)) · i)) = (0(,)(π /
3)) |
97 | 93, 96 | eqtrdi 2796 |
. . . . . . 7
⊢ (⊤
→ dom (ℝ D (𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = (0(,)(π / 3))) |
98 | | 1re 10976 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
99 | 98 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 1 ∈ ℝ) |
100 | 92 | fveq1d 6773 |
. . . . . . . . . . 11
⊢ (⊤
→ ((ℝ D (𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥))))‘𝑦) = ((𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i))‘𝑦)) |
101 | | oveq2 7279 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (i · 𝑥) = (i · 𝑦)) |
102 | 101 | fveq2d 6775 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (exp‘(i · 𝑥)) = (exp‘(i ·
𝑦))) |
103 | 102 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((exp‘(i · 𝑥)) · i) = ((exp‘(i
· 𝑦)) ·
i)) |
104 | 103, 95, 94 | fvmpt3i 6877 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0(,)(π / 3)) →
((𝑥 ∈ (0(,)(π / 3))
↦ ((exp‘(i · 𝑥)) · i))‘𝑦) = ((exp‘(i · 𝑦)) · i)) |
105 | 100, 104 | sylan9eq 2800 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → ((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦) = ((exp‘(i · 𝑦)) · i)) |
106 | 105 | fveq2d 6775 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦)) = (abs‘((exp‘(i · 𝑦)) ·
i))) |
107 | | ioossre 13139 |
. . . . . . . . . . . . . . 15
⊢
(0(,)(π / 3)) ⊆ ℝ |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (0(,)(π / 3)) ⊆ ℝ) |
109 | 108 | sselda 3926 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → 𝑦 ∈ ℝ) |
110 | 109 | recnd 11004 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → 𝑦 ∈ ℂ) |
111 | | mulcl 10956 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ 𝑦
∈ ℂ) → (i · 𝑦) ∈ ℂ) |
112 | 34, 110, 111 | sylancr 587 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (i · 𝑦) ∈ ℂ) |
113 | | efcl 15790 |
. . . . . . . . . . 11
⊢ ((i
· 𝑦) ∈ ℂ
→ (exp‘(i · 𝑦)) ∈ ℂ) |
114 | 112, 113 | syl 17 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (exp‘(i · 𝑦)) ∈ ℂ) |
115 | | absmul 15004 |
. . . . . . . . . 10
⊢
(((exp‘(i · 𝑦)) ∈ ℂ ∧ i ∈ ℂ)
→ (abs‘((exp‘(i · 𝑦)) · i)) = ((abs‘(exp‘(i
· 𝑦))) ·
(abs‘i))) |
116 | 114, 34, 115 | sylancl 586 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘((exp‘(i · 𝑦)) · i)) =
((abs‘(exp‘(i · 𝑦))) · (abs‘i))) |
117 | | absefi 15903 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ →
(abs‘(exp‘(i · 𝑦))) = 1) |
118 | 109, 117 | syl 17 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘(exp‘(i · 𝑦))) = 1) |
119 | | absi 14996 |
. . . . . . . . . . . 12
⊢
(abs‘i) = 1 |
120 | 119 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘i) = 1) |
121 | 118, 120 | oveq12d 7289 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → ((abs‘(exp‘(i · 𝑦))) · (abs‘i)) = (1
· 1)) |
122 | 41 | mulid1i 10980 |
. . . . . . . . . 10
⊢ (1
· 1) = 1 |
123 | 121, 122 | eqtrdi 2796 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → ((abs‘(exp‘(i · 𝑦))) · (abs‘i)) =
1) |
124 | 106, 116,
123 | 3eqtrd 2784 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦)) = 1) |
125 | | 1le1 11603 |
. . . . . . . 8
⊢ 1 ≤
1 |
126 | 124, 125 | eqbrtrdi 5118 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦)) ≤ 1) |
127 | 19, 24, 59, 97, 99, 126 | dvlip 25155 |
. . . . . 6
⊢
((⊤ ∧ (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 689 |
. . . . 5
⊢
(abs‘(((𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3)))) ≤ (1 ·
(abs‘(0 − (π / 3)))) |
129 | | oveq2 7279 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → (i · 𝑥) = (i ·
0)) |
130 | | it0e0 12195 |
. . . . . . . . . . . . 13
⊢ (i
· 0) = 0 |
131 | 129, 130 | eqtrdi 2796 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (i · 𝑥) = 0) |
132 | 131 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (exp‘(i
· 𝑥)) =
(exp‘0)) |
133 | | ef0 15798 |
. . . . . . . . . . 11
⊢
(exp‘0) = 1 |
134 | 132, 133 | eqtrdi 2796 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (exp‘(i
· 𝑥)) =
1) |
135 | | eqid 2740 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))
= (𝑥 ∈ (0[,](π /
3)) ↦ (exp‘(i · 𝑥))) |
136 | | fvex 6784 |
. . . . . . . . . 10
⊢
(exp‘(i · 𝑥)) ∈ V |
137 | 134, 135,
136 | fvmpt3i 6877 |
. . . . . . . . 9
⊢ (0 ∈
(0[,](π / 3)) → ((𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) = 1) |
138 | 14, 137 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘0) = 1 |
139 | | oveq2 7279 |
. . . . . . . . . . 11
⊢ (𝑥 = (π / 3) → (i ·
𝑥) = (i · (π /
3))) |
140 | 139 | fveq2d 6775 |
. . . . . . . . . 10
⊢ (𝑥 = (π / 3) →
(exp‘(i · 𝑥))
= (exp‘(i · (π / 3)))) |
141 | 140, 135,
136 | fvmpt3i 6877 |
. . . . . . . . 9
⊢ ((π /
3) ∈ (0[,](π / 3)) → ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3)) = (exp‘(i
· (π / 3)))) |
142 | 16, 141 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3)) = (exp‘(i
· (π / 3))) |
143 | 138, 142 | oveq12i 7283 |
. . . . . . 7
⊢ (((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3))) = (1 −
(exp‘(i · (π / 3)))) |
144 | 23 | recni 10990 |
. . . . . . . . . 10
⊢ (π /
3) ∈ ℂ |
145 | 34, 144 | mulcli 10983 |
. . . . . . . . 9
⊢ (i
· (π / 3)) ∈ ℂ |
146 | | efcl 15790 |
. . . . . . . . 9
⊢ ((i
· (π / 3)) ∈ ℂ → (exp‘(i · (π / 3)))
∈ ℂ) |
147 | 145, 146 | ax-mp 5 |
. . . . . . . 8
⊢
(exp‘(i · (π / 3))) ∈ ℂ |
148 | | negicn 11222 |
. . . . . . . . . 10
⊢ -i ∈
ℂ |
149 | 148, 144 | mulcli 10983 |
. . . . . . . . 9
⊢ (-i
· (π / 3)) ∈ ℂ |
150 | | efcl 15790 |
. . . . . . . . 9
⊢ ((-i
· (π / 3)) ∈ ℂ → (exp‘(-i · (π / 3)))
∈ ℂ) |
151 | 149, 150 | ax-mp 5 |
. . . . . . . 8
⊢
(exp‘(-i · (π / 3))) ∈ ℂ |
152 | | cosval 15830 |
. . . . . . . . . . 11
⊢ ((π /
3) ∈ ℂ → (cos‘(π / 3)) = (((exp‘(i ·
(π / 3))) + (exp‘(-i · (π / 3)))) / 2)) |
153 | 144, 152 | ax-mp 5 |
. . . . . . . . . 10
⊢
(cos‘(π / 3)) = (((exp‘(i · (π / 3))) +
(exp‘(-i · (π / 3)))) / 2) |
154 | | sincos3rdpi 25671 |
. . . . . . . . . . 11
⊢
((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π
/ 3)) = (1 / 2)) |
155 | 154 | simpri 486 |
. . . . . . . . . 10
⊢
(cos‘(π / 3)) = (1 / 2) |
156 | 153, 155 | eqtr3i 2770 |
. . . . . . . . 9
⊢
(((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) / 2) = (1 / 2) |
157 | 147, 151 | addcli 10982 |
. . . . . . . . . 10
⊢
((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) ∈ ℂ |
158 | | 2cn 12048 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
159 | | 2ne0 12077 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
160 | 157, 41, 158, 159 | div11i 11734 |
. . . . . . . . 9
⊢
((((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) / 2) = (1 / 2) ↔ ((exp‘(i · (π / 3))) +
(exp‘(-i · (π / 3)))) = 1) |
161 | 156, 160 | mpbi 229 |
. . . . . . . 8
⊢
((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) = 1 |
162 | 41, 147, 151, 161 | subaddrii 11310 |
. . . . . . 7
⊢ (1
− (exp‘(i · (π / 3)))) = (exp‘(-i · (π /
3))) |
163 | | mulneg12 11413 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ (π / 3) ∈ ℂ) → (-i · (π / 3))
= (i · -(π / 3))) |
164 | 34, 144, 163 | mp2an 689 |
. . . . . . . 8
⊢ (-i
· (π / 3)) = (i · -(π / 3)) |
165 | 164 | fveq2i 6774 |
. . . . . . 7
⊢
(exp‘(-i · (π / 3))) = (exp‘(i · -(π /
3))) |
166 | 143, 162,
165 | 3eqtri 2772 |
. . . . . 6
⊢ (((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3))) = (exp‘(i
· -(π / 3))) |
167 | 166 | fveq2i 6774 |
. . . . 5
⊢
(abs‘(((𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3)))) =
(abs‘(exp‘(i · -(π / 3)))) |
168 | 144 | absnegi 15110 |
. . . . . . . 8
⊢
(abs‘-(π / 3)) = (abs‘(π / 3)) |
169 | | df-neg 11208 |
. . . . . . . . 9
⊢ -(π /
3) = (0 − (π / 3)) |
170 | 169 | fveq2i 6774 |
. . . . . . . 8
⊢
(abs‘-(π / 3)) = (abs‘(0 − (π /
3))) |
171 | 168, 170 | eqtr3i 2770 |
. . . . . . 7
⊢
(abs‘(π / 3)) = (abs‘(0 − (π /
3))) |
172 | | rprege0 12744 |
. . . . . . . 8
⊢ ((π /
3) ∈ ℝ+ → ((π / 3) ∈ ℝ ∧ 0 ≤
(π / 3))) |
173 | | absid 15006 |
. . . . . . . 8
⊢ (((π /
3) ∈ ℝ ∧ 0 ≤ (π / 3)) → (abs‘(π / 3)) =
(π / 3)) |
174 | 8, 172, 173 | mp2b 10 |
. . . . . . 7
⊢
(abs‘(π / 3)) = (π / 3) |
175 | 171, 174 | eqtr3i 2770 |
. . . . . 6
⊢
(abs‘(0 − (π / 3))) = (π / 3) |
176 | 175 | oveq2i 7282 |
. . . . 5
⊢ (1
· (abs‘(0 − (π / 3)))) = (1 · (π /
3)) |
177 | 128, 167,
176 | 3brtr3i 5108 |
. . . 4
⊢
(abs‘(exp‘(i · -(π / 3)))) ≤ (1 · (π
/ 3)) |
178 | 23 | renegcli 11282 |
. . . . 5
⊢ -(π /
3) ∈ ℝ |
179 | | absefi 15903 |
. . . . 5
⊢ (-(π /
3) ∈ ℝ → (abs‘(exp‘(i · -(π / 3)))) =
1) |
180 | 178, 179 | ax-mp 5 |
. . . 4
⊢
(abs‘(exp‘(i · -(π / 3)))) = 1 |
181 | 144 | mulid2i 10981 |
. . . 4
⊢ (1
· (π / 3)) = (π / 3) |
182 | 177, 180,
181 | 3brtr3i 5108 |
. . 3
⊢ 1 ≤
(π / 3) |
183 | | 3pos 12078 |
. . . . 5
⊢ 0 <
3 |
184 | 21, 183 | pm3.2i 471 |
. . . 4
⊢ (3 ∈
ℝ ∧ 0 < 3) |
185 | | lemuldiv 11855 |
. . . 4
⊢ ((1
∈ ℝ ∧ π ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 <
3)) → ((1 · 3) ≤ π ↔ 1 ≤ (π /
3))) |
186 | 98, 20, 184, 185 | mp3an 1460 |
. . 3
⊢ ((1
· 3) ≤ π ↔ 1 ≤ (π / 3)) |
187 | 182, 186 | mpbir 230 |
. 2
⊢ (1
· 3) ≤ π |
188 | 2, 187 | eqbrtrri 5102 |
1
⊢ 3 ≤
π |