fourierdlem58

Description: The derivative of K is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem58.k	$⊢ K = (s \in A ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
	fourierdlem58.ass	$⊢ φ \to A \subseteq [- π, π]$
	fourierdlem58.0nA	$⊢ φ \to \neg 0 \in A$
	fourierdlem58.4	$⊢ φ \to A \in topGen (ran (.))$
Assertion	fourierdlem58	$⊢ φ \to K_{ℝ}^{'} : A \underset{cn}{⟶} ℝ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem58.k	$⊢ K = (s \in A ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
2		fourierdlem58.ass	$⊢ φ \to A \subseteq [- π, π]$
3		fourierdlem58.0nA	$⊢ φ \to \neg 0 \in A$
4		fourierdlem58.4	$⊢ φ \to A \in topGen (ran (.))$
5		pire	$⊢ π \in ℝ$
6	5	a1i	$⊢ (φ \land s \in A) \to π \in ℝ$
7	6	renegcld	$⊢ (φ \land s \in A) \to - π \in ℝ$
8	7 6	iccssred	$⊢ (φ \land s \in A) \to [- π, π] \subseteq ℝ$
9	2	sselda	$⊢ (φ \land s \in A) \to s \in [- π, π]$
10	8 9	sseldd	$⊢ (φ \land s \in A) \to s \in ℝ$
11		2re	$⊢ 2 \in ℝ$
12	11	a1i	$⊢ (φ \land s \in A) \to 2 \in ℝ$
13	10	rehalfcld	$⊢ (φ \land s \in A) \to \frac{s}{2} \in ℝ$
14	13	resincld	$⊢ (φ \land s \in A) \to \sin (\frac{s}{2}) \in ℝ$
15	12 14	remulcld	$⊢ (φ \land s \in A) \to 2 \sin (\frac{s}{2}) \in ℝ$
16		2cnd	$⊢ (φ \land s \in A) \to 2 \in ℂ$
17	10	recnd	$⊢ (φ \land s \in A) \to s \in ℂ$
18	17	halfcld	$⊢ (φ \land s \in A) \to \frac{s}{2} \in ℂ$
19	18	sincld	$⊢ (φ \land s \in A) \to \sin (\frac{s}{2}) \in ℂ$
20		2ne0	$⊢ 2 \neq 0$
21	20	a1i	$⊢ (φ \land s \in A) \to 2 \neq 0$
22		eqcom	$⊢ s = 0 \leftrightarrow 0 = s$
23	22	bilani	$⊢ (s \in A \land s = 0) \to 0 = s$
24		simpl	$⊢ (s \in A \land s = 0) \to s \in A$
25	23 24	eqeltrd	$⊢ (s \in A \land s = 0) \to 0 \in A$
26	25	adantll	$⊢ ((φ \land s \in A) \land s = 0) \to 0 \in A$
27	3	ad2antrr	$⊢ ((φ \land s \in A) \land s = 0) \to \neg 0 \in A$
28	26 27	pm2.65da	$⊢ (φ \land s \in A) \to \neg s = 0$
29	28	neqned	$⊢ (φ \land s \in A) \to s \neq 0$
30		fourierdlem44	$⊢ (s \in [- π, π] \land s \neq 0) \to \sin (\frac{s}{2}) \neq 0$
31	9 29 30	syl2anc	$⊢ (φ \land s \in A) \to \sin (\frac{s}{2}) \neq 0$
32	16 19 21 31	mulne0d	$⊢ (φ \land s \in A) \to 2 \sin (\frac{s}{2}) \neq 0$
33	10 15 32	redivcld	$⊢ (φ \land s \in A) \to \frac{s}{2 \sin (\frac{s}{2})} \in ℝ$
34	33 1	fmptd	$⊢ φ \to K : A ⟶ ℝ$
35	5	a1i	$⊢ φ \to π \in ℝ$
36	35	renegcld	$⊢ φ \to - π \in ℝ$
37	36 35	iccssred	$⊢ φ \to [- π, π] \subseteq ℝ$
38	2 37	sstrd	$⊢ φ \to A \subseteq ℝ$
39		dvfre	$⊢ (K : A ⟶ ℝ \land A \subseteq ℝ) \to K_{ℝ}^{'} : dom K_{ℝ}^{'} ⟶ ℝ$
40	34 38 39	syl2anc	$⊢ φ \to K_{ℝ}^{'} : dom K_{ℝ}^{'} ⟶ ℝ$
41		eqidd	$⊢ φ \to (s \in A ⟼ s) = (s \in A ⟼ s)$
42		eqidd	$⊢ φ \to (s \in A ⟼ 2 \sin (\frac{s}{2})) = (s \in A ⟼ 2 \sin (\frac{s}{2}))$
43	4 10 15 41 42	offval2	$⊢ φ \to (s \in A ⟼ s) \div_{f} (s \in A ⟼ 2 \sin (\frac{s}{2})) = (s \in A ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
44	1 43	eqtr4id	$⊢ φ \to K = (s \in A ⟼ s) \div_{f} (s \in A ⟼ 2 \sin (\frac{s}{2}))$
45	44	oveq2d	$⊢ φ \to ℝ D K = ℝ D ((s \in A ⟼ s) \div_{f} (s \in A ⟼ 2 \sin (\frac{s}{2})))$
46		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
47	46	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
48		eqid	$⊢ (s \in A ⟼ s) = (s \in A ⟼ s)$
49	17 48	fmptd	$⊢ φ \to (s \in A ⟼ s) : A ⟶ ℂ$
50	16 19	mulcld	$⊢ (φ \land s \in A) \to 2 \sin (\frac{s}{2}) \in ℂ$
51	32	neneqd	$⊢ (φ \land s \in A) \to \neg 2 \sin (\frac{s}{2}) = 0$
52		elsng	$⊢ 2 \sin (\frac{s}{2}) \in ℝ \to (2 \sin (\frac{s}{2}) \in \{0\} \leftrightarrow 2 \sin (\frac{s}{2}) = 0)$
53	15 52	syl	$⊢ (φ \land s \in A) \to (2 \sin (\frac{s}{2}) \in \{0\} \leftrightarrow 2 \sin (\frac{s}{2}) = 0)$
54	51 53	mtbird	$⊢ (φ \land s \in A) \to \neg 2 \sin (\frac{s}{2}) \in \{0\}$
55	50 54	eldifd	$⊢ (φ \land s \in A) \to 2 \sin (\frac{s}{2}) \in (ℂ ∖ \{0\})$
56		eqid	$⊢ (s \in A ⟼ 2 \sin (\frac{s}{2})) = (s \in A ⟼ 2 \sin (\frac{s}{2}))$
57	55 56	fmptd	$⊢ φ \to (s \in A ⟼ 2 \sin (\frac{s}{2})) : A ⟶ ℂ ∖ \{0\}$
58		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
59	4 58	eleqtrdi	$⊢ φ \to A \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
60	47 59	dvmptidg	$⊢ φ \to \frac{d (s \in A⟼ s)}{d_{ℝ} s} = (s \in A ⟼ 1)$
61		ax-resscn	$⊢ ℝ \subseteq ℂ$
62	61	a1i	$⊢ φ \to ℝ \subseteq ℂ$
63	38 62	sstrd	$⊢ φ \to A \subseteq ℂ$
64		1cnd	$⊢ φ \to 1 \in ℂ$
65		ssid	$⊢ ℂ \subseteq ℂ$
66	65	a1i	$⊢ φ \to ℂ \subseteq ℂ$
67	63 64 66	constcncfg	$⊢ φ \to (s \in A ⟼ 1) : A \underset{cn}{⟶} ℂ$
68	60 67	eqeltrd	$⊢ φ \to \frac{d (s \in A⟼ s)}{d_{ℝ} s} : A \underset{cn}{⟶} ℂ$
69	38	resmptd	$⊢ φ \to {(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{A} = (s \in A ⟼ 2 \sin (\frac{s}{2}))$
70	69	eqcomd	$⊢ φ \to (s \in A ⟼ 2 \sin (\frac{s}{2})) = {(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{A}$
71	70	oveq2d	$⊢ φ \to \frac{d (s \in A⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = ℝ D ({(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{A})$
72		eqid	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) = (s \in ℝ ⟼ 2 \sin (\frac{s}{2}))$
73		2cnd	$⊢ s \in ℝ \to 2 \in ℂ$
74		recn	$⊢ s \in ℝ \to s \in ℂ$
75	74	halfcld	$⊢ s \in ℝ \to \frac{s}{2} \in ℂ$
76	75	sincld	$⊢ s \in ℝ \to \sin (\frac{s}{2}) \in ℂ$
77	73 76	mulcld	$⊢ s \in ℝ \to 2 \sin (\frac{s}{2}) \in ℂ$
78	72 77	fmpti	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) : ℝ ⟶ ℂ$
79	78	a1i	$⊢ φ \to (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) : ℝ ⟶ ℂ$
80		ssid	$⊢ ℝ \subseteq ℝ$
81	80	a1i	$⊢ φ \to ℝ \subseteq ℝ$
82		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
83	82 58	dvres	$⊢ ((ℝ \subseteq ℂ \land (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) : ℝ ⟶ ℂ) \land (ℝ \subseteq ℝ \land A \subseteq ℝ)) \to ℝ D ({(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{A}) = {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) (A)}$
84	62 79 81 38 83	syl22anc	$⊢ φ \to ℝ D ({(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{A}) = {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) (A)}$
85		retop	$⊢ topGen (ran (.)) \in Top$
86	85	a1i	$⊢ φ \to topGen (ran (.)) \in Top$
87		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
88	87	isopn3	$⊢ (topGen (ran (.)) \in Top \land A \subseteq ℝ) \to (A \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (A) = A)$
89	86 38 88	syl2anc	$⊢ φ \to (A \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (A) = A)$
90	4 89	mpbid	$⊢ φ \to int (topGen (ran (.))) (A) = A$
91	90	reseq2d	$⊢ φ \to {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) (A)} = {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{A}$
92		resmpt	$⊢ ℝ \subseteq ℂ \to {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ} = (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s)$
93	61 92	ax-mp	$⊢ {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ} = (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s)$
94		id	$⊢ s \in ℂ \to s \in ℂ$
95		2cnd	$⊢ s \in ℂ \to 2 \in ℂ$
96	20	a1i	$⊢ s \in ℂ \to 2 \neq 0$
97	94 95 96	divrec2d	$⊢ s \in ℂ \to \frac{s}{2} = (\frac{1}{2}) s$
98	97	eqcomd	$⊢ s \in ℂ \to (\frac{1}{2}) s = \frac{s}{2}$
99	74 98	syl	$⊢ s \in ℝ \to (\frac{1}{2}) s = \frac{s}{2}$
100	99	fveq2d	$⊢ s \in ℝ \to \sin (\frac{1}{2}) s = \sin (\frac{s}{2})$
101	100	oveq2d	$⊢ s \in ℝ \to 2 \sin (\frac{1}{2}) s = 2 \sin (\frac{s}{2})$
102	101	mpteq2ia	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s) = (s \in ℝ ⟼ 2 \sin (\frac{s}{2}))$
103	93 102	eqtr2i	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) = {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ}$
104	103	oveq2i	$⊢ \frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = ℝ D ({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ})$
105		eqid	$⊢ (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) = (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s)$
106		halfcn	$⊢ \frac{1}{2} \in ℂ$
107	106	a1i	$⊢ s \in ℂ \to \frac{1}{2} \in ℂ$
108	107 94	mulcld	$⊢ s \in ℂ \to (\frac{1}{2}) s \in ℂ$
109	108	sincld	$⊢ s \in ℂ \to \sin (\frac{1}{2}) s \in ℂ$
110	95 109	mulcld	$⊢ s \in ℂ \to 2 \sin (\frac{1}{2}) s \in ℂ$
111	105 110	fmpti	$⊢ (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) : ℂ ⟶ ℂ$
112		2cn	$⊢ 2 \in ℂ$
113		dvasinbx	$⊢ (2 \in ℂ \land \frac{1}{2} \in ℂ) \to \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
114	112 106 113	mp2an	$⊢ \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
115	112 20	recidi	$⊢ 2 (\frac{1}{2}) = 1$
116	115	a1i	$⊢ s \in ℂ \to 2 (\frac{1}{2}) = 1$
117	98	fveq2d	$⊢ s \in ℂ \to \cos (\frac{1}{2}) s = \cos (\frac{s}{2})$
118	116 117	oveq12d	$⊢ s \in ℂ \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) s = 1 \cos (\frac{s}{2})$
119		halfcl	$⊢ s \in ℂ \to \frac{s}{2} \in ℂ$
120	119	coscld	$⊢ s \in ℂ \to \cos (\frac{s}{2}) \in ℂ$
121	120	mullidd	$⊢ s \in ℂ \to 1 \cos (\frac{s}{2}) = \cos (\frac{s}{2})$
122	118 121	eqtrd	$⊢ s \in ℂ \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) s = \cos (\frac{s}{2})$
123	122	mpteq2ia	$⊢ (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) = (s \in ℂ ⟼ \cos (\frac{s}{2}))$
124	114 123	eqtri	$⊢ \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = (s \in ℂ ⟼ \cos (\frac{s}{2}))$
125	124	dmeqi	$⊢ dom \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = dom (s \in ℂ ⟼ \cos (\frac{s}{2}))$
126		dmmptg	$⊢ \forall s \in ℂ \cos (\frac{s}{2}) \in ℂ \to dom (s \in ℂ ⟼ \cos (\frac{s}{2})) = ℂ$
127	126 120	mprg	$⊢ dom (s \in ℂ ⟼ \cos (\frac{s}{2})) = ℂ$
128	125 127	eqtri	$⊢ dom \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = ℂ$
129	61 128	sseqtrri	$⊢ ℝ \subseteq dom \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s}$
130		dvres3	$⊢ ((ℝ \in \{ℝ, ℂ\} \land (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) : ℂ ⟶ ℂ) \land (ℂ \subseteq ℂ \land ℝ \subseteq dom \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s})) \to ℝ D ({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ}) = {\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ}$
131	46 111 65 129 130	mp4an	$⊢ ℝ D ({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ}) = {\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ}$
132	124	reseq1i	$⊢ {\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ} = {(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}$
133	104 131 132	3eqtri	$⊢ \frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = {(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}$
134	133	reseq1i	$⊢ {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{A} = {({(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}) ↾}_{A}$
135	134	a1i	$⊢ φ \to {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{A} = {({(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}) ↾}_{A}$
136	38	resabs1d	$⊢ φ \to {({(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}) ↾}_{A} = {(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{A}$
137	63	resmptd	$⊢ φ \to {(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{A} = (s \in A ⟼ \cos (\frac{s}{2}))$
138	136 137	eqtrd	$⊢ φ \to {({(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}) ↾}_{A} = (s \in A ⟼ \cos (\frac{s}{2}))$
139	91 135 138	3eqtrd	$⊢ φ \to {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) (A)} = (s \in A ⟼ \cos (\frac{s}{2}))$
140	71 84 139	3eqtrd	$⊢ φ \to \frac{d (s \in A⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in A ⟼ \cos (\frac{s}{2}))$
141		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
142	141	a1i	$⊢ φ \to \cos : ℂ \underset{cn}{⟶} ℂ$
143	63 66	idcncfg	$⊢ φ \to (s \in A ⟼ s) : A \underset{cn}{⟶} ℂ$
144		2cnd	$⊢ φ \to 2 \in ℂ$
145	20	a1i	$⊢ φ \to 2 \neq 0$
146		eldifsn	$⊢ 2 \in (ℂ ∖ \{0\}) \leftrightarrow (2 \in ℂ \land 2 \neq 0)$
147	144 145 146	sylanbrc	$⊢ φ \to 2 \in (ℂ ∖ \{0\})$
148		difssd	$⊢ φ \to ℂ ∖ \{0\} \subseteq ℂ$
149	63 147 148	constcncfg	$⊢ φ \to (s \in A ⟼ 2) : A \underset{cn}{⟶} (ℂ ∖ \{0\})$
150	143 149	divcncf	$⊢ φ \to (s \in A ⟼ \frac{s}{2}) : A \underset{cn}{⟶} ℂ$
151	142 150	cncfmpt1f	$⊢ φ \to (s \in A ⟼ \cos (\frac{s}{2})) : A \underset{cn}{⟶} ℂ$
152	140 151	eqeltrd	$⊢ φ \to \frac{d (s \in A⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} : A \underset{cn}{⟶} ℂ$
153	47 49 57 68 152	dvdivcncf	$⊢ φ \to {((s \in A ⟼ s) \div_{f} (s \in A ⟼ 2 \sin (\frac{s}{2})))}_{ℝ}^{'} : A \underset{cn}{⟶} ℂ$
154	45 153	eqeltrd	$⊢ φ \to K_{ℝ}^{'} : A \underset{cn}{⟶} ℂ$
155		cncff	$⊢ K_{ℝ}^{'} : A \underset{cn}{⟶} ℂ \to K_{ℝ}^{'} : A ⟶ ℂ$
156		fdm	$⊢ K_{ℝ}^{'} : A ⟶ ℂ \to dom K_{ℝ}^{'} = A$
157	154 155 156	3syl	$⊢ φ \to dom K_{ℝ}^{'} = A$
158	157	feq2d	$⊢ φ \to (K_{ℝ}^{'} : dom K_{ℝ}^{'} ⟶ ℝ \leftrightarrow K_{ℝ}^{'} : A ⟶ ℝ)$
159	40 158	mpbid	$⊢ φ \to K_{ℝ}^{'} : A ⟶ ℝ$
160		cncfcdm	$⊢ (ℝ \subseteq ℂ \land K_{ℝ}^{'} : A \underset{cn}{⟶} ℂ) \to (K_{ℝ}^{'} : A \underset{cn}{⟶} ℝ \leftrightarrow K_{ℝ}^{'} : A ⟶ ℝ)$
161	62 154 160	syl2anc	$⊢ φ \to (K_{ℝ}^{'} : A \underset{cn}{⟶} ℝ \leftrightarrow K_{ℝ}^{'} : A ⟶ ℝ)$
162	159 161	mpbird	$⊢ φ \to K_{ℝ}^{'} : A \underset{cn}{⟶} ℝ$

Metamath Proof Explorer

Theorem fourierdlem58

Proof