Step |
Hyp |
Ref |
Expression |
1 |
|
fouriercn.f |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ ) |
2 |
|
fouriercn.t |
⊢ 𝑇 = ( 2 · π ) |
3 |
|
fouriercn.per |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ) |
4 |
|
fouriercn.dv |
⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( ℝ –cn→ ℂ ) ) |
5 |
|
fouriercn.g |
⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) |
6 |
|
fouriercn.x |
⊢ ( 𝜑 → 𝑋 ∈ ℝ ) |
7 |
|
fouriercn.a |
⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) ) |
8 |
|
fouriercn.b |
⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) ) |
9 |
5
|
dmeqi |
⊢ dom 𝐺 = dom ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) |
10 |
|
ioossre |
⊢ ( - π (,) π ) ⊆ ℝ |
11 |
|
cncff |
⊢ ( ( ℝ D 𝐹 ) ∈ ( ℝ –cn→ ℂ ) → ( ℝ D 𝐹 ) : ℝ ⟶ ℂ ) |
12 |
|
fdm |
⊢ ( ( ℝ D 𝐹 ) : ℝ ⟶ ℂ → dom ( ℝ D 𝐹 ) = ℝ ) |
13 |
4 11 12
|
3syl |
⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ℝ ) |
14 |
10 13
|
sseqtrrid |
⊢ ( 𝜑 → ( - π (,) π ) ⊆ dom ( ℝ D 𝐹 ) ) |
15 |
|
ssdmres |
⊢ ( ( - π (,) π ) ⊆ dom ( ℝ D 𝐹 ) ↔ dom ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) = ( - π (,) π ) ) |
16 |
14 15
|
sylib |
⊢ ( 𝜑 → dom ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) = ( - π (,) π ) ) |
17 |
9 16
|
eqtrid |
⊢ ( 𝜑 → dom 𝐺 = ( - π (,) π ) ) |
18 |
17
|
difeq2d |
⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) = ( ( - π (,) π ) ∖ ( - π (,) π ) ) ) |
19 |
|
difid |
⊢ ( ( - π (,) π ) ∖ ( - π (,) π ) ) = ∅ |
20 |
18 19
|
eqtrdi |
⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) = ∅ ) |
21 |
|
0fin |
⊢ ∅ ∈ Fin |
22 |
20 21
|
eqeltrdi |
⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin ) |
23 |
|
rescncf |
⊢ ( ( - π (,) π ) ⊆ ℝ → ( ( ℝ D 𝐹 ) ∈ ( ℝ –cn→ ℂ ) → ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ∈ ( ( - π (,) π ) –cn→ ℂ ) ) ) |
24 |
10 4 23
|
mpsyl |
⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ∈ ( ( - π (,) π ) –cn→ ℂ ) ) |
25 |
5
|
a1i |
⊢ ( 𝜑 → 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ) |
26 |
17
|
oveq1d |
⊢ ( 𝜑 → ( dom 𝐺 –cn→ ℂ ) = ( ( - π (,) π ) –cn→ ℂ ) ) |
27 |
24 25 26
|
3eltr4d |
⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) ) |
28 |
|
pire |
⊢ π ∈ ℝ |
29 |
28
|
renegcli |
⊢ - π ∈ ℝ |
30 |
28
|
rexri |
⊢ π ∈ ℝ* |
31 |
|
icossre |
⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ* ) → ( - π [,) π ) ⊆ ℝ ) |
32 |
29 30 31
|
mp2an |
⊢ ( - π [,) π ) ⊆ ℝ |
33 |
|
eldifi |
⊢ ( 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) → 𝑥 ∈ ( - π [,) π ) ) |
34 |
32 33
|
sselid |
⊢ ( 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) → 𝑥 ∈ ℝ ) |
35 |
|
limcresi |
⊢ ( ( ℝ D 𝐹 ) limℂ 𝑥 ) ⊆ ( ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( 𝑥 (,) +∞ ) ) ) limℂ 𝑥 ) |
36 |
5
|
reseq1i |
⊢ ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) = ( ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ↾ ( 𝑥 (,) +∞ ) ) |
37 |
|
resres |
⊢ ( ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ↾ ( 𝑥 (,) +∞ ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( 𝑥 (,) +∞ ) ) ) |
38 |
36 37
|
eqtr2i |
⊢ ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( 𝑥 (,) +∞ ) ) ) = ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) |
39 |
38
|
oveq1i |
⊢ ( ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( 𝑥 (,) +∞ ) ) ) limℂ 𝑥 ) = ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) |
40 |
35 39
|
sseqtri |
⊢ ( ( ℝ D 𝐹 ) limℂ 𝑥 ) ⊆ ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) |
41 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ℝ D 𝐹 ) ∈ ( ℝ –cn→ ℂ ) ) |
42 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ ) |
43 |
41 42
|
cnlimci |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ( ( ℝ D 𝐹 ) limℂ 𝑥 ) ) |
44 |
40 43
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ) |
45 |
44
|
ne0d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ ) |
46 |
34 45
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ ) |
47 |
|
negpitopissre |
⊢ ( - π (,] π ) ⊆ ℝ |
48 |
|
eldifi |
⊢ ( 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) → 𝑥 ∈ ( - π (,] π ) ) |
49 |
47 48
|
sselid |
⊢ ( 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) → 𝑥 ∈ ℝ ) |
50 |
|
limcresi |
⊢ ( ( ℝ D 𝐹 ) limℂ 𝑥 ) ⊆ ( ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( -∞ (,) 𝑥 ) ) ) limℂ 𝑥 ) |
51 |
5
|
reseq1i |
⊢ ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) = ( ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ↾ ( -∞ (,) 𝑥 ) ) |
52 |
|
resres |
⊢ ( ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ↾ ( -∞ (,) 𝑥 ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( -∞ (,) 𝑥 ) ) ) |
53 |
51 52
|
eqtr2i |
⊢ ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( -∞ (,) 𝑥 ) ) ) = ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) |
54 |
53
|
oveq1i |
⊢ ( ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( -∞ (,) 𝑥 ) ) ) limℂ 𝑥 ) = ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) |
55 |
50 54
|
sseqtri |
⊢ ( ( ℝ D 𝐹 ) limℂ 𝑥 ) ⊆ ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) |
56 |
55 43
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ) |
57 |
56
|
ne0d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ ) |
58 |
49 57
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ ) |
59 |
|
eqid |
⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) ) |
60 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
61 |
60
|
a1i |
⊢ ( 𝜑 → ℝ ⊆ ℂ ) |
62 |
1 61
|
fssd |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ ) |
63 |
|
ssid |
⊢ ℝ ⊆ ℝ |
64 |
63
|
a1i |
⊢ ( 𝜑 → ℝ ⊆ ℝ ) |
65 |
|
dvcn |
⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ℝ ⟶ ℂ ∧ ℝ ⊆ ℝ ) ∧ dom ( ℝ D 𝐹 ) = ℝ ) → 𝐹 ∈ ( ℝ –cn→ ℂ ) ) |
66 |
61 62 64 13 65
|
syl31anc |
⊢ ( 𝜑 → 𝐹 ∈ ( ℝ –cn→ ℂ ) ) |
67 |
|
cncffvrn |
⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ℝ –cn→ ℂ ) ) → ( 𝐹 ∈ ( ℝ –cn→ ℝ ) ↔ 𝐹 : ℝ ⟶ ℝ ) ) |
68 |
61 66 67
|
syl2anc |
⊢ ( 𝜑 → ( 𝐹 ∈ ( ℝ –cn→ ℝ ) ↔ 𝐹 : ℝ ⟶ ℝ ) ) |
69 |
1 68
|
mpbird |
⊢ ( 𝜑 → 𝐹 ∈ ( ℝ –cn→ ℝ ) ) |
70 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
71 |
70
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
72 |
70 71 71
|
cncfcn |
⊢ ( ( ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℝ –cn→ ℝ ) = ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) ) |
73 |
61 61 72
|
syl2anc |
⊢ ( 𝜑 → ( ℝ –cn→ ℝ ) = ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) ) |
74 |
69 73
|
eleqtrd |
⊢ ( 𝜑 → 𝐹 ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) ) |
75 |
|
uniretop |
⊢ ℝ = ∪ ( topGen ‘ ran (,) ) |
76 |
75
|
cncnpi |
⊢ ( ( 𝐹 ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) ∧ 𝑋 ∈ ℝ ) → 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) ) |
77 |
74 6 76
|
syl2anc |
⊢ ( 𝜑 → 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) ) |
78 |
1 2 3 5 22 27 46 58 59 77 7 8
|
fouriercnp |
⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( 𝐹 ‘ 𝑋 ) ) |