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	ffvelrnd	$⊢ (φ \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	ffvelrnd	$⊢ (φ \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	biimpi	$⊢ s = 0 \to 0 = s$
62	61	adantl	$⊢ (s \in (A, B) \land s = 0) \to 0 = s$
63		simpl	$⊢ (s \in (A, B) \land s = 0) \to s \in (A, B)$
64	62 63	eqeltrd	$⊢ (s \in (A, B) \land s = 0) \to 0 \in (A, B)$
65	64	adantll	$⊢ ((φ \land s \in (A, B)) \land s = 0) \to 0 \in (A, B)$
66	7	ad2antrr	$⊢ ((φ \land s \in (A, B)) \land s = 0) \to \neg 0 \in (A, B)$
67	65 66	pm2.65da	$⊢ (φ \land s \in (A, B)) \to \neg s = 0$
68	67	neqned	$⊢ (φ \land s \in (A, B)) \to s \neq 0$
69		fourierdlem44	$⊢ (s \in [- π, π] \land s \neq 0) \to \sin (\frac{s}{2}) \neq 0$
70	59 68 69	syl2anc	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \neq 0$
71	55 56 58 70	mulne0d	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \neq 0$
72		2z	$⊢ 2 \in ℤ$
73	72	a1i	$⊢ (φ \land s \in (A, B)) \to 2 \in ℤ$
74	54 71 73	expne0d	$⊢ (φ \land s \in (A, B)) \to {2 \sin (\frac{s}{2})}^{2} \neq 0$
75	48 49 74	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 ℝ$
76		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}})$
77	75 76	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) ⟶ ℝ$
78	9	a1i	$⊢ φ \to O = (s \in (A, B) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
79	78	oveq2d	$⊢ φ \to ℝ D O = \frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s}$
80		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
81	80	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
82	46	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) - C \in ℂ$
83	44	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℂ$
84		eqid	$⊢ ℝ D ({F ↾}_{(X + A, X + B)}) = ℝ D ({F ↾}_{(X + A, X + B)})$
85	1 2 3 4 84 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))$
86	45	recnd	$⊢ (φ \land s \in (A, B)) \to C \in ℂ$
87		0red	$⊢ (φ \land s \in (A, B)) \to 0 \in ℝ$
88		iooretop	$⊢ (A, B) \in topGen (ran (.))$
89		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
90	89	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
91	88 90	eleqtri	$⊢ (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
92	91	a1i	$⊢ φ \to (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
93	8	recnd	$⊢ φ \to C \in ℂ$
94	81 92 93	dvmptconst	$⊢ φ \to \frac{d (s \in (A, B)⟼ C)}{d_{ℝ} s} = (s \in (A, B) ⟼ 0)$
95	81 83 34 85 86 87 94	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)$
96	34	recnd	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) \in ℂ$
97	96	subid1d	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) - 0 = {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)$
98	97	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))$
99	95 98	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))$
100		eldifsn	$⊢ 2 \sin (\frac{s}{2}) \in (ℂ ∖ \{0\}) \leftrightarrow (2 \sin (\frac{s}{2}) \in ℂ \land 2 \sin (\frac{s}{2}) \neq 0)$
101	54 71 100	sylanbrc	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \in (ℂ ∖ \{0\})$
102		recn	$⊢ s \in ℝ \to s \in ℂ$
103	57	a1i	$⊢ s \in ℝ \to 2 \neq 0$
104	102 50 103	divrec2d	$⊢ s \in ℝ \to \frac{s}{2} = (\frac{1}{2}) s$
105	104	eqcomd	$⊢ s \in ℝ \to (\frac{1}{2}) s = \frac{s}{2}$
106	18 105	syl	$⊢ s \in (A, B) \to (\frac{1}{2}) s = \frac{s}{2}$
107	106	fveq2d	$⊢ s \in (A, B) \to \cos (\frac{1}{2}) s = \cos (\frac{s}{2})$
108		halfcn	$⊢ \frac{1}{2} \in ℂ$
109	108	a1i	$⊢ s \in ℂ \to \frac{1}{2} \in ℂ$
110		id	$⊢ s \in ℂ \to s \in ℂ$
111	109 110	mulcld	$⊢ s \in ℂ \to (\frac{1}{2}) s \in ℂ$
112	111	coscld	$⊢ s \in ℂ \to \cos (\frac{1}{2}) s \in ℂ$
113	18 102 112	3syl	$⊢ s \in (A, B) \to \cos (\frac{1}{2}) s \in ℂ$
114	107 113	eqeltrrd	$⊢ s \in (A, B) \to \cos (\frac{s}{2}) \in ℂ$
115	114	adantl	$⊢ (φ \land s \in (A, B)) \to \cos (\frac{s}{2}) \in ℂ$
116		ioossre	$⊢ (A, B) \subseteq ℝ$
117		resmpt	$⊢ (A, B) \subseteq ℝ \to {(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{(A, B)} = (s \in (A, B) ⟼ 2 \sin (\frac{s}{2}))$
118	116 117	ax-mp	$⊢ {(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{(A, B)} = (s \in (A, B) ⟼ 2 \sin (\frac{s}{2}))$
119	118	eqcomi	$⊢ (s \in (A, B) ⟼ 2 \sin (\frac{s}{2})) = {(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{(A, B)}$
120	119	oveq2i	$⊢ \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = ℝ D ({(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{(A, B)})$
121		ax-resscn	$⊢ ℝ \subseteq ℂ$
122		eqid	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) = (s \in ℝ ⟼ 2 \sin (\frac{s}{2}))$
123	122 53	fmpti	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) : ℝ ⟶ ℂ$
124		ssid	$⊢ ℝ \subseteq ℝ$
125	89 90	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))}$
126	121 123 124 116 125	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))}$
127		resmpt	$⊢ ℝ \subseteq ℂ \to {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ} = (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s)$
128	121 127	ax-mp	$⊢ {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ} = (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s)$
129	105	fveq2d	$⊢ s \in ℝ \to \sin (\frac{1}{2}) s = \sin (\frac{s}{2})$
130	129	oveq2d	$⊢ s \in ℝ \to 2 \sin (\frac{1}{2}) s = 2 \sin (\frac{s}{2})$
131	130	mpteq2ia	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s) = (s \in ℝ ⟼ 2 \sin (\frac{s}{2}))$
132	128 131	eqtr2i	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) = {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ}$
133	132	oveq2i	$⊢ \frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = ℝ D ({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ})$
134		ioontr	$⊢ int (topGen (ran (.))) ((A, B)) = (A, B)$
135	133 134	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)}$
136		eqid	$⊢ (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) = (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s)$
137		2cnd	$⊢ s \in ℂ \to 2 \in ℂ$
138	111	sincld	$⊢ s \in ℂ \to \sin (\frac{1}{2}) s \in ℂ$
139	137 138	mulcld	$⊢ s \in ℂ \to 2 \sin (\frac{1}{2}) s \in ℂ$
140	136 139	fmpti	$⊢ (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) : ℂ ⟶ ℂ$
141		ssid	$⊢ ℂ \subseteq ℂ$
142		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) = ℂ$
143		2cn	$⊢ 2 \in ℂ$
144	143 108	mulcli	$⊢ 2 (\frac{1}{2}) \in ℂ$
145	144	a1i	$⊢ s \in ℂ \to 2 (\frac{1}{2}) \in ℂ$
146	145 112	mulcld	$⊢ s \in ℂ \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) s \in ℂ$
147	142 146	mprg	$⊢ dom (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) = ℂ$
148	121 147	sseqtrri	$⊢ ℝ \subseteq dom (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
149		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)$
150	143 108 149	mp2an	$⊢ \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
151	150	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)$
152	148 151	sseqtrri	$⊢ ℝ \subseteq dom \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s}$
153		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} ↾}_{ℝ}$
154	80 140 141 152 153	mp4an	$⊢ ℝ D ({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ}) = {\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ}$
155	154	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)}$
156	150	reseq1i	$⊢ {\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ} = {(s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) ↾}_{ℝ}$
157	156	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)}$
158		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)}$
159	116 158	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)}$
160		ioosscn	$⊢ (A, B) \subseteq ℂ$
161		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)$
162	160 161	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)$
163	157 159 162	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)$
164	135 155 163	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)$
165	120 126 164	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)$
166	143 57	recidi	$⊢ 2 (\frac{1}{2}) = 1$
167	166	oveq1i	$⊢ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s = 1 \cos (\frac{1}{2}) s$
168	167	a1i	$⊢ s \in (A, B) \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) s = 1 \cos (\frac{1}{2}) s$
169	113	mulid2d	$⊢ s \in (A, B) \to 1 \cos (\frac{1}{2}) s = \cos (\frac{1}{2}) s$
170	168 169 107	3eqtrd	$⊢ s \in (A, B) \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) s = \cos (\frac{s}{2})$
171	170	mpteq2ia	$⊢ (s \in (A, B) ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) = (s \in (A, B) ⟼ \cos (\frac{s}{2}))$
172	165 171	eqtri	$⊢ \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ \cos (\frac{s}{2}))$
173	172	a1i	$⊢ φ \to \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ \cos (\frac{s}{2}))$
174	81 82 34 99 101 115 173	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}})$
175	79 174	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}})$
176	175	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) ⟶ ℝ)$
177	77 176	mpbird	$⊢ φ \to O_{ℝ}^{'} : (A, B) ⟶ ℝ$
178	177 175	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}}))$
179	178 172	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