Step | Hyp | Ref
| Expression |
1 | | resincncf 43387 |
. . . . 5
⊢ (sin
↾ ℝ) ∈ (ℝ–cn→ℝ) |
2 | | cncff 24054 |
. . . . 5
⊢ ((sin
↾ ℝ) ∈ (ℝ–cn→ℝ) → (sin ↾
ℝ):ℝ⟶ℝ) |
3 | 1, 2 | ax-mp 5 |
. . . 4
⊢ (sin
↾ ℝ):ℝ⟶ℝ |
4 | | fourierdlem18.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℝ) |
5 | | halfre 12187 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ |
6 | 5 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
7 | 4, 6 | readdcld 11005 |
. . . . . . 7
⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ) |
8 | 7 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (-π[,]π)) → (𝑁 + (1 / 2)) ∈
ℝ) |
9 | | pire 25613 |
. . . . . . . . . 10
⊢ π
∈ ℝ |
10 | 9 | renegcli 11282 |
. . . . . . . . 9
⊢ -π
∈ ℝ |
11 | | iccssre 13160 |
. . . . . . . . 9
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆
ℝ) |
12 | 10, 9, 11 | mp2an 689 |
. . . . . . . 8
⊢
(-π[,]π) ⊆ ℝ |
13 | 12 | sseli 3922 |
. . . . . . 7
⊢ (𝑠 ∈ (-π[,]π) →
𝑠 ∈
ℝ) |
14 | 13 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈
ℝ) |
15 | 8, 14 | remulcld 11006 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (-π[,]π)) → ((𝑁 + (1 / 2)) · 𝑠) ∈
ℝ) |
16 | | eqid 2740 |
. . . . 5
⊢ (𝑠 ∈ (-π[,]π) ↦
((𝑁 + (1 / 2)) ·
𝑠)) = (𝑠 ∈ (-π[,]π) ↦ ((𝑁 + (1 / 2)) · 𝑠)) |
17 | 15, 16 | fmptd 6985 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ (-π[,]π) ↦ ((𝑁 + (1 / 2)) · 𝑠)):(-π[,]π)⟶ℝ) |
18 | | fcompt 7002 |
. . . 4
⊢ (((sin
↾ ℝ):ℝ⟶ℝ ∧ (𝑠 ∈ (-π[,]π) ↦ ((𝑁 + (1 / 2)) · 𝑠)):(-π[,]π)⟶ℝ) →
((sin ↾ ℝ) ∘ (𝑠 ∈ (-π[,]π) ↦ ((𝑁 + (1 / 2)) · 𝑠))) = (𝑥 ∈ (-π[,]π) ↦ ((sin ↾
ℝ)‘((𝑠 ∈
(-π[,]π) ↦ ((𝑁
+ (1 / 2)) · 𝑠))‘𝑥)))) |
19 | 3, 17, 18 | sylancr 587 |
. . 3
⊢ (𝜑 → ((sin ↾ ℝ)
∘ (𝑠 ∈
(-π[,]π) ↦ ((𝑁
+ (1 / 2)) · 𝑠))) =
(𝑥 ∈ (-π[,]π)
↦ ((sin ↾ ℝ)‘((𝑠 ∈ (-π[,]π) ↦ ((𝑁 + (1 / 2)) · 𝑠))‘𝑥)))) |
20 | | eqidd 2741 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝑠 ∈ (-π[,]π) ↦
((𝑁 + (1 / 2)) ·
𝑠)) = (𝑠 ∈ (-π[,]π) ↦ ((𝑁 + (1 / 2)) · 𝑠))) |
21 | | oveq2 7279 |
. . . . . . . 8
⊢ (𝑠 = 𝑥 → ((𝑁 + (1 / 2)) · 𝑠) = ((𝑁 + (1 / 2)) · 𝑥)) |
22 | 21 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (-π[,]π)) ∧ 𝑠 = 𝑥) → ((𝑁 + (1 / 2)) · 𝑠) = ((𝑁 + (1 / 2)) · 𝑥)) |
23 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈
(-π[,]π)) |
24 | 7 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝑁 + (1 / 2)) ∈
ℝ) |
25 | 12, 23 | sselid 3924 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈
ℝ) |
26 | 24, 25 | remulcld 11006 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝑁 + (1 / 2)) · 𝑥) ∈
ℝ) |
27 | 20, 22, 23, 26 | fvmptd 6879 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝑠 ∈ (-π[,]π) ↦
((𝑁 + (1 / 2)) ·
𝑠))‘𝑥) = ((𝑁 + (1 / 2)) · 𝑥)) |
28 | 27 | fveq2d 6775 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((sin ↾
ℝ)‘((𝑠 ∈
(-π[,]π) ↦ ((𝑁
+ (1 / 2)) · 𝑠))‘𝑥)) = ((sin ↾ ℝ)‘((𝑁 + (1 / 2)) · 𝑥))) |
29 | 28 | mpteq2dva 5179 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((sin ↾
ℝ)‘((𝑠 ∈
(-π[,]π) ↦ ((𝑁
+ (1 / 2)) · 𝑠))‘𝑥))) = (𝑥 ∈ (-π[,]π) ↦ ((sin ↾
ℝ)‘((𝑁 + (1 /
2)) · 𝑥)))) |
30 | | fvres 6790 |
. . . . . 6
⊢ (((𝑁 + (1 / 2)) · 𝑥) ∈ ℝ → ((sin
↾ ℝ)‘((𝑁
+ (1 / 2)) · 𝑥)) =
(sin‘((𝑁 + (1 / 2))
· 𝑥))) |
31 | 26, 30 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((sin ↾
ℝ)‘((𝑁 + (1 /
2)) · 𝑥)) =
(sin‘((𝑁 + (1 / 2))
· 𝑥))) |
32 | 31 | mpteq2dva 5179 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((sin ↾
ℝ)‘((𝑁 + (1 /
2)) · 𝑥))) = (𝑥 ∈ (-π[,]π) ↦
(sin‘((𝑁 + (1 / 2))
· 𝑥)))) |
33 | | oveq2 7279 |
. . . . . . 7
⊢ (𝑥 = 𝑠 → ((𝑁 + (1 / 2)) · 𝑥) = ((𝑁 + (1 / 2)) · 𝑠)) |
34 | 33 | fveq2d 6775 |
. . . . . 6
⊢ (𝑥 = 𝑠 → (sin‘((𝑁 + (1 / 2)) · 𝑥)) = (sin‘((𝑁 + (1 / 2)) · 𝑠))) |
35 | 34 | cbvmptv 5192 |
. . . . 5
⊢ (𝑥 ∈ (-π[,]π) ↦
(sin‘((𝑁 + (1 / 2))
· 𝑥))) = (𝑠 ∈ (-π[,]π) ↦
(sin‘((𝑁 + (1 / 2))
· 𝑠))) |
36 | 35 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦
(sin‘((𝑁 + (1 / 2))
· 𝑥))) = (𝑠 ∈ (-π[,]π) ↦
(sin‘((𝑁 + (1 / 2))
· 𝑠)))) |
37 | 29, 32, 36 | 3eqtrd 2784 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((sin ↾
ℝ)‘((𝑠 ∈
(-π[,]π) ↦ ((𝑁
+ (1 / 2)) · 𝑠))‘𝑥))) = (𝑠 ∈ (-π[,]π) ↦
(sin‘((𝑁 + (1 / 2))
· 𝑠)))) |
38 | | fourierdlem18.s |
. . . . 5
⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦
(sin‘((𝑁 + (1 / 2))
· 𝑠))) |
39 | 38 | eqcomi 2749 |
. . . 4
⊢ (𝑠 ∈ (-π[,]π) ↦
(sin‘((𝑁 + (1 / 2))
· 𝑠))) = 𝑆 |
40 | 39 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑠 ∈ (-π[,]π) ↦
(sin‘((𝑁 + (1 / 2))
· 𝑠))) = 𝑆) |
41 | 19, 37, 40 | 3eqtrrd 2785 |
. 2
⊢ (𝜑 → 𝑆 = ((sin ↾ ℝ) ∘ (𝑠 ∈ (-π[,]π) ↦
((𝑁 + (1 / 2)) ·
𝑠)))) |
42 | | ax-resscn 10929 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
43 | 12, 42 | sstri 3935 |
. . . . . . 7
⊢
(-π[,]π) ⊆ ℂ |
44 | 43 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (-π[,]π) ⊆
ℂ) |
45 | 4 | recnd 11004 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
46 | | halfcn 12188 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℂ |
47 | 46 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
48 | 45, 47 | addcld 10995 |
. . . . . 6
⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ) |
49 | | ssid 3948 |
. . . . . . 7
⊢ ℂ
⊆ ℂ |
50 | 49 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂ ⊆
ℂ) |
51 | 44, 48, 50 | constcncfg 43384 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ (-π[,]π) ↦ (𝑁 + (1 / 2))) ∈
((-π[,]π)–cn→ℂ)) |
52 | 44, 50 | idcncfg 43385 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ (-π[,]π) ↦ 𝑠) ∈
((-π[,]π)–cn→ℂ)) |
53 | 51, 52 | mulcncf 24608 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ (-π[,]π) ↦ ((𝑁 + (1 / 2)) · 𝑠)) ∈
((-π[,]π)–cn→ℂ)) |
54 | | ssid 3948 |
. . . . 5
⊢
(-π[,]π) ⊆ (-π[,]π) |
55 | 54 | a1i 11 |
. . . 4
⊢ (𝜑 → (-π[,]π) ⊆
(-π[,]π)) |
56 | 42 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ⊆
ℂ) |
57 | 16, 53, 55, 56, 15 | cncfmptssg 43383 |
. . 3
⊢ (𝜑 → (𝑠 ∈ (-π[,]π) ↦ ((𝑁 + (1 / 2)) · 𝑠)) ∈
((-π[,]π)–cn→ℝ)) |
58 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → (sin ↾ ℝ)
∈ (ℝ–cn→ℝ)) |
59 | 57, 58 | cncfco 24068 |
. 2
⊢ (𝜑 → ((sin ↾ ℝ)
∘ (𝑠 ∈
(-π[,]π) ↦ ((𝑁
+ (1 / 2)) · 𝑠)))
∈ ((-π[,]π)–cn→ℝ)) |
60 | 41, 59 | eqeltrd 2841 |
1
⊢ (𝜑 → 𝑆 ∈ ((-π[,]π)–cn→ℝ)) |