fourierdlem18

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

	Ref	Expression
Hypotheses	fourierdlem18.n	$⊢ φ \to N \in ℝ$
	fourierdlem18.s	$⊢ S = (s \in [- π, π] ⟼ \sin (N + (\frac{1}{2})) s)$
Assertion	fourierdlem18	$⊢ φ \to S : [- π, π] \underset{cn}{⟶} ℝ$

Proof

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

Metamath Proof Explorer

Theorem fourierdlem18

Proof