Step | Hyp | Ref
| Expression |
1 | | 3cn 11095 |
. . 3
⊢ 3 ∈
ℂ |
2 | 1 | mulid2i 10043 |
. 2
⊢ (1
· 3) = 3 |
3 | | tru 1487 |
. . . . . 6
⊢
⊤ |
4 | | 0xr 10086 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
5 | | pirp 24213 |
. . . . . . . . . 10
⊢ π
∈ ℝ+ |
6 | | 3re 11094 |
. . . . . . . . . . 11
⊢ 3 ∈
ℝ |
7 | | 3pos 11114 |
. . . . . . . . . . 11
⊢ 0 <
3 |
8 | 6, 7 | elrpii 11835 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ+ |
9 | | rpdivcl 11856 |
. . . . . . . . . 10
⊢ ((π
∈ ℝ+ ∧ 3 ∈ ℝ+) → (π /
3) ∈ ℝ+) |
10 | 5, 8, 9 | mp2an 708 |
. . . . . . . . 9
⊢ (π /
3) ∈ ℝ+ |
11 | | rpxr 11840 |
. . . . . . . . 9
⊢ ((π /
3) ∈ ℝ+ → (π / 3) ∈
ℝ*) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . 8
⊢ (π /
3) ∈ ℝ* |
13 | | rpge0 11845 |
. . . . . . . . 9
⊢ ((π /
3) ∈ ℝ+ → 0 ≤ (π / 3)) |
14 | 10, 13 | ax-mp 5 |
. . . . . . . 8
⊢ 0 ≤
(π / 3) |
15 | | lbicc2 12288 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ (π / 3) ∈ ℝ* ∧ 0
≤ (π / 3)) → 0 ∈ (0[,](π / 3))) |
16 | 4, 12, 14, 15 | mp3an 1424 |
. . . . . . 7
⊢ 0 ∈
(0[,](π / 3)) |
17 | | ubicc2 12289 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ (π / 3) ∈ ℝ* ∧ 0
≤ (π / 3)) → (π / 3) ∈ (0[,](π / 3))) |
18 | 4, 12, 14, 17 | mp3an 1424 |
. . . . . . 7
⊢ (π /
3) ∈ (0[,](π / 3)) |
19 | 16, 18 | pm3.2i 471 |
. . . . . 6
⊢ (0 ∈
(0[,](π / 3)) ∧ (π / 3) ∈ (0[,](π / 3))) |
20 | | 0re 10040 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
21 | 20 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 0 ∈ ℝ) |
22 | | pire 24210 |
. . . . . . . . 9
⊢ π
∈ ℝ |
23 | | 3ne0 11115 |
. . . . . . . . 9
⊢ 3 ≠
0 |
24 | 22, 6, 23 | redivcli 10792 |
. . . . . . . 8
⊢ (π /
3) ∈ ℝ |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (π / 3) ∈ ℝ) |
26 | | efcn 24197 |
. . . . . . . . 9
⊢ exp
∈ (ℂ–cn→ℂ) |
27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ exp ∈ (ℂ–cn→ℂ)) |
28 | | iccssre 12255 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ (π / 3) ∈ ℝ) → (0[,](π / 3)) ⊆
ℝ) |
29 | 20, 24, 28 | mp2an 708 |
. . . . . . . . . . 11
⊢
(0[,](π / 3)) ⊆ ℝ |
30 | | ax-resscn 9993 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
31 | 29, 30 | sstri 3612 |
. . . . . . . . . 10
⊢
(0[,](π / 3)) ⊆ ℂ |
32 | | resmpt 5449 |
. . . . . . . . . 10
⊢
((0[,](π / 3)) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ↾ (0[,](π / 3))) =
(𝑥 ∈ (0[,](π / 3))
↦ (i · 𝑥))) |
33 | 31, 32 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑥 ∈ ℂ
↦ (i · 𝑥))
↾ (0[,](π / 3))) = (𝑥 ∈ (0[,](π / 3)) ↦ (i ·
𝑥))) |
34 | | ssid 3624 |
. . . . . . . . . . . 12
⊢ ℂ
⊆ ℂ |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ ℂ ⊆ ℂ) |
36 | | ax-icn 9995 |
. . . . . . . . . . . . 13
⊢ i ∈
ℂ |
37 | | simpr 477 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 𝑥
∈ ℂ) |
38 | | mulcl 10020 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
39 | 36, 37, 38 | sylancr 695 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
40 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ ↦ (i
· 𝑥)) = (𝑥 ∈ ℂ ↦ (i
· 𝑥)) |
41 | 39, 40 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ (i · 𝑥)):ℂ⟶ℂ) |
42 | | cnelprrecn 10029 |
. . . . . . . . . . . . . . . 16
⊢ ℂ
∈ {ℝ, ℂ} |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
44 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 1 ∈ ℂ) |
46 | 43 | dvmptid 23720 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 𝑥)) =
(𝑥 ∈ ℂ ↦
1)) |
47 | 36 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ i ∈ ℂ) |
48 | 43, 37, 45, 46, 47 | dvmptcmul 23727 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ (i ·
1))) |
49 | 36 | mulid1i 10042 |
. . . . . . . . . . . . . . 15
⊢ (i
· 1) = i |
50 | 49 | mpteq2i 4741 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ ↦ (i
· 1)) = (𝑥 ∈
ℂ ↦ i) |
51 | 48, 50 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ i)) |
52 | 51 | dmeqd 5326 |
. . . . . . . . . . . 12
⊢ (⊤
→ dom (ℂ D (𝑥
∈ ℂ ↦ (i · 𝑥))) = dom (𝑥 ∈ ℂ ↦ i)) |
53 | 36 | elexi 3213 |
. . . . . . . . . . . . 13
⊢ i ∈
V |
54 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ ↦ i) =
(𝑥 ∈ ℂ ↦
i) |
55 | 53, 54 | dmmpti 6023 |
. . . . . . . . . . . 12
⊢ dom
(𝑥 ∈ ℂ ↦
i) = ℂ |
56 | 52, 55 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (⊤
→ dom (ℂ D (𝑥
∈ ℂ ↦ (i · 𝑥))) = ℂ) |
57 | | dvcn 23684 |
. . . . . . . . . . 11
⊢
(((ℂ ⊆ ℂ ∧ (𝑥 ∈ ℂ ↦ (i · 𝑥)):ℂ⟶ℂ ∧
ℂ ⊆ ℂ) ∧ dom (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = ℂ) → (𝑥 ∈ ℂ ↦ (i
· 𝑥)) ∈
(ℂ–cn→ℂ)) |
58 | 35, 41, 35, 56, 57 | syl31anc 1329 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ (i · 𝑥))
∈ (ℂ–cn→ℂ)) |
59 | | rescncf 22700 |
. . . . . . . . . 10
⊢
((0[,](π / 3)) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ↾ (0[,](π / 3)))
∈ ((0[,](π / 3))–cn→ℂ))) |
60 | 31, 58, 59 | mpsyl 68 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑥 ∈ ℂ
↦ (i · 𝑥))
↾ (0[,](π / 3))) ∈ ((0[,](π / 3))–cn→ℂ)) |
61 | 33, 60 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈ (0[,](π
/ 3)) ↦ (i · 𝑥)) ∈ ((0[,](π / 3))–cn→ℂ)) |
62 | 27, 61 | cncfmpt1f 22716 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈ (0[,](π
/ 3)) ↦ (exp‘(i · 𝑥))) ∈ ((0[,](π / 3))–cn→ℂ)) |
63 | | reelprrecn 10028 |
. . . . . . . . . . 11
⊢ ℝ
∈ {ℝ, ℂ} |
64 | 63 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
65 | | recn 10026 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
66 | | efcl 14813 |
. . . . . . . . . . . 12
⊢ ((i
· 𝑥) ∈ ℂ
→ (exp‘(i · 𝑥)) ∈ ℂ) |
67 | 39, 66 | syl 17 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (exp‘(i · 𝑥)) ∈ ℂ) |
68 | 65, 67 | sylan2 491 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (exp‘(i · 𝑥)) ∈ ℂ) |
69 | | mulcl 10020 |
. . . . . . . . . . . 12
⊢
(((exp‘(i · 𝑥)) ∈ ℂ ∧ i ∈ ℂ)
→ ((exp‘(i · 𝑥)) · i) ∈
ℂ) |
70 | 67, 36, 69 | sylancl 694 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → ((exp‘(i · 𝑥)) · i) ∈
ℂ) |
71 | 65, 70 | sylan2 491 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ) → ((exp‘(i · 𝑥)) · i) ∈
ℂ) |
72 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
73 | 72 | cnfldtopon 22586 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
74 | | toponmax 20730 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) |
75 | 73, 74 | mp1i 13 |
. . . . . . . . . . 11
⊢ (⊤
→ ℂ ∈ (TopOpen‘ℂfld)) |
76 | 30 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ℝ ⊆ ℂ) |
77 | | df-ss 3588 |
. . . . . . . . . . . 12
⊢ (ℝ
⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ) |
78 | 76, 77 | sylib 208 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℝ ∩ ℂ) = ℝ) |
79 | 36 | a1i 11 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℂ) → i ∈ ℂ) |
80 | | efcl 14813 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ →
(exp‘𝑦) ∈
ℂ) |
81 | 80 | adantl 482 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑦
∈ ℂ) → (exp‘𝑦) ∈ ℂ) |
82 | | dvef 23743 |
. . . . . . . . . . . . 13
⊢ (ℂ
D exp) = exp |
83 | | eff 14812 |
. . . . . . . . . . . . . . . 16
⊢
exp:ℂ⟶ℂ |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ exp:ℂ⟶ℂ) |
85 | 84 | feqmptd 6249 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ exp = (𝑦 ∈
ℂ ↦ (exp‘𝑦))) |
86 | 85 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D exp) = (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦)))) |
87 | 82, 86, 85 | 3eqtr3a 2680 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦))) |
88 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑦 = (i · 𝑥) → (exp‘𝑦) = (exp‘(i · 𝑥))) |
89 | 43, 43, 39, 79, 81, 81, 51, 87, 88, 88 | dvmptco 23735 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((exp‘(i
· 𝑥)) ·
i))) |
90 | 72, 64, 75, 78, 67, 70, 89 | dvmptres3 23719 |
. . . . . . . . . 10
⊢ (⊤
→ (ℝ D (𝑥 ∈
ℝ ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ ℝ ↦ ((exp‘(i
· 𝑥)) ·
i))) |
91 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (0[,](π / 3)) ⊆ ℝ) |
92 | 72 | tgioo2 22606 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
93 | | iccntr 22624 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ (π / 3) ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(0[,](π / 3))) = (0(,)(π /
3))) |
94 | 20, 25, 93 | sylancr 695 |
. . . . . . . . . 10
⊢ (⊤
→ ((int‘(topGen‘ran (,)))‘(0[,](π / 3))) = (0(,)(π
/ 3))) |
95 | 64, 68, 71, 90, 91, 92, 72, 94 | dvmptres2 23725 |
. . . . . . . . 9
⊢ (⊤
→ (ℝ D (𝑥 ∈
(0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i))) |
96 | 95 | dmeqd 5326 |
. . . . . . . 8
⊢ (⊤
→ dom (ℝ D (𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = dom (𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i))) |
97 | | ovex 6678 |
. . . . . . . . 9
⊢
((exp‘(i · 𝑥)) · i) ∈ V |
98 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i)) = (𝑥 ∈
(0(,)(π / 3)) ↦ ((exp‘(i · 𝑥)) · i)) |
99 | 97, 98 | dmmpti 6023 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ (0(,)(π / 3))
↦ ((exp‘(i · 𝑥)) · i)) = (0(,)(π /
3)) |
100 | 96, 99 | syl6eq 2672 |
. . . . . . 7
⊢ (⊤
→ dom (ℝ D (𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = (0(,)(π / 3))) |
101 | | 1re 10039 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
102 | 101 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 1 ∈ ℝ) |
103 | 95 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ (⊤
→ ((ℝ D (𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥))))‘𝑦) = ((𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i))‘𝑦)) |
104 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (i · 𝑥) = (i · 𝑦)) |
105 | 104 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (exp‘(i · 𝑥)) = (exp‘(i ·
𝑦))) |
106 | 105 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((exp‘(i · 𝑥)) · i) = ((exp‘(i
· 𝑦)) ·
i)) |
107 | 106, 98, 97 | fvmpt3i 6287 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0(,)(π / 3)) →
((𝑥 ∈ (0(,)(π / 3))
↦ ((exp‘(i · 𝑥)) · i))‘𝑦) = ((exp‘(i · 𝑦)) · i)) |
108 | 103, 107 | sylan9eq 2676 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → ((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦) = ((exp‘(i · 𝑦)) · i)) |
109 | 108 | fveq2d 6195 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦)) = (abs‘((exp‘(i · 𝑦)) ·
i))) |
110 | | ioossre 12235 |
. . . . . . . . . . . . . . 15
⊢
(0(,)(π / 3)) ⊆ ℝ |
111 | 110 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (0(,)(π / 3)) ⊆ ℝ) |
112 | 111 | sselda 3603 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → 𝑦 ∈ ℝ) |
113 | 112 | recnd 10068 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → 𝑦 ∈ ℂ) |
114 | | mulcl 10020 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ 𝑦
∈ ℂ) → (i · 𝑦) ∈ ℂ) |
115 | 36, 113, 114 | sylancr 695 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (i · 𝑦) ∈ ℂ) |
116 | | efcl 14813 |
. . . . . . . . . . 11
⊢ ((i
· 𝑦) ∈ ℂ
→ (exp‘(i · 𝑦)) ∈ ℂ) |
117 | 115, 116 | syl 17 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (exp‘(i · 𝑦)) ∈ ℂ) |
118 | | absmul 14034 |
. . . . . . . . . 10
⊢
(((exp‘(i · 𝑦)) ∈ ℂ ∧ i ∈ ℂ)
→ (abs‘((exp‘(i · 𝑦)) · i)) = ((abs‘(exp‘(i
· 𝑦))) ·
(abs‘i))) |
119 | 117, 36, 118 | sylancl 694 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘((exp‘(i · 𝑦)) · i)) =
((abs‘(exp‘(i · 𝑦))) · (abs‘i))) |
120 | | absefi 14926 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ →
(abs‘(exp‘(i · 𝑦))) = 1) |
121 | 112, 120 | syl 17 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘(exp‘(i · 𝑦))) = 1) |
122 | | absi 14026 |
. . . . . . . . . . . 12
⊢
(abs‘i) = 1 |
123 | 122 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘i) = 1) |
124 | 121, 123 | oveq12d 6668 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → ((abs‘(exp‘(i · 𝑦))) · (abs‘i)) = (1
· 1)) |
125 | 44 | mulid1i 10042 |
. . . . . . . . . 10
⊢ (1
· 1) = 1 |
126 | 124, 125 | syl6eq 2672 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → ((abs‘(exp‘(i · 𝑦))) · (abs‘i)) =
1) |
127 | 109, 119,
126 | 3eqtrd 2660 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦)) = 1) |
128 | | 1le1 10655 |
. . . . . . . 8
⊢ 1 ≤
1 |
129 | 127, 128 | syl6eqbr 4692 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦)) ≤ 1) |
130 | 21, 25, 62, 100, 102, 129 | dvlip 23756 |
. . . . . 6
⊢
((⊤ ∧ (0 ∈ (0[,](π / 3)) ∧ (π / 3) ∈
(0[,](π / 3)))) → (abs‘(((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3)))) ≤ (1 ·
(abs‘(0 − (π / 3))))) |
131 | 3, 19, 130 | mp2an 708 |
. . . . 5
⊢
(abs‘(((𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3)))) ≤ (1 ·
(abs‘(0 − (π / 3)))) |
132 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → (i · 𝑥) = (i ·
0)) |
133 | | it0e0 11254 |
. . . . . . . . . . . . 13
⊢ (i
· 0) = 0 |
134 | 132, 133 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (i · 𝑥) = 0) |
135 | 134 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (exp‘(i
· 𝑥)) =
(exp‘0)) |
136 | | ef0 14821 |
. . . . . . . . . . 11
⊢
(exp‘0) = 1 |
137 | 135, 136 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (exp‘(i
· 𝑥)) =
1) |
138 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))
= (𝑥 ∈ (0[,](π /
3)) ↦ (exp‘(i · 𝑥))) |
139 | | fvex 6201 |
. . . . . . . . . 10
⊢
(exp‘(i · 𝑥)) ∈ V |
140 | 137, 138,
139 | fvmpt3i 6287 |
. . . . . . . . 9
⊢ (0 ∈
(0[,](π / 3)) → ((𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) = 1) |
141 | 16, 140 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘0) = 1 |
142 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑥 = (π / 3) → (i ·
𝑥) = (i · (π /
3))) |
143 | 142 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = (π / 3) →
(exp‘(i · 𝑥))
= (exp‘(i · (π / 3)))) |
144 | 143, 138,
139 | fvmpt3i 6287 |
. . . . . . . . 9
⊢ ((π /
3) ∈ (0[,](π / 3)) → ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3)) = (exp‘(i
· (π / 3)))) |
145 | 18, 144 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3)) = (exp‘(i
· (π / 3))) |
146 | 141, 145 | oveq12i 6662 |
. . . . . . 7
⊢ (((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3))) = (1 −
(exp‘(i · (π / 3)))) |
147 | 24 | recni 10052 |
. . . . . . . . . 10
⊢ (π /
3) ∈ ℂ |
148 | 36, 147 | mulcli 10045 |
. . . . . . . . 9
⊢ (i
· (π / 3)) ∈ ℂ |
149 | | efcl 14813 |
. . . . . . . . 9
⊢ ((i
· (π / 3)) ∈ ℂ → (exp‘(i · (π / 3)))
∈ ℂ) |
150 | 148, 149 | ax-mp 5 |
. . . . . . . 8
⊢
(exp‘(i · (π / 3))) ∈ ℂ |
151 | | negicn 10282 |
. . . . . . . . . 10
⊢ -i ∈
ℂ |
152 | 151, 147 | mulcli 10045 |
. . . . . . . . 9
⊢ (-i
· (π / 3)) ∈ ℂ |
153 | | efcl 14813 |
. . . . . . . . 9
⊢ ((-i
· (π / 3)) ∈ ℂ → (exp‘(-i · (π / 3)))
∈ ℂ) |
154 | 152, 153 | ax-mp 5 |
. . . . . . . 8
⊢
(exp‘(-i · (π / 3))) ∈ ℂ |
155 | | cosval 14853 |
. . . . . . . . . . 11
⊢ ((π /
3) ∈ ℂ → (cos‘(π / 3)) = (((exp‘(i ·
(π / 3))) + (exp‘(-i · (π / 3)))) / 2)) |
156 | 147, 155 | ax-mp 5 |
. . . . . . . . . 10
⊢
(cos‘(π / 3)) = (((exp‘(i · (π / 3))) +
(exp‘(-i · (π / 3)))) / 2) |
157 | | sincos3rdpi 24268 |
. . . . . . . . . . 11
⊢
((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π
/ 3)) = (1 / 2)) |
158 | 157 | simpri 478 |
. . . . . . . . . 10
⊢
(cos‘(π / 3)) = (1 / 2) |
159 | 156, 158 | eqtr3i 2646 |
. . . . . . . . 9
⊢
(((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) / 2) = (1 / 2) |
160 | 150, 154 | addcli 10044 |
. . . . . . . . . 10
⊢
((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) ∈ ℂ |
161 | | 2cn 11091 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
162 | | 2ne0 11113 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
163 | 160, 44, 161, 162 | div11i 10784 |
. . . . . . . . 9
⊢
((((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) / 2) = (1 / 2) ↔ ((exp‘(i · (π / 3))) +
(exp‘(-i · (π / 3)))) = 1) |
164 | 159, 163 | mpbi 220 |
. . . . . . . 8
⊢
((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) = 1 |
165 | 44, 150, 154, 164 | subaddrii 10370 |
. . . . . . 7
⊢ (1
− (exp‘(i · (π / 3)))) = (exp‘(-i · (π /
3))) |
166 | | mulneg12 10468 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ (π / 3) ∈ ℂ) → (-i · (π / 3))
= (i · -(π / 3))) |
167 | 36, 147, 166 | mp2an 708 |
. . . . . . . 8
⊢ (-i
· (π / 3)) = (i · -(π / 3)) |
168 | 167 | fveq2i 6194 |
. . . . . . 7
⊢
(exp‘(-i · (π / 3))) = (exp‘(i · -(π /
3))) |
169 | 146, 165,
168 | 3eqtri 2648 |
. . . . . 6
⊢ (((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3))) = (exp‘(i
· -(π / 3))) |
170 | 169 | fveq2i 6194 |
. . . . 5
⊢
(abs‘(((𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3)))) =
(abs‘(exp‘(i · -(π / 3)))) |
171 | 147 | absnegi 14139 |
. . . . . . . 8
⊢
(abs‘-(π / 3)) = (abs‘(π / 3)) |
172 | | df-neg 10269 |
. . . . . . . . 9
⊢ -(π /
3) = (0 − (π / 3)) |
173 | 172 | fveq2i 6194 |
. . . . . . . 8
⊢
(abs‘-(π / 3)) = (abs‘(0 − (π /
3))) |
174 | 171, 173 | eqtr3i 2646 |
. . . . . . 7
⊢
(abs‘(π / 3)) = (abs‘(0 − (π /
3))) |
175 | | rprege0 11847 |
. . . . . . . 8
⊢ ((π /
3) ∈ ℝ+ → ((π / 3) ∈ ℝ ∧ 0 ≤
(π / 3))) |
176 | | absid 14036 |
. . . . . . . 8
⊢ (((π /
3) ∈ ℝ ∧ 0 ≤ (π / 3)) → (abs‘(π / 3)) =
(π / 3)) |
177 | 10, 175, 176 | mp2b 10 |
. . . . . . 7
⊢
(abs‘(π / 3)) = (π / 3) |
178 | 174, 177 | eqtr3i 2646 |
. . . . . 6
⊢
(abs‘(0 − (π / 3))) = (π / 3) |
179 | 178 | oveq2i 6661 |
. . . . 5
⊢ (1
· (abs‘(0 − (π / 3)))) = (1 · (π /
3)) |
180 | 131, 170,
179 | 3brtr3i 4682 |
. . . 4
⊢
(abs‘(exp‘(i · -(π / 3)))) ≤ (1 · (π
/ 3)) |
181 | 24 | renegcli 10342 |
. . . . 5
⊢ -(π /
3) ∈ ℝ |
182 | | absefi 14926 |
. . . . 5
⊢ (-(π /
3) ∈ ℝ → (abs‘(exp‘(i · -(π / 3)))) =
1) |
183 | 181, 182 | ax-mp 5 |
. . . 4
⊢
(abs‘(exp‘(i · -(π / 3)))) = 1 |
184 | 147 | mulid2i 10043 |
. . . 4
⊢ (1
· (π / 3)) = (π / 3) |
185 | 180, 183,
184 | 3brtr3i 4682 |
. . 3
⊢ 1 ≤
(π / 3) |
186 | 6, 7 | pm3.2i 471 |
. . . 4
⊢ (3 ∈
ℝ ∧ 0 < 3) |
187 | | lemuldiv 10903 |
. . . 4
⊢ ((1
∈ ℝ ∧ π ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 <
3)) → ((1 · 3) ≤ π ↔ 1 ≤ (π /
3))) |
188 | 101, 22, 186, 187 | mp3an 1424 |
. . 3
⊢ ((1
· 3) ≤ π ↔ 1 ≤ (π / 3)) |
189 | 185, 188 | mpbir 221 |
. 2
⊢ (1
· 3) ≤ π |
190 | 2, 189 | eqbrtrri 4676 |
1
⊢ 3 ≤
π |