Theorem fourierdlem18

Description: The function S is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem18.n	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
	fourierdlem18.s	⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
Assertion	fourierdlem18	⊢ ( 𝜑 → 𝑆 ∈ ( ( - π [,] π ) –cn→ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem18.n	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
2		fourierdlem18.s	⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
3		resincncf	⊢ ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ )
4		cncff	⊢ ( ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) → ( sin ↾ ℝ ) : ℝ ⟶ ℝ )
5	3 4	ax-mp	⊢ ( sin ↾ ℝ ) : ℝ ⟶ ℝ
6		halfre	⊢ ( 1 / 2 ) ∈ ℝ
7	6	a1i	⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
8	1 7	readdcld	⊢ ( 𝜑 → ( 𝑁 + ( 1 / 2 ) ) ∈ ℝ )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℝ )
10		pire	⊢ π ∈ ℝ
11	10	renegcli	⊢ - π ∈ ℝ
12		iccssre	⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
13	11 10 12	mp2an	⊢ ( - π [,] π ) ⊆ ℝ
14	13	sseli	⊢ ( 𝑠 ∈ ( - π [,] π ) → 𝑠 ∈ ℝ )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ℝ )
16	9 15	remulcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ∈ ℝ )
17		eqid	⊢ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) )
18	16 17	fmptd	⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) : ( - π [,] π ) ⟶ ℝ )
19		fcompt	⊢ ( ( ( sin ↾ ℝ ) : ℝ ⟶ ℝ ∧ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) : ( - π [,] π ) ⟶ ℝ ) → ( ( sin ↾ ℝ ) ∘ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) = ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) ) ) )
20	5 18 19	sylancr	⊢ ( 𝜑 → ( ( sin ↾ ℝ ) ∘ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) = ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) ) ) )
21		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
22		oveq2	⊢ ( 𝑠 = 𝑥 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) )
23	22	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) ∧ 𝑠 = 𝑥 ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) )
24		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → 𝑥 ∈ ( - π [,] π ) )
25	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℝ )
26	13 24	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → 𝑥 ∈ ℝ )
27	25 26	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ∈ ℝ )
28	21 23 24 27	fvmptd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) )
29	28	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( ( sin ↾ ℝ ) ‘ ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) ) = ( ( sin ↾ ℝ ) ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) )
30	29	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ) )
31		fvres	⊢ ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ∈ ℝ → ( ( sin ↾ ℝ ) ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) )
32	27 31	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( ( sin ↾ ℝ ) ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) )
33	32	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ) = ( 𝑥 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ) )
34		oveq2	⊢ ( 𝑥 = 𝑠 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) )
35	34	fveq2d	⊢ ( 𝑥 = 𝑠 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
36	35	cbvmptv	⊢ ( 𝑥 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ) = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
37	36	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ) = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) )
38	30 33 37	3eqtrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) ) ) = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) )
39	2	eqcomi	⊢ ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) = 𝑆
40	39	a1i	⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) = 𝑆 )
41	20 38 40	3eqtrrd	⊢ ( 𝜑 → 𝑆 = ( ( sin ↾ ℝ ) ∘ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) )
42		ax-resscn	⊢ ℝ ⊆ ℂ
43	13 42	sstri	⊢ ( - π [,] π ) ⊆ ℂ
44	43	a1i	⊢ ( 𝜑 → ( - π [,] π ) ⊆ ℂ )
45	1	recnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
46		halfcn	⊢ ( 1 / 2 ) ∈ ℂ
47	46	a1i	⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
48	45 47	addcld	⊢ ( 𝜑 → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
49		ssid	⊢ ℂ ⊆ ℂ
50	49	a1i	⊢ ( 𝜑 → ℂ ⊆ ℂ )
51	44 48 50	constcncfg	⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ ( 𝑁 + ( 1 / 2 ) ) ) ∈ ( ( - π [,] π ) –cn→ ℂ ) )
52	44 50	idcncfg	⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ 𝑠 ) ∈ ( ( - π [,] π ) –cn→ ℂ ) )
53	51 52	mulcncf	⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℂ ) )
54		ssid	⊢ ( - π [,] π ) ⊆ ( - π [,] π )
55	54	a1i	⊢ ( 𝜑 → ( - π [,] π ) ⊆ ( - π [,] π ) )
56	42	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
57	17 53 55 56 16	cncfmptssg	⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℝ ) )
58	3	a1i	⊢ ( 𝜑 → ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) )
59	57 58	cncfco	⊢ ( 𝜑 → ( ( sin ↾ ℝ ) ∘ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) ∈ ( ( - π [,] π ) –cn→ ℝ ) )
60	41 59	eqeltrd	⊢ ( 𝜑 → 𝑆 ∈ ( ( - π [,] π ) –cn→ ℝ ) )