fourierdlem56

Description: Derivative of the K function on an interval not containing ' 0 '. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem56.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
	fourierdlem56.a	$⊢ φ \to (A, B) \subseteq [- π, π] ∖ \{0\}$
	fourierdlem56.r4	$⊢ (φ \land s \in (A, B)) \to s \neq 0$
Assertion	fourierdlem56	$⊢ φ \to \frac{d (s \in (A, B)⟼ K (s))}{d_{ℝ} s} = (s \in (A, B) ⟼ \frac{\frac{\sin (\frac{s}{2}) - (\frac{\cos (\frac{s}{2})}{2}) s}{{\sin (\frac{s}{2})}^{2}}}{2})$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem56.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
2		fourierdlem56.a	$⊢ φ \to (A, B) \subseteq [- π, π] ∖ \{0\}$
3		fourierdlem56.r4	$⊢ (φ \land s \in (A, B)) \to s \neq 0$
4	2	difss2d	$⊢ φ \to (A, B) \subseteq [- π, π]$
5	4	sselda	$⊢ (φ \land s \in (A, B)) \to s \in [- π, π]$
6		1ex	$⊢ 1 \in V$
7		ovex	$⊢ \frac{s}{2 \sin (\frac{s}{2})} \in V$
8	6 7	ifex	$⊢ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) \in V$
9	8	a1i	$⊢ (φ \land s \in (A, B)) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) \in V$
10	1	fvmpt2	$⊢ (s \in [- π, π] \land if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) \in V) \to K (s) = if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})$
11	5 9 10	syl2anc	$⊢ (φ \land s \in (A, B)) \to K (s) = if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})$
12	3	neneqd	$⊢ (φ \land s \in (A, B)) \to \neg s = 0$
13	12	iffalsed	$⊢ (φ \land s \in (A, B)) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) = \frac{s}{2 \sin (\frac{s}{2})}$
14		elioore	$⊢ s \in (A, B) \to s \in ℝ$
15	14	adantl	$⊢ (φ \land s \in (A, B)) \to s \in ℝ$
16	15	recnd	$⊢ (φ \land s \in (A, B)) \to s \in ℂ$
17	16	halfcld	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2} \in ℂ$
18	17	sincld	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \in ℂ$
19		2cnd	$⊢ (φ \land s \in (A, B)) \to 2 \in ℂ$
20		fourierdlem44	$⊢ (s \in [- π, π] \land s \neq 0) \to \sin (\frac{s}{2}) \neq 0$
21	5 3 20	syl2anc	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \neq 0$
22		2ne0	$⊢ 2 \neq 0$
23	22	a1i	$⊢ (φ \land s \in (A, B)) \to 2 \neq 0$
24	16 18 19 21 23	divdiv1d	$⊢ (φ \land s \in (A, B)) \to \frac{\frac{s}{\sin (\frac{s}{2})}}{2} = \frac{s}{\sin (\frac{s}{2}) \cdot 2}$
25	18 19	mulcomd	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \cdot 2 = 2 \sin (\frac{s}{2})$
26	25	oveq2d	$⊢ (φ \land s \in (A, B)) \to \frac{s}{\sin (\frac{s}{2}) \cdot 2} = \frac{s}{2 \sin (\frac{s}{2})}$
27	24 26	eqtr2d	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2 \sin (\frac{s}{2})} = \frac{\frac{s}{\sin (\frac{s}{2})}}{2}$
28	11 13 27	3eqtrd	$⊢ (φ \land s \in (A, B)) \to K (s) = \frac{\frac{s}{\sin (\frac{s}{2})}}{2}$
29	28	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ K (s)) = (s \in (A, B) ⟼ \frac{\frac{s}{\sin (\frac{s}{2})}}{2})$
30	29	oveq2d	$⊢ φ \to \frac{d (s \in (A, B)⟼ K (s))}{d_{ℝ} s} = \frac{d (s \in (A, B)⟼ \frac{\frac{s}{\sin (\frac{s}{2})}}{2})}{d_{ℝ} s}$
31		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
32	31	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
33	16 18 21	divcld	$⊢ (φ \land s \in (A, B)) \to \frac{s}{\sin (\frac{s}{2})} \in ℂ$
34		1red	$⊢ (φ \land s \in (A, B)) \to 1 \in ℝ$
35	15	rehalfcld	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2} \in ℝ$
36	35	resincld	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \in ℝ$
37	34 36	remulcld	$⊢ (φ \land s \in (A, B)) \to 1 \sin (\frac{s}{2}) \in ℝ$
38	35	recoscld	$⊢ (φ \land s \in (A, B)) \to \cos (\frac{s}{2}) \in ℝ$
39	34	rehalfcld	$⊢ (φ \land s \in (A, B)) \to \frac{1}{2} \in ℝ$
40	38 39	remulcld	$⊢ (φ \land s \in (A, B)) \to \cos (\frac{s}{2}) (\frac{1}{2}) \in ℝ$
41	40 15	remulcld	$⊢ (φ \land s \in (A, B)) \to \cos (\frac{s}{2}) (\frac{1}{2}) s \in ℝ$
42	37 41	resubcld	$⊢ (φ \land s \in (A, B)) \to 1 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (\frac{1}{2}) s \in ℝ$
43	36	resqcld	$⊢ (φ \land s \in (A, B)) \to {\sin (\frac{s}{2})}^{2} \in ℝ$
44		2z	$⊢ 2 \in ℤ$
45	44	a1i	$⊢ (φ \land s \in (A, B)) \to 2 \in ℤ$
46	18 21 45	expne0d	$⊢ (φ \land s \in (A, B)) \to {\sin (\frac{s}{2})}^{2} \neq 0$
47	42 43 46	redivcld	$⊢ (φ \land s \in (A, B)) \to \frac{1 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (\frac{1}{2}) s}{{\sin (\frac{s}{2})}^{2}} \in ℝ$
48		1cnd	$⊢ (φ \land s \in (A, B)) \to 1 \in ℂ$
49		recn	$⊢ s \in ℝ \to s \in ℂ$
50	49	adantl	$⊢ (φ \land s \in ℝ) \to s \in ℂ$
51		1red	$⊢ (φ \land s \in ℝ) \to 1 \in ℝ$
52	32	dvmptid	$⊢ φ \to \frac{d (s \in ℝ⟼ s)}{d_{ℝ} s} = (s \in ℝ ⟼ 1)$
53		ioossre	$⊢ (A, B) \subseteq ℝ$
54	53	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
55		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
56	55	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
57		iooretop	$⊢ (A, B) \in topGen (ran (.))$
58	57	a1i	$⊢ φ \to (A, B) \in topGen (ran (.))$
59	32 50 51 52 54 56 55 58	dvmptres	$⊢ φ \to \frac{d (s \in (A, B)⟼ s)}{d_{ℝ} s} = (s \in (A, B) ⟼ 1)$
60		elsni	$⊢ \sin (\frac{s}{2}) \in \{0\} \to \sin (\frac{s}{2}) = 0$
61	60	necon3ai	$⊢ \sin (\frac{s}{2}) \neq 0 \to \neg \sin (\frac{s}{2}) \in \{0\}$
62	21 61	syl	$⊢ (φ \land s \in (A, B)) \to \neg \sin (\frac{s}{2}) \in \{0\}$
63	18 62	eldifd	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \in (ℂ ∖ \{0\})$
64	17	coscld	$⊢ (φ \land s \in (A, B)) \to \cos (\frac{s}{2}) \in ℂ$
65	48	halfcld	$⊢ (φ \land s \in (A, B)) \to \frac{1}{2} \in ℂ$
66	64 65	mulcld	$⊢ (φ \land s \in (A, B)) \to \cos (\frac{s}{2}) (\frac{1}{2}) \in ℂ$
67		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
68	67	a1i	$⊢ φ \to ℂ \in \{ℝ, ℂ\}$
69		sinf	$⊢ \sin : ℂ ⟶ ℂ$
70	69	a1i	$⊢ φ \to \sin : ℂ ⟶ ℂ$
71	70	ffvelcdmda	$⊢ (φ \land x \in ℂ) \to \sin x \in ℂ$
72		cosf	$⊢ \cos : ℂ ⟶ ℂ$
73	72	a1i	$⊢ φ \to \cos : ℂ ⟶ ℂ$
74	73	ffvelcdmda	$⊢ (φ \land x \in ℂ) \to \cos x \in ℂ$
75		2cnd	$⊢ φ \to 2 \in ℂ$
76	22	a1i	$⊢ φ \to 2 \neq 0$
77	32 16 34 59 75 76	dvmptdivc	$⊢ φ \to \frac{d (s \in (A, B)⟼ \frac{s}{2})}{d_{ℝ} s} = (s \in (A, B) ⟼ \frac{1}{2})$
78		ffn	$⊢ \sin : ℂ ⟶ ℂ \to \sin Fn ℂ$
79	69 78	ax-mp	$⊢ \sin Fn ℂ$
80		dffn5	$⊢ \sin Fn ℂ \leftrightarrow \sin = (x \in ℂ ⟼ \sin x)$
81	79 80	mpbi	$⊢ \sin = (x \in ℂ ⟼ \sin x)$
82	81	eqcomi	$⊢ (x \in ℂ ⟼ \sin x) = \sin$
83	82	oveq2i	$⊢ \frac{d (x \in ℂ⟼ \sin x)}{d_{ℂ} x} = ℂ D \sin$
84		dvsin	$⊢ ℂ D \sin = \cos$
85		ffn	$⊢ \cos : ℂ ⟶ ℂ \to \cos Fn ℂ$
86	72 85	ax-mp	$⊢ \cos Fn ℂ$
87		dffn5	$⊢ \cos Fn ℂ \leftrightarrow \cos = (x \in ℂ ⟼ \cos x)$
88	86 87	mpbi	$⊢ \cos = (x \in ℂ ⟼ \cos x)$
89	83 84 88	3eqtri	$⊢ \frac{d (x \in ℂ⟼ \sin x)}{d_{ℂ} x} = (x \in ℂ ⟼ \cos x)$
90	89	a1i	$⊢ φ \to \frac{d (x \in ℂ⟼ \sin x)}{d_{ℂ} x} = (x \in ℂ ⟼ \cos x)$
91		fveq2	$⊢ x = \frac{s}{2} \to \sin x = \sin (\frac{s}{2})$
92		fveq2	$⊢ x = \frac{s}{2} \to \cos x = \cos (\frac{s}{2})$
93	32 68 17 39 71 74 77 90 91 92	dvmptco	$⊢ φ \to \frac{d (s \in (A, B)⟼ \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ \cos (\frac{s}{2}) (\frac{1}{2}))$
94	32 16 48 59 63 66 93	dvmptdiv	$⊢ φ \to \frac{d (s \in (A, B)⟼ \frac{s}{\sin (\frac{s}{2})})}{d_{ℝ} s} = (s \in (A, B) ⟼ \frac{1 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (\frac{1}{2}) s}{{\sin (\frac{s}{2})}^{2}})$
95	32 33 47 94 75 76	dvmptdivc	$⊢ φ \to \frac{d (s \in (A, B)⟼ \frac{\frac{s}{\sin (\frac{s}{2})}}{2})}{d_{ℝ} s} = (s \in (A, B) ⟼ \frac{\frac{1 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (\frac{1}{2}) s}{{\sin (\frac{s}{2})}^{2}}}{2})$
96	14	recnd	$⊢ s \in (A, B) \to s \in ℂ$
97	96	halfcld	$⊢ s \in (A, B) \to \frac{s}{2} \in ℂ$
98	97	sincld	$⊢ s \in (A, B) \to \sin (\frac{s}{2}) \in ℂ$
99	98	mullidd	$⊢ s \in (A, B) \to 1 \sin (\frac{s}{2}) = \sin (\frac{s}{2})$
100	97	coscld	$⊢ s \in (A, B) \to \cos (\frac{s}{2}) \in ℂ$
101		2cnd	$⊢ s \in (A, B) \to 2 \in ℂ$
102	22	a1i	$⊢ s \in (A, B) \to 2 \neq 0$
103	100 101 102	divrecd	$⊢ s \in (A, B) \to \frac{\cos (\frac{s}{2})}{2} = \cos (\frac{s}{2}) (\frac{1}{2})$
104	103	eqcomd	$⊢ s \in (A, B) \to \cos (\frac{s}{2}) (\frac{1}{2}) = \frac{\cos (\frac{s}{2})}{2}$
105	104	oveq1d	$⊢ s \in (A, B) \to \cos (\frac{s}{2}) (\frac{1}{2}) s = (\frac{\cos (\frac{s}{2})}{2}) s$
106	99 105	oveq12d	$⊢ s \in (A, B) \to 1 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (\frac{1}{2}) s = \sin (\frac{s}{2}) - (\frac{\cos (\frac{s}{2})}{2}) s$
107	106	oveq1d	$⊢ s \in (A, B) \to \frac{1 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (\frac{1}{2}) s}{{\sin (\frac{s}{2})}^{2}} = \frac{\sin (\frac{s}{2}) - (\frac{\cos (\frac{s}{2})}{2}) s}{{\sin (\frac{s}{2})}^{2}}$
108	107	oveq1d	$⊢ s \in (A, B) \to \frac{\frac{1 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (\frac{1}{2}) s}{{\sin (\frac{s}{2})}^{2}}}{2} = \frac{\frac{\sin (\frac{s}{2}) - (\frac{\cos (\frac{s}{2})}{2}) s}{{\sin (\frac{s}{2})}^{2}}}{2}$
109	108	mpteq2ia	$⊢ (s \in (A, B) ⟼ \frac{\frac{1 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (\frac{1}{2}) s}{{\sin (\frac{s}{2})}^{2}}}{2}) = (s \in (A, B) ⟼ \frac{\frac{\sin (\frac{s}{2}) - (\frac{\cos (\frac{s}{2})}{2}) s}{{\sin (\frac{s}{2})}^{2}}}{2})$
110	109	a1i	$⊢ φ \to (s \in (A, B) ⟼ \frac{\frac{1 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (\frac{1}{2}) s}{{\sin (\frac{s}{2})}^{2}}}{2}) = (s \in (A, B) ⟼ \frac{\frac{\sin (\frac{s}{2}) - (\frac{\cos (\frac{s}{2})}{2}) s}{{\sin (\frac{s}{2})}^{2}}}{2})$
111	30 95 110	3eqtrd	$⊢ φ \to \frac{d (s \in (A, B)⟼ K (s))}{d_{ℝ} s} = (s \in (A, B) ⟼ \frac{\frac{\sin (\frac{s}{2}) - (\frac{\cos (\frac{s}{2})}{2}) s}{{\sin (\frac{s}{2})}^{2}}}{2})$

Metamath Proof Explorer

Theorem fourierdlem56

Proof