fourierdlem57

Description: The derivative of O . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem57.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem57.xre	$⊢ φ \to X \in ℝ$
	fourierdlem57.a	$⊢ φ \to A \in ℝ$
	fourierdlem57.b	$⊢ φ \to B \in ℝ$
	fourierdlem57.fdv	$⊢ φ \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) ⟶ ℝ$
	fourierdlem57.ab	$⊢ φ \to (A, B) \subseteq [- π, π]$
	fourierdlem57.n0	$⊢ φ \to \neg 0 \in (A, B)$
	fourierdlem57.c	$⊢ φ \to C \in ℝ$
	fourierdlem57.o	$⊢ O = (s \in (A, B) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
Assertion	fourierdlem57	$⊢ ((φ \to (O_{ℝ}^{'} : (A, B) ⟶ ℝ \land ℝ D O = (s \in (A, B) ⟼ \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}}))) \land \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ \cos (\frac{s}{2})))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem57.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem57.xre	$⊢ φ \to X \in ℝ$
3		fourierdlem57.a	$⊢ φ \to A \in ℝ$
4		fourierdlem57.b	$⊢ φ \to B \in ℝ$
5		fourierdlem57.fdv	$⊢ φ \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) ⟶ ℝ$
6		fourierdlem57.ab	$⊢ φ \to (A, B) \subseteq [- π, π]$
7		fourierdlem57.n0	$⊢ φ \to \neg 0 \in (A, B)$
8		fourierdlem57.c	$⊢ φ \to C \in ℝ$
9		fourierdlem57.o	$⊢ O = (s \in (A, B) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
10	5	adantr	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) ⟶ ℝ$
11	2 3	readdcld	$⊢ φ \to X + A \in ℝ$
12	11	rexrd	$⊢ φ \to X + A \in ℝ^{*}$
13	12	adantr	$⊢ (φ \land s \in (A, B)) \to X + A \in ℝ^{*}$
14	2 4	readdcld	$⊢ φ \to X + B \in ℝ$
15	14	rexrd	$⊢ φ \to X + B \in ℝ^{*}$
16	15	adantr	$⊢ (φ \land s \in (A, B)) \to X + B \in ℝ^{*}$
17	2	adantr	$⊢ (φ \land s \in (A, B)) \to X \in ℝ$
18		elioore	$⊢ s \in (A, B) \to s \in ℝ$
19	18	adantl	$⊢ (φ \land s \in (A, B)) \to s \in ℝ$
20	17 19	readdcld	$⊢ (φ \land s \in (A, B)) \to X + s \in ℝ$
21	3	adantr	$⊢ (φ \land s \in (A, B)) \to A \in ℝ$
22	21	rexrd	$⊢ (φ \land s \in (A, B)) \to A \in ℝ^{*}$
23	4	rexrd	$⊢ φ \to B \in ℝ^{*}$
24	23	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ^{*}$
25		simpr	$⊢ (φ \land s \in (A, B)) \to s \in (A, B)$
26		ioogtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to A < s$
27	22 24 25 26	syl3anc	$⊢ (φ \land s \in (A, B)) \to A < s$
28	21 19 17 27	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + A < X + s$
29	4	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ$
30		iooltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to s < B$
31	22 24 25 30	syl3anc	$⊢ (φ \land s \in (A, B)) \to s < B$
32	19 29 17 31	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + s < X + B$
33	13 16 20 28 32	eliood	$⊢ (φ \land s \in (A, B)) \to X + s \in (X + A, X + B)$
34	10 33	ffvelcdmd	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) \in ℝ$
35		2re	$⊢ 2 \in ℝ$
36	35	a1i	$⊢ (φ \land s \in (A, B)) \to 2 \in ℝ$
37		rehalfcl	$⊢ s \in ℝ \to \frac{s}{2} \in ℝ$
38	19 37	syl	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2} \in ℝ$
39	38	resincld	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \in ℝ$
40	36 39	remulcld	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \in ℝ$
41	34 40	remulcld	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) \in ℝ$
42	38	recoscld	$⊢ (φ \land s \in (A, B)) \to \cos (\frac{s}{2}) \in ℝ$
43	1	adantr	$⊢ (φ \land s \in (A, B)) \to F : ℝ ⟶ ℝ$
44	43 20	ffvelcdmd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℝ$
45	8	adantr	$⊢ (φ \land s \in (A, B)) \to C \in ℝ$
46	44 45	resubcld	$⊢ (φ \land s \in (A, B)) \to F (X + s) - C \in ℝ$
47	42 46	remulcld	$⊢ (φ \land s \in (A, B)) \to \cos (\frac{s}{2}) (F (X + s) - C) \in ℝ$
48	41 47	resubcld	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C) \in ℝ$
49	40	resqcld	$⊢ (φ \land s \in (A, B)) \to {2 \sin (\frac{s}{2})}^{2} \in ℝ$
50		2cnd	$⊢ s \in ℝ \to 2 \in ℂ$
51	37	recnd	$⊢ s \in ℝ \to \frac{s}{2} \in ℂ$
52	51	sincld	$⊢ s \in ℝ \to \sin (\frac{s}{2}) \in ℂ$
53	50 52	mulcld	$⊢ s \in ℝ \to 2 \sin (\frac{s}{2}) \in ℂ$
54	19 53	syl	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \in ℂ$
55		2cnd	$⊢ (φ \land s \in (A, B)) \to 2 \in ℂ$
56	19 52	syl	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \in ℂ$
57		2ne0	$⊢ 2 \neq 0$
58	57	a1i	$⊢ (φ \land s \in (A, B)) \to 2 \neq 0$
59	6	sselda	$⊢ (φ \land s \in (A, B)) \to s \in [- π, π]$
60		eqcom	$⊢ s = 0 \leftrightarrow 0 = s$
61	60	bilani	$⊢ (s \in (A, B) \land s = 0) \to 0 = s$
62		simpl	$⊢ (s \in (A, B) \land s = 0) \to s \in (A, B)$
63	61 62	eqeltrd	$⊢ (s \in (A, B) \land s = 0) \to 0 \in (A, B)$
64	63	adantll	$⊢ ((φ \land s \in (A, B)) \land s = 0) \to 0 \in (A, B)$
65	7	ad2antrr	$⊢ ((φ \land s \in (A, B)) \land s = 0) \to \neg 0 \in (A, B)$
66	64 65	pm2.65da	$⊢ (φ \land s \in (A, B)) \to \neg s = 0$
67	66	neqned	$⊢ (φ \land s \in (A, B)) \to s \neq 0$
68		fourierdlem44	$⊢ (s \in [- π, π] \land s \neq 0) \to \sin (\frac{s}{2}) \neq 0$
69	59 67 68	syl2anc	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \neq 0$
70	55 56 58 69	mulne0d	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \neq 0$
71		2z	$⊢ 2 \in ℤ$
72	71	a1i	$⊢ (φ \land s \in (A, B)) \to 2 \in ℤ$
73	54 70 72	expne0d	$⊢ (φ \land s \in (A, B)) \to {2 \sin (\frac{s}{2})}^{2} \neq 0$
74	48 49 73	redivcld	$⊢ (φ \land s \in (A, B)) \to \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}} \in ℝ$
75		eqid	$⊢ (s \in (A, B) ⟼ \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}}) = (s \in (A, B) ⟼ \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}})$
76	74 75	fmptd	$⊢ φ \to (s \in (A, B) ⟼ \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}}) : (A, B) ⟶ ℝ$
77	9	a1i	$⊢ φ \to O = (s \in (A, B) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
78	77	oveq2d	$⊢ φ \to ℝ D O = \frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s}$
79		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
80	79	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
81	46	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) - C \in ℂ$
82	44	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℂ$
83		eqid	$⊢ ℝ D ({F ↾}_{(X + A, X + B)}) = ℝ D ({F ↾}_{(X + A, X + B)})$
84	1 2 3 4 83 5	fourierdlem28	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s))}{d_{ℝ} s} = (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s))$
85	45	recnd	$⊢ (φ \land s \in (A, B)) \to C \in ℂ$
86		0red	$⊢ (φ \land s \in (A, B)) \to 0 \in ℝ$
87		iooretop	$⊢ (A, B) \in topGen (ran (.))$
88		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
89	87 88	eleqtri	$⊢ (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
90	89	a1i	$⊢ φ \to (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
91	8	recnd	$⊢ φ \to C \in ℂ$
92	80 90 91	dvmptconst	$⊢ φ \to \frac{d (s \in (A, B)⟼ C)}{d_{ℝ} s} = (s \in (A, B) ⟼ 0)$
93	80 82 34 84 85 86 92	dvmptsub	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s) - C)}{d_{ℝ} s} = (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) - 0)$
94	34	recnd	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) \in ℂ$
95	94	subid1d	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) - 0 = {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)$
96	95	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) - 0) = (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s))$
97	93 96	eqtrd	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s) - C)}{d_{ℝ} s} = (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s))$
98		eldifsn	$⊢ 2 \sin (\frac{s}{2}) \in (ℂ ∖ \{0\}) \leftrightarrow (2 \sin (\frac{s}{2}) \in ℂ \land 2 \sin (\frac{s}{2}) \neq 0)$
99	54 70 98	sylanbrc	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \in (ℂ ∖ \{0\})$
100		recn	$⊢ s \in ℝ \to s \in ℂ$
101	57	a1i	$⊢ s \in ℝ \to 2 \neq 0$
102	100 50 101	divrec2d	$⊢ s \in ℝ \to \frac{s}{2} = (\frac{1}{2}) s$
103	102	eqcomd	$⊢ s \in ℝ \to (\frac{1}{2}) s = \frac{s}{2}$
104	18 103	syl	$⊢ s \in (A, B) \to (\frac{1}{2}) s = \frac{s}{2}$
105	104	fveq2d	$⊢ s \in (A, B) \to \cos (\frac{1}{2}) s = \cos (\frac{s}{2})$
106		halfcn	$⊢ \frac{1}{2} \in ℂ$
107	106	a1i	$⊢ s \in ℂ \to \frac{1}{2} \in ℂ$
108		id	$⊢ s \in ℂ \to s \in ℂ$
109	107 108	mulcld	$⊢ s \in ℂ \to (\frac{1}{2}) s \in ℂ$
110	109	coscld	$⊢ s \in ℂ \to \cos (\frac{1}{2}) s \in ℂ$
111	18 100 110	3syl	$⊢ s \in (A, B) \to \cos (\frac{1}{2}) s \in ℂ$
112	105 111	eqeltrrd	$⊢ s \in (A, B) \to \cos (\frac{s}{2}) \in ℂ$
113	112	adantl	$⊢ (φ \land s \in (A, B)) \to \cos (\frac{s}{2}) \in ℂ$
114		ioossre	$⊢ (A, B) \subseteq ℝ$
115		resmpt	$⊢ (A, B) \subseteq ℝ \to {(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{(A, B)} = (s \in (A, B) ⟼ 2 \sin (\frac{s}{2}))$
116	114 115	ax-mp	$⊢ {(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{(A, B)} = (s \in (A, B) ⟼ 2 \sin (\frac{s}{2}))$
117	116	eqcomi	$⊢ (s \in (A, B) ⟼ 2 \sin (\frac{s}{2})) = {(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{(A, B)}$
118	117	oveq2i	$⊢ \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = ℝ D ({(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{(A, B)})$
119		ax-resscn	$⊢ ℝ \subseteq ℂ$
120		eqid	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) = (s \in ℝ ⟼ 2 \sin (\frac{s}{2}))$
121	120 53	fmpti	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) : ℝ ⟶ ℂ$
122		ssid	$⊢ ℝ \subseteq ℝ$
123		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
124	123 88	dvres	$⊢ ((ℝ \subseteq ℂ \land (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) : ℝ ⟶ ℂ) \land (ℝ \subseteq ℝ \land (A, B) \subseteq ℝ)) \to ℝ D ({(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{(A, B)}) = {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) ((A, B))}$
125	119 121 122 114 124	mp4an	$⊢ ℝ D ({(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{(A, B)}) = {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) ((A, B))}$
126		resmpt	$⊢ ℝ \subseteq ℂ \to {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ} = (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s)$
127	119 126	ax-mp	$⊢ {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ} = (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s)$
128	103	fveq2d	$⊢ s \in ℝ \to \sin (\frac{1}{2}) s = \sin (\frac{s}{2})$
129	128	oveq2d	$⊢ s \in ℝ \to 2 \sin (\frac{1}{2}) s = 2 \sin (\frac{s}{2})$
130	129	mpteq2ia	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s) = (s \in ℝ ⟼ 2 \sin (\frac{s}{2}))$
131	127 130	eqtr2i	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) = {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ}$
132	131	oveq2i	$⊢ \frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = ℝ D ({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ})$
133		ioontr	$⊢ int (topGen (ran (.))) ((A, B)) = (A, B)$
134	132 133	reseq12i	$⊢ {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) ((A, B))} = {{({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ})}_{ℝ}^{'} ↾}_{(A, B)}$
135		eqid	$⊢ (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) = (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s)$
136		2cnd	$⊢ s \in ℂ \to 2 \in ℂ$
137	109	sincld	$⊢ s \in ℂ \to \sin (\frac{1}{2}) s \in ℂ$
138	136 137	mulcld	$⊢ s \in ℂ \to 2 \sin (\frac{1}{2}) s \in ℂ$
139	135 138	fmpti	$⊢ (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) : ℂ ⟶ ℂ$
140		ssid	$⊢ ℂ \subseteq ℂ$
141		dmmptg	$⊢ \forall s \in ℂ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s \in ℂ \to dom (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) = ℂ$
142		2cn	$⊢ 2 \in ℂ$
143	142 106	mulcli	$⊢ 2 (\frac{1}{2}) \in ℂ$
144	143	a1i	$⊢ s \in ℂ \to 2 (\frac{1}{2}) \in ℂ$
145	144 110	mulcld	$⊢ s \in ℂ \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) s \in ℂ$
146	141 145	mprg	$⊢ dom (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) = ℂ$
147	119 146	sseqtrri	$⊢ ℝ \subseteq dom (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
148		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)$
149	142 106 148	mp2an	$⊢ \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
150	149	dmeqi	$⊢ dom \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = dom (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
151	147 150	sseqtrri	$⊢ ℝ \subseteq dom \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s}$
152		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} ↾}_{ℝ}$
153	79 139 140 151 152	mp4an	$⊢ ℝ D ({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ}) = {\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ}$
154	153	reseq1i	$⊢ {{({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ})}_{ℝ}^{'} ↾}_{(A, B)} = {({\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ}) ↾}_{(A, B)}$
155	149	reseq1i	$⊢ {\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ} = {(s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) ↾}_{ℝ}$
156	155	reseq1i	$⊢ {({\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ}) ↾}_{(A, B)} = {({(s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) ↾}_{ℝ}) ↾}_{(A, B)}$
157		resabs1	$⊢ (A, B) \subseteq ℝ \to {({(s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) ↾}_{ℝ}) ↾}_{(A, B)} = {(s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) ↾}_{(A, B)}$
158	114 157	ax-mp	$⊢ {({(s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) ↾}_{ℝ}) ↾}_{(A, B)} = {(s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) ↾}_{(A, B)}$
159		ioosscn	$⊢ (A, B) \subseteq ℂ$
160		resmpt	$⊢ (A, B) \subseteq ℂ \to {(s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) ↾}_{(A, B)} = (s \in (A, B) ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
161	159 160	ax-mp	$⊢ {(s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) ↾}_{(A, B)} = (s \in (A, B) ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
162	156 158 161	3eqtri	$⊢ {({\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ}) ↾}_{(A, B)} = (s \in (A, B) ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
163	134 154 162	3eqtri	$⊢ {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) ((A, B))} = (s \in (A, B) ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
164	118 125 163	3eqtri	$⊢ \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
165		2thalfe1	$⊢ 2 (\frac{1}{2}) = 1$
166	165	oveq1i	$⊢ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s = 1 \cos (\frac{1}{2}) s$
167	166	a1i	$⊢ s \in (A, B) \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) s = 1 \cos (\frac{1}{2}) s$
168	111	mullidd	$⊢ s \in (A, B) \to 1 \cos (\frac{1}{2}) s = \cos (\frac{1}{2}) s$
169	167 168 105	3eqtrd	$⊢ s \in (A, B) \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) s = \cos (\frac{s}{2})$
170	169	mpteq2ia	$⊢ (s \in (A, B) ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) = (s \in (A, B) ⟼ \cos (\frac{s}{2}))$
171	164 170	eqtri	$⊢ \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ \cos (\frac{s}{2}))$
172	171	a1i	$⊢ φ \to \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ \cos (\frac{s}{2}))$
173	80 81 34 97 99 113 172	dvmptdiv	$⊢ φ \to \frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} = (s \in (A, B) ⟼ \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}})$
174	78 173	eqtrd	$⊢ φ \to ℝ D O = (s \in (A, B) ⟼ \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}})$
175	174	feq1d	$⊢ φ \to (O_{ℝ}^{'} : (A, B) ⟶ ℝ \leftrightarrow (s \in (A, B) ⟼ \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}}) : (A, B) ⟶ ℝ)$
176	76 175	mpbird	$⊢ φ \to O_{ℝ}^{'} : (A, B) ⟶ ℝ$
177	176 174	jca	$⊢ φ \to (O_{ℝ}^{'} : (A, B) ⟶ ℝ \land ℝ D O = (s \in (A, B) ⟼ \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}}))$
178	177 171	pm3.2i	$⊢ ((φ \to (O_{ℝ}^{'} : (A, B) ⟶ ℝ \land ℝ D O = (s \in (A, B) ⟼ \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}}))) \land \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ \cos (\frac{s}{2})))$

Metamath Proof Explorer

Theorem fourierdlem57

Proof