| Step | Hyp | Ref
| Expression |
| 1 | | 3cn 12347 |
. . 3
⊢ 3 ∈
ℂ |
| 2 | 1 | mullidi 11266 |
. 2
⊢ (1
· 3) = 3 |
| 3 | | tru 1544 |
. . . . . 6
⊢
⊤ |
| 4 | | 0xr 11308 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
| 5 | | pirp 26503 |
. . . . . . . . . 10
⊢ π
∈ ℝ+ |
| 6 | | 3rp 13040 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ+ |
| 7 | | rpdivcl 13060 |
. . . . . . . . . 10
⊢ ((π
∈ ℝ+ ∧ 3 ∈ ℝ+) → (π /
3) ∈ ℝ+) |
| 8 | 5, 6, 7 | mp2an 692 |
. . . . . . . . 9
⊢ (π /
3) ∈ ℝ+ |
| 9 | | rpxr 13044 |
. . . . . . . . 9
⊢ ((π /
3) ∈ ℝ+ → (π / 3) ∈
ℝ*) |
| 10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢ (π /
3) ∈ ℝ* |
| 11 | | rpge0 13048 |
. . . . . . . . 9
⊢ ((π /
3) ∈ ℝ+ → 0 ≤ (π / 3)) |
| 12 | 8, 11 | ax-mp 5 |
. . . . . . . 8
⊢ 0 ≤
(π / 3) |
| 13 | | lbicc2 13504 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ (π / 3) ∈ ℝ* ∧ 0
≤ (π / 3)) → 0 ∈ (0[,](π / 3))) |
| 14 | 4, 10, 12, 13 | mp3an 1463 |
. . . . . . 7
⊢ 0 ∈
(0[,](π / 3)) |
| 15 | | ubicc2 13505 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ (π / 3) ∈ ℝ* ∧ 0
≤ (π / 3)) → (π / 3) ∈ (0[,](π / 3))) |
| 16 | 4, 10, 12, 15 | mp3an 1463 |
. . . . . . 7
⊢ (π /
3) ∈ (0[,](π / 3)) |
| 17 | 14, 16 | pm3.2i 470 |
. . . . . 6
⊢ (0 ∈
(0[,](π / 3)) ∧ (π / 3) ∈ (0[,](π / 3))) |
| 18 | | 0re 11263 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
| 19 | 18 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 0 ∈ ℝ) |
| 20 | | pire 26500 |
. . . . . . . . 9
⊢ π
∈ ℝ |
| 21 | | 3re 12346 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
| 22 | | 3ne0 12372 |
. . . . . . . . 9
⊢ 3 ≠
0 |
| 23 | 20, 21, 22 | redivcli 12034 |
. . . . . . . 8
⊢ (π /
3) ∈ ℝ |
| 24 | 23 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (π / 3) ∈ ℝ) |
| 25 | | efcn 26487 |
. . . . . . . . 9
⊢ exp
∈ (ℂ–cn→ℂ) |
| 26 | 25 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ exp ∈ (ℂ–cn→ℂ)) |
| 27 | | iccssre 13469 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ (π / 3) ∈ ℝ) → (0[,](π / 3)) ⊆
ℝ) |
| 28 | 18, 23, 27 | mp2an 692 |
. . . . . . . . . . 11
⊢
(0[,](π / 3)) ⊆ ℝ |
| 29 | | ax-resscn 11212 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
| 30 | 28, 29 | sstri 3993 |
. . . . . . . . . 10
⊢
(0[,](π / 3)) ⊆ ℂ |
| 31 | | resmpt 6055 |
. . . . . . . . . 10
⊢
((0[,](π / 3)) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ↾ (0[,](π / 3))) =
(𝑥 ∈ (0[,](π / 3))
↦ (i · 𝑥))) |
| 32 | 30, 31 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑥 ∈ ℂ
↦ (i · 𝑥))
↾ (0[,](π / 3))) = (𝑥 ∈ (0[,](π / 3)) ↦ (i ·
𝑥))) |
| 33 | | ssidd 4007 |
. . . . . . . . . . 11
⊢ (⊤
→ ℂ ⊆ ℂ) |
| 34 | | ax-icn 11214 |
. . . . . . . . . . . . 13
⊢ i ∈
ℂ |
| 35 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 𝑥
∈ ℂ) |
| 36 | | mulcl 11239 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
| 37 | 34, 35, 36 | sylancr 587 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
| 38 | 37 | fmpttd 7135 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ (i · 𝑥)):ℂ⟶ℂ) |
| 39 | | cnelprrecn 11248 |
. . . . . . . . . . . . . . . 16
⊢ ℂ
∈ {ℝ, ℂ} |
| 40 | 39 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
| 41 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
| 42 | 41 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 1 ∈ ℂ) |
| 43 | 40 | dvmptid 25995 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 𝑥)) =
(𝑥 ∈ ℂ ↦
1)) |
| 44 | 34 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ i ∈ ℂ) |
| 45 | 40, 35, 42, 43, 44 | dvmptcmul 26002 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ (i ·
1))) |
| 46 | 34 | mulridi 11265 |
. . . . . . . . . . . . . . 15
⊢ (i
· 1) = i |
| 47 | 46 | mpteq2i 5247 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ ↦ (i
· 1)) = (𝑥 ∈
ℂ ↦ i) |
| 48 | 45, 47 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ i)) |
| 49 | 48 | dmeqd 5916 |
. . . . . . . . . . . 12
⊢ (⊤
→ dom (ℂ D (𝑥
∈ ℂ ↦ (i · 𝑥))) = dom (𝑥 ∈ ℂ ↦ i)) |
| 50 | 34 | elexi 3503 |
. . . . . . . . . . . . 13
⊢ i ∈
V |
| 51 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ ↦ i) =
(𝑥 ∈ ℂ ↦
i) |
| 52 | 50, 51 | dmmpti 6712 |
. . . . . . . . . . . 12
⊢ dom
(𝑥 ∈ ℂ ↦
i) = ℂ |
| 53 | 49, 52 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (⊤
→ dom (ℂ D (𝑥
∈ ℂ ↦ (i · 𝑥))) = ℂ) |
| 54 | | dvcn 25957 |
. . . . . . . . . . 11
⊢
(((ℂ ⊆ ℂ ∧ (𝑥 ∈ ℂ ↦ (i · 𝑥)):ℂ⟶ℂ ∧
ℂ ⊆ ℂ) ∧ dom (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = ℂ) → (𝑥 ∈ ℂ ↦ (i
· 𝑥)) ∈
(ℂ–cn→ℂ)) |
| 55 | 33, 38, 33, 53, 54 | syl31anc 1375 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ (i · 𝑥))
∈ (ℂ–cn→ℂ)) |
| 56 | | rescncf 24923 |
. . . . . . . . . 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 24940 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈ (0[,](π
/ 3)) ↦ (exp‘(i · 𝑥))) ∈ ((0[,](π / 3))–cn→ℂ)) |
| 60 | | reelprrecn 11247 |
. . . . . . . . . . 11
⊢ ℝ
∈ {ℝ, ℂ} |
| 61 | 60 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
| 62 | | recn 11245 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
| 63 | | efcl 16118 |
. . . . . . . . . . . 12
⊢ ((i
· 𝑥) ∈ ℂ
→ (exp‘(i · 𝑥)) ∈ ℂ) |
| 64 | 37, 63 | syl 17 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (exp‘(i · 𝑥)) ∈ ℂ) |
| 65 | 62, 64 | sylan2 593 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (exp‘(i · 𝑥)) ∈ ℂ) |
| 66 | | mulcl 11239 |
. . . . . . . . . . . 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 2737 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 70 | 69 | cnfldtopon 24803 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 71 | | toponmax 22932 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) |
| 72 | 70, 71 | mp1i 13 |
. . . . . . . . . . 11
⊢ (⊤
→ ℂ ∈ (TopOpen‘ℂfld)) |
| 73 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ℝ ⊆ ℂ) |
| 74 | | dfss2 3969 |
. . . . . . . . . . . 12
⊢ (ℝ
⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ) |
| 75 | 73, 74 | sylib 218 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℝ ∩ ℂ) = ℝ) |
| 76 | 34 | a1i 11 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℂ) → i ∈ ℂ) |
| 77 | | efcl 16118 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ →
(exp‘𝑦) ∈
ℂ) |
| 78 | 77 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑦
∈ ℂ) → (exp‘𝑦) ∈ ℂ) |
| 79 | | dvef 26018 |
. . . . . . . . . . . . 13
⊢ (ℂ
D exp) = exp |
| 80 | | eff 16117 |
. . . . . . . . . . . . . . . 16
⊢
exp:ℂ⟶ℂ |
| 81 | 80 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ exp:ℂ⟶ℂ) |
| 82 | 81 | feqmptd 6977 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ exp = (𝑦 ∈
ℂ ↦ (exp‘𝑦))) |
| 83 | 82 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D exp) = (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦)))) |
| 84 | 79, 83, 82 | 3eqtr3a 2801 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦))) |
| 85 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑦 = (i · 𝑥) → (exp‘𝑦) = (exp‘(i · 𝑥))) |
| 86 | 40, 40, 37, 76, 78, 78, 48, 84, 85, 85 | dvmptco 26010 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((exp‘(i
· 𝑥)) ·
i))) |
| 87 | 69, 61, 72, 75, 64, 67, 86 | dvmptres3 25994 |
. . . . . . . . . 10
⊢ (⊤
→ (ℝ D (𝑥 ∈
ℝ ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ ℝ ↦ ((exp‘(i
· 𝑥)) ·
i))) |
| 88 | 28 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (0[,](π / 3)) ⊆ ℝ) |
| 89 | 69 | tgioo2 24824 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 90 | | iccntr 24843 |
. . . . . . . . . . 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 26000 |
. . . . . . . . 9
⊢ (⊤
→ (ℝ D (𝑥 ∈
(0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i))) |
| 93 | 92 | dmeqd 5916 |
. . . . . . . 8
⊢ (⊤
→ dom (ℝ D (𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = dom (𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i))) |
| 94 | | ovex 7464 |
. . . . . . . . 9
⊢
((exp‘(i · 𝑥)) · i) ∈ V |
| 95 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i)) = (𝑥 ∈
(0(,)(π / 3)) ↦ ((exp‘(i · 𝑥)) · i)) |
| 96 | 94, 95 | dmmpti 6712 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ (0(,)(π / 3))
↦ ((exp‘(i · 𝑥)) · i)) = (0(,)(π /
3)) |
| 97 | 93, 96 | eqtrdi 2793 |
. . . . . . 7
⊢ (⊤
→ dom (ℝ D (𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = (0(,)(π / 3))) |
| 98 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 99 | 98 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 1 ∈ ℝ) |
| 100 | 92 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ (⊤
→ ((ℝ D (𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥))))‘𝑦) = ((𝑥 ∈ (0(,)(π / 3)) ↦
((exp‘(i · 𝑥))
· i))‘𝑦)) |
| 101 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (i · 𝑥) = (i · 𝑦)) |
| 102 | 101 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (exp‘(i · 𝑥)) = (exp‘(i ·
𝑦))) |
| 103 | 102 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((exp‘(i · 𝑥)) · i) = ((exp‘(i
· 𝑦)) ·
i)) |
| 104 | 103, 95, 94 | fvmpt3i 7021 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0(,)(π / 3)) →
((𝑥 ∈ (0(,)(π / 3))
↦ ((exp‘(i · 𝑥)) · i))‘𝑦) = ((exp‘(i · 𝑦)) · i)) |
| 105 | 100, 104 | sylan9eq 2797 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → ((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦) = ((exp‘(i · 𝑦)) · i)) |
| 106 | 105 | fveq2d 6910 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦)) = (abs‘((exp‘(i · 𝑦)) ·
i))) |
| 107 | | ioossre 13448 |
. . . . . . . . . . . . . . 15
⊢
(0(,)(π / 3)) ⊆ ℝ |
| 108 | 107 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (0(,)(π / 3)) ⊆ ℝ) |
| 109 | 108 | sselda 3983 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → 𝑦 ∈ ℝ) |
| 110 | 109 | recnd 11289 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → 𝑦 ∈ ℂ) |
| 111 | | mulcl 11239 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ 𝑦
∈ ℂ) → (i · 𝑦) ∈ ℂ) |
| 112 | 34, 110, 111 | sylancr 587 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (i · 𝑦) ∈ ℂ) |
| 113 | | efcl 16118 |
. . . . . . . . . . 11
⊢ ((i
· 𝑦) ∈ ℂ
→ (exp‘(i · 𝑦)) ∈ ℂ) |
| 114 | 112, 113 | syl 17 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (exp‘(i · 𝑦)) ∈ ℂ) |
| 115 | | absmul 15333 |
. . . . . . . . . 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 16232 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ →
(abs‘(exp‘(i · 𝑦))) = 1) |
| 118 | 109, 117 | syl 17 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘(exp‘(i · 𝑦))) = 1) |
| 119 | | absi 15325 |
. . . . . . . . . . . 12
⊢
(abs‘i) = 1 |
| 120 | 119 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘i) = 1) |
| 121 | 118, 120 | oveq12d 7449 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → ((abs‘(exp‘(i · 𝑦))) · (abs‘i)) = (1
· 1)) |
| 122 | 41 | mulridi 11265 |
. . . . . . . . . 10
⊢ (1
· 1) = 1 |
| 123 | 121, 122 | eqtrdi 2793 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → ((abs‘(exp‘(i · 𝑦))) · (abs‘i)) =
1) |
| 124 | 106, 116,
123 | 3eqtrd 2781 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦)) = 1) |
| 125 | | 1le1 11891 |
. . . . . . . 8
⊢ 1 ≤
1 |
| 126 | 124, 125 | eqbrtrdi 5182 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥))))‘𝑦)) ≤ 1) |
| 127 | 19, 24, 59, 97, 99, 126 | dvlip 26032 |
. . . . . 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 692 |
. . . . 5
⊢
(abs‘(((𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3)))) ≤ (1 ·
(abs‘(0 − (π / 3)))) |
| 129 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → (i · 𝑥) = (i ·
0)) |
| 130 | | it0e0 12488 |
. . . . . . . . . . . . 13
⊢ (i
· 0) = 0 |
| 131 | 129, 130 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (i · 𝑥) = 0) |
| 132 | 131 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (exp‘(i
· 𝑥)) =
(exp‘0)) |
| 133 | | ef0 16127 |
. . . . . . . . . . 11
⊢
(exp‘0) = 1 |
| 134 | 132, 133 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (exp‘(i
· 𝑥)) =
1) |
| 135 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))
= (𝑥 ∈ (0[,](π /
3)) ↦ (exp‘(i · 𝑥))) |
| 136 | | fvex 6919 |
. . . . . . . . . 10
⊢
(exp‘(i · 𝑥)) ∈ V |
| 137 | 134, 135,
136 | fvmpt3i 7021 |
. . . . . . . . 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 7439 |
. . . . . . . . . . 11
⊢ (𝑥 = (π / 3) → (i ·
𝑥) = (i · (π /
3))) |
| 140 | 139 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑥 = (π / 3) →
(exp‘(i · 𝑥))
= (exp‘(i · (π / 3)))) |
| 141 | 140, 135,
136 | fvmpt3i 7021 |
. . . . . . . . 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 7443 |
. . . . . . 7
⊢ (((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3))) = (1 −
(exp‘(i · (π / 3)))) |
| 144 | 23 | recni 11275 |
. . . . . . . . . 10
⊢ (π /
3) ∈ ℂ |
| 145 | 34, 144 | mulcli 11268 |
. . . . . . . . 9
⊢ (i
· (π / 3)) ∈ ℂ |
| 146 | | efcl 16118 |
. . . . . . . . 9
⊢ ((i
· (π / 3)) ∈ ℂ → (exp‘(i · (π / 3)))
∈ ℂ) |
| 147 | 145, 146 | ax-mp 5 |
. . . . . . . 8
⊢
(exp‘(i · (π / 3))) ∈ ℂ |
| 148 | | negicn 11509 |
. . . . . . . . . 10
⊢ -i ∈
ℂ |
| 149 | 148, 144 | mulcli 11268 |
. . . . . . . . 9
⊢ (-i
· (π / 3)) ∈ ℂ |
| 150 | | efcl 16118 |
. . . . . . . . 9
⊢ ((-i
· (π / 3)) ∈ ℂ → (exp‘(-i · (π / 3)))
∈ ℂ) |
| 151 | 149, 150 | ax-mp 5 |
. . . . . . . 8
⊢
(exp‘(-i · (π / 3))) ∈ ℂ |
| 152 | | cosval 16159 |
. . . . . . . . . . 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 26559 |
. . . . . . . . . . 11
⊢
((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π
/ 3)) = (1 / 2)) |
| 155 | 154 | simpri 485 |
. . . . . . . . . 10
⊢
(cos‘(π / 3)) = (1 / 2) |
| 156 | 153, 155 | eqtr3i 2767 |
. . . . . . . . 9
⊢
(((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) / 2) = (1 / 2) |
| 157 | 147, 151 | addcli 11267 |
. . . . . . . . . 10
⊢
((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) ∈ ℂ |
| 158 | | 2cn 12341 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
| 159 | | 2ne0 12370 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
| 160 | 157, 41, 158, 159 | div11i 12026 |
. . . . . . . . 9
⊢
((((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) / 2) = (1 / 2) ↔ ((exp‘(i · (π / 3))) +
(exp‘(-i · (π / 3)))) = 1) |
| 161 | 156, 160 | mpbi 230 |
. . . . . . . 8
⊢
((exp‘(i · (π / 3))) + (exp‘(-i · (π /
3)))) = 1 |
| 162 | 41, 147, 151, 161 | subaddrii 11598 |
. . . . . . 7
⊢ (1
− (exp‘(i · (π / 3)))) = (exp‘(-i · (π /
3))) |
| 163 | | mulneg12 11701 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ (π / 3) ∈ ℂ) → (-i · (π / 3))
= (i · -(π / 3))) |
| 164 | 34, 144, 163 | mp2an 692 |
. . . . . . . 8
⊢ (-i
· (π / 3)) = (i · -(π / 3)) |
| 165 | 164 | fveq2i 6909 |
. . . . . . 7
⊢
(exp‘(-i · (π / 3))) = (exp‘(i · -(π /
3))) |
| 166 | 143, 162,
165 | 3eqtri 2769 |
. . . . . 6
⊢ (((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3))) = (exp‘(i
· -(π / 3))) |
| 167 | 166 | fveq2i 6909 |
. . . . 5
⊢
(abs‘(((𝑥
∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦
(exp‘(i · 𝑥)))‘(π / 3)))) =
(abs‘(exp‘(i · -(π / 3)))) |
| 168 | 144 | absnegi 15439 |
. . . . . . . 8
⊢
(abs‘-(π / 3)) = (abs‘(π / 3)) |
| 169 | | df-neg 11495 |
. . . . . . . . 9
⊢ -(π /
3) = (0 − (π / 3)) |
| 170 | 169 | fveq2i 6909 |
. . . . . . . 8
⊢
(abs‘-(π / 3)) = (abs‘(0 − (π /
3))) |
| 171 | 168, 170 | eqtr3i 2767 |
. . . . . . 7
⊢
(abs‘(π / 3)) = (abs‘(0 − (π /
3))) |
| 172 | | rprege0 13050 |
. . . . . . . 8
⊢ ((π /
3) ∈ ℝ+ → ((π / 3) ∈ ℝ ∧ 0 ≤
(π / 3))) |
| 173 | | absid 15335 |
. . . . . . . 8
⊢ (((π /
3) ∈ ℝ ∧ 0 ≤ (π / 3)) → (abs‘(π / 3)) =
(π / 3)) |
| 174 | 8, 172, 173 | mp2b 10 |
. . . . . . 7
⊢
(abs‘(π / 3)) = (π / 3) |
| 175 | 171, 174 | eqtr3i 2767 |
. . . . . 6
⊢
(abs‘(0 − (π / 3))) = (π / 3) |
| 176 | 175 | oveq2i 7442 |
. . . . 5
⊢ (1
· (abs‘(0 − (π / 3)))) = (1 · (π /
3)) |
| 177 | 128, 167,
176 | 3brtr3i 5172 |
. . . 4
⊢
(abs‘(exp‘(i · -(π / 3)))) ≤ (1 · (π
/ 3)) |
| 178 | 23 | renegcli 11570 |
. . . . 5
⊢ -(π /
3) ∈ ℝ |
| 179 | | absefi 16232 |
. . . . 5
⊢ (-(π /
3) ∈ ℝ → (abs‘(exp‘(i · -(π / 3)))) =
1) |
| 180 | 178, 179 | ax-mp 5 |
. . . 4
⊢
(abs‘(exp‘(i · -(π / 3)))) = 1 |
| 181 | 144 | mullidi 11266 |
. . . 4
⊢ (1
· (π / 3)) = (π / 3) |
| 182 | 177, 180,
181 | 3brtr3i 5172 |
. . 3
⊢ 1 ≤
(π / 3) |
| 183 | | 3pos 12371 |
. . . . 5
⊢ 0 <
3 |
| 184 | 21, 183 | pm3.2i 470 |
. . . 4
⊢ (3 ∈
ℝ ∧ 0 < 3) |
| 185 | | lemuldiv 12148 |
. . . 4
⊢ ((1
∈ ℝ ∧ π ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 <
3)) → ((1 · 3) ≤ π ↔ 1 ≤ (π /
3))) |
| 186 | 98, 20, 184, 185 | mp3an 1463 |
. . 3
⊢ ((1
· 3) ≤ π ↔ 1 ≤ (π / 3)) |
| 187 | 182, 186 | mpbir 231 |
. 2
⊢ (1
· 3) ≤ π |
| 188 | 2, 187 | eqbrtrri 5166 |
1
⊢ 3 ≤
π |