Step |
Hyp |
Ref |
Expression |
1 |
|
df-sin |
⊢ sin = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) |
2 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
3 |
2
|
subcn |
⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
4 |
3
|
a1i |
⊢ ( ⊤ → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ) |
5 |
|
efcn |
⊢ exp ∈ ( ℂ –cn→ ℂ ) |
6 |
5
|
a1i |
⊢ ( ⊤ → exp ∈ ( ℂ –cn→ ℂ ) ) |
7 |
|
ax-icn |
⊢ i ∈ ℂ |
8 |
|
eqid |
⊢ ( 𝑥 ∈ ℂ ↦ ( i · 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( i · 𝑥 ) ) |
9 |
8
|
mulc1cncf |
⊢ ( i ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( i · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) ) |
10 |
7 9
|
mp1i |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( i · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) ) |
11 |
6 10
|
cncfmpt1f |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( i · 𝑥 ) ) ) ∈ ( ℂ –cn→ ℂ ) ) |
12 |
|
negicn |
⊢ - i ∈ ℂ |
13 |
|
eqid |
⊢ ( 𝑥 ∈ ℂ ↦ ( - i · 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( - i · 𝑥 ) ) |
14 |
13
|
mulc1cncf |
⊢ ( - i ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( - i · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) ) |
15 |
12 14
|
mp1i |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( - i · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) ) |
16 |
6 15
|
cncfmpt1f |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ( ℂ –cn→ ℂ ) ) |
17 |
2 4 11 16
|
cncfmpt2f |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) ) |
18 |
|
cncff |
⊢ ( ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) → ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) : ℂ ⟶ ℂ ) |
19 |
17 18
|
syl |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) : ℂ ⟶ ℂ ) |
20 |
|
eqid |
⊢ ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) |
21 |
20
|
fmpt |
⊢ ( ∀ 𝑥 ∈ ℂ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ℂ ↔ ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) : ℂ ⟶ ℂ ) |
22 |
19 21
|
sylibr |
⊢ ( ⊤ → ∀ 𝑥 ∈ ℂ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ℂ ) |
23 |
|
eqidd |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) ) |
24 |
|
eqidd |
⊢ ( ⊤ → ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) ) |
25 |
|
oveq1 |
⊢ ( 𝑦 = ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) → ( 𝑦 / ( 2 · i ) ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) |
26 |
22 23 24 25
|
fmptcof |
⊢ ( ⊤ → ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) ∘ ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) ) |
27 |
|
2mulicn |
⊢ ( 2 · i ) ∈ ℂ |
28 |
|
2muline0 |
⊢ ( 2 · i ) ≠ 0 |
29 |
|
eqid |
⊢ ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) |
30 |
29
|
divccncf |
⊢ ( ( ( 2 · i ) ∈ ℂ ∧ ( 2 · i ) ≠ 0 ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) ∈ ( ℂ –cn→ ℂ ) ) |
31 |
27 28 30
|
mp2an |
⊢ ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) ∈ ( ℂ –cn→ ℂ ) |
32 |
31
|
a1i |
⊢ ( ⊤ → ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) ∈ ( ℂ –cn→ ℂ ) ) |
33 |
17 32
|
cncfco |
⊢ ( ⊤ → ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) ∘ ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) ) ∈ ( ℂ –cn→ ℂ ) ) |
34 |
26 33
|
eqeltrrd |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) ∈ ( ℂ –cn→ ℂ ) ) |
35 |
34
|
mptru |
⊢ ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) ∈ ( ℂ –cn→ ℂ ) |
36 |
1 35
|
eqeltri |
⊢ sin ∈ ( ℂ –cn→ ℂ ) |