fourierdlem78

Description: G is continuous when restricted on an interval not containing 0 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem78.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem78.a	$⊢ φ \to A \in [- π, π]$
	fourierdlem78.b	$⊢ φ \to B \in [- π, π]$
	fourierdlem78.x	$⊢ φ \to X \in ℝ$
	fourierdlem78.nxelab	$⊢ φ \to \neg 0 \in (A, B)$
	fourierdlem78.fcn	$⊢ φ \to ({F ↾}_{(A + X, B + X)}) : (A + X, B + X) \underset{cn}{⟶} ℂ$
	fourierdlem78.y	$⊢ φ \to Y \in ℝ$
	fourierdlem78.w	$⊢ φ \to W \in ℝ$
	fourierdlem78.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
	fourierdlem78.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
	fourierdlem78.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
	fourierdlem78.n	$⊢ φ \to N \in ℝ$
	fourierdlem78.s	$⊢ S = (s \in [- π, π] ⟼ \sin (N + (\frac{1}{2})) s)$
	fourierdlem78.g	$⊢ G = (s \in [- π, π] ⟼ U (s) S (s))$
Assertion	fourierdlem78	$⊢ φ \to ({G ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℝ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem78.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem78.a	$⊢ φ \to A \in [- π, π]$
3		fourierdlem78.b	$⊢ φ \to B \in [- π, π]$
4		fourierdlem78.x	$⊢ φ \to X \in ℝ$
5		fourierdlem78.nxelab	$⊢ φ \to \neg 0 \in (A, B)$
6		fourierdlem78.fcn	$⊢ φ \to ({F ↾}_{(A + X, B + X)}) : (A + X, B + X) \underset{cn}{⟶} ℂ$
7		fourierdlem78.y	$⊢ φ \to Y \in ℝ$
8		fourierdlem78.w	$⊢ φ \to W \in ℝ$
9		fourierdlem78.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
10		fourierdlem78.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
11		fourierdlem78.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
12		fourierdlem78.n	$⊢ φ \to N \in ℝ$
13		fourierdlem78.s	$⊢ S = (s \in [- π, π] ⟼ \sin (N + (\frac{1}{2})) s)$
14		fourierdlem78.g	$⊢ G = (s \in [- π, π] ⟼ U (s) S (s))$
15	14	a1i	$⊢ φ \to G = (s \in [- π, π] ⟼ U (s) S (s))$
16	15	reseq1d	$⊢ φ \to {G ↾}_{(A, B)} = {(s \in [- π, π] ⟼ U (s) S (s)) ↾}_{(A, B)}$
17		pire	$⊢ π \in ℝ$
18	17	renegcli	$⊢ - π \in ℝ$
19	18	a1i	$⊢ (φ \land s \in (A, B)) \to - π \in ℝ$
20	17	a1i	$⊢ (φ \land s \in (A, B)) \to π \in ℝ$
21		elioore	$⊢ s \in (A, B) \to s \in ℝ$
22	21	adantl	$⊢ (φ \land s \in (A, B)) \to s \in ℝ$
23	18	a1i	$⊢ φ \to - π \in ℝ$
24	17	a1i	$⊢ φ \to π \in ℝ$
25	23 24	iccssred	$⊢ φ \to [- π, π] \subseteq ℝ$
26	25 2	sseldd	$⊢ φ \to A \in ℝ$
27	26	adantr	$⊢ (φ \land s \in (A, B)) \to A \in ℝ$
28	18 17	elicc2i	$⊢ A \in [- π, π] \leftrightarrow (A \in ℝ \land - π \leq A \land A \leq π)$
29	28	simp2bi	$⊢ A \in [- π, π] \to - π \leq A$
30	2 29	syl	$⊢ φ \to - π \leq A$
31	30	adantr	$⊢ (φ \land s \in (A, B)) \to - π \leq A$
32	27	rexrd	$⊢ (φ \land s \in (A, B)) \to A \in ℝ^{*}$
33	25 3	sseldd	$⊢ φ \to B \in ℝ$
34	33	rexrd	$⊢ φ \to B \in ℝ^{*}$
35	34	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ^{*}$
36		simpr	$⊢ (φ \land s \in (A, B)) \to s \in (A, B)$
37		ioogtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to A < s$
38	32 35 36 37	syl3anc	$⊢ (φ \land s \in (A, B)) \to A < s$
39	19 27 22 31 38	lelttrd	$⊢ (φ \land s \in (A, B)) \to - π < s$
40	19 22 39	ltled	$⊢ (φ \land s \in (A, B)) \to - π \leq s$
41	33	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ$
42		iooltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to s < B$
43	32 35 36 42	syl3anc	$⊢ (φ \land s \in (A, B)) \to s < B$
44	18 17	elicc2i	$⊢ B \in [- π, π] \leftrightarrow (B \in ℝ \land - π \leq B \land B \leq π)$
45	44	simp3bi	$⊢ B \in [- π, π] \to B \leq π$
46	3 45	syl	$⊢ φ \to B \leq π$
47	46	adantr	$⊢ (φ \land s \in (A, B)) \to B \leq π$
48	22 41 20 43 47	ltletrd	$⊢ (φ \land s \in (A, B)) \to s < π$
49	22 20 48	ltled	$⊢ (φ \land s \in (A, B)) \to s \leq π$
50	19 20 22 40 49	eliccd	$⊢ (φ \land s \in (A, B)) \to s \in [- π, π]$
51	50	ex	$⊢ φ \to (s \in (A, B) \to s \in [- π, π])$
52	51	ssrdv	$⊢ φ \to (A, B) \subseteq [- π, π]$
53	52	resmptd	$⊢ φ \to {(s \in [- π, π] ⟼ U (s) S (s)) ↾}_{(A, B)} = (s \in (A, B) ⟼ U (s) S (s))$
54	16 53	eqtrd	$⊢ φ \to {G ↾}_{(A, B)} = (s \in (A, B) ⟼ U (s) S (s))$
55		0red	$⊢ (φ \land s \in (A, B)) \to 0 \in ℝ$
56	1	adantr	$⊢ (φ \land s \in (A, B)) \to F : ℝ ⟶ ℝ$
57	4	adantr	$⊢ (φ \land s \in (A, B)) \to X \in ℝ$
58	57 22	readdcld	$⊢ (φ \land s \in (A, B)) \to X + s \in ℝ$
59	56 58	ffvelcdmd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℝ$
60	7 8	ifcld	$⊢ φ \to if (0 < s, Y, W) \in ℝ$
61	60	adantr	$⊢ (φ \land s \in (A, B)) \to if (0 < s, Y, W) \in ℝ$
62	59 61	resubcld	$⊢ (φ \land s \in (A, B)) \to F (X + s) - if (0 < s, Y, W) \in ℝ$
63		eleq1	$⊢ s = 0 \to (s \in (A, B) \leftrightarrow 0 \in (A, B))$
64	63	biimpac	$⊢ (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	5	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	62 22 68	redivcld	$⊢ (φ \land s \in (A, B)) \to \frac{F (X + s) - if (0 < s, Y, W)}{s} \in ℝ$
70	55 69	ifcld	$⊢ (φ \land s \in (A, B)) \to if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}) \in ℝ$
71	9	fvmpt2	$⊢ (s \in [- π, π] \land if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}) \in ℝ) \to H (s) = if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})$
72	50 70 71	syl2anc	$⊢ (φ \land s \in (A, B)) \to H (s) = if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})$
73	72 70	eqeltrd	$⊢ (φ \land s \in (A, B)) \to H (s) \in ℝ$
74		1red	$⊢ (φ \land s \in (A, B)) \to 1 \in ℝ$
75		2re	$⊢ 2 \in ℝ$
76	75	a1i	$⊢ (φ \land s \in (A, B)) \to 2 \in ℝ$
77	22	rehalfcld	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2} \in ℝ$
78	77	resincld	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \in ℝ$
79	76 78	remulcld	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \in ℝ$
80	76	recnd	$⊢ (φ \land s \in (A, B)) \to 2 \in ℂ$
81	78	recnd	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \in ℂ$
82		2ne0	$⊢ 2 \neq 0$
83	82	a1i	$⊢ (φ \land s \in (A, B)) \to 2 \neq 0$
84		fourierdlem44	$⊢ (s \in [- π, π] \land s \neq 0) \to \sin (\frac{s}{2}) \neq 0$
85	50 68 84	syl2anc	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \neq 0$
86	80 81 83 85	mulne0d	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \neq 0$
87	22 79 86	redivcld	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2 \sin (\frac{s}{2})} \in ℝ$
88	74 87	ifcld	$⊢ (φ \land s \in (A, B)) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) \in ℝ$
89	10	fvmpt2	$⊢ (s \in [- π, π] \land if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) \in ℝ) \to K (s) = if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})$
90	50 88 89	syl2anc	$⊢ (φ \land s \in (A, B)) \to K (s) = if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})$
91	90 88	eqeltrd	$⊢ (φ \land s \in (A, B)) \to K (s) \in ℝ$
92	73 91	remulcld	$⊢ (φ \land s \in (A, B)) \to H (s) K (s) \in ℝ$
93	11	fvmpt2	$⊢ (s \in [- π, π] \land H (s) K (s) \in ℝ) \to U (s) = H (s) K (s)$
94	50 92 93	syl2anc	$⊢ (φ \land s \in (A, B)) \to U (s) = H (s) K (s)$
95	94 92	eqeltrd	$⊢ (φ \land s \in (A, B)) \to U (s) \in ℝ$
96	12	adantr	$⊢ (φ \land s \in (A, B)) \to N \in ℝ$
97	76 83	rereccld	$⊢ (φ \land s \in (A, B)) \to \frac{1}{2} \in ℝ$
98	96 97	readdcld	$⊢ (φ \land s \in (A, B)) \to N + (\frac{1}{2}) \in ℝ$
99	98 22	remulcld	$⊢ (φ \land s \in (A, B)) \to (N + (\frac{1}{2})) s \in ℝ$
100	99	resincld	$⊢ (φ \land s \in (A, B)) \to \sin (N + (\frac{1}{2})) s \in ℝ$
101	13	fvmpt2	$⊢ (s \in [- π, π] \land \sin (N + (\frac{1}{2})) s \in ℝ) \to S (s) = \sin (N + (\frac{1}{2})) s$
102	50 100 101	syl2anc	$⊢ (φ \land s \in (A, B)) \to S (s) = \sin (N + (\frac{1}{2})) s$
103	102 100	eqeltrd	$⊢ (φ \land s \in (A, B)) \to S (s) \in ℝ$
104	95 103	remulcld	$⊢ (φ \land s \in (A, B)) \to U (s) S (s) \in ℝ$
105		eqid	$⊢ (s \in (A, B) ⟼ U (s) S (s)) = (s \in (A, B) ⟼ U (s) S (s))$
106	104 105	fmptd	$⊢ φ \to (s \in (A, B) ⟼ U (s) S (s)) : (A, B) ⟶ ℝ$
107		ax-resscn	$⊢ ℝ \subseteq ℂ$
108	107	a1i	$⊢ φ \to ℝ \subseteq ℂ$
109	94	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ U (s)) = (s \in (A, B) ⟼ H (s) K (s))$
110	67	iffalsed	$⊢ (φ \land s \in (A, B)) \to if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}) = \frac{F (X + s) - if (0 < s, Y, W)}{s}$
111	62	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) - if (0 < s, Y, W) \in ℂ$
112	22	recnd	$⊢ (φ \land s \in (A, B)) \to s \in ℂ$
113	111 112 68	divrecd	$⊢ (φ \land s \in (A, B)) \to \frac{F (X + s) - if (0 < s, Y, W)}{s} = (F (X + s) - if (0 < s, Y, W)) (\frac{1}{s})$
114	72 110 113	3eqtrd	$⊢ (φ \land s \in (A, B)) \to H (s) = (F (X + s) - if (0 < s, Y, W)) (\frac{1}{s})$
115	114	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ H (s)) = (s \in (A, B) ⟼ (F (X + s) - if (0 < s, Y, W)) (\frac{1}{s}))$
116	59	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℂ$
117	61	recnd	$⊢ (φ \land s \in (A, B)) \to if (0 < s, Y, W) \in ℂ$
118	116 117	negsubd	$⊢ (φ \land s \in (A, B)) \to F (X + s) + (- if (0 < s, Y, W)) = F (X + s) - if (0 < s, Y, W)$
119	118	eqcomd	$⊢ (φ \land s \in (A, B)) \to F (X + s) - if (0 < s, Y, W) = F (X + s) + (- if (0 < s, Y, W))$
120	119	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ F (X + s) - if (0 < s, Y, W)) = (s \in (A, B) ⟼ F (X + s) + (- if (0 < s, Y, W)))$
121	26 4	readdcld	$⊢ φ \to A + X \in ℝ$
122	121	rexrd	$⊢ φ \to A + X \in ℝ^{*}$
123	122	adantr	$⊢ (φ \land s \in (A, B)) \to A + X \in ℝ^{*}$
124	33 4	readdcld	$⊢ φ \to B + X \in ℝ$
125	124	rexrd	$⊢ φ \to B + X \in ℝ^{*}$
126	125	adantr	$⊢ (φ \land s \in (A, B)) \to B + X \in ℝ^{*}$
127	26	recnd	$⊢ φ \to A \in ℂ$
128	4	recnd	$⊢ φ \to X \in ℂ$
129	127 128	addcomd	$⊢ φ \to A + X = X + A$
130	129	adantr	$⊢ (φ \land s \in (A, B)) \to A + X = X + A$
131	27 22 57 38	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + A < X + s$
132	130 131	eqbrtrd	$⊢ (φ \land s \in (A, B)) \to A + X < X + s$
133	22 41 57 43	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + s < X + B$
134	33	recnd	$⊢ φ \to B \in ℂ$
135	128 134	addcomd	$⊢ φ \to X + B = B + X$
136	135	adantr	$⊢ (φ \land s \in (A, B)) \to X + B = B + X$
137	133 136	breqtrd	$⊢ (φ \land s \in (A, B)) \to X + s < B + X$
138	123 126 58 132 137	eliood	$⊢ (φ \land s \in (A, B)) \to X + s \in (A + X, B + X)$
139		fvres	$⊢ X + s \in (A + X, B + X) \to ({F ↾}_{(A + X, B + X)}) (X + s) = F (X + s)$
140	138 139	syl	$⊢ (φ \land s \in (A, B)) \to ({F ↾}_{(A + X, B + X)}) (X + s) = F (X + s)$
141	140	eqcomd	$⊢ (φ \land s \in (A, B)) \to F (X + s) = ({F ↾}_{(A + X, B + X)}) (X + s)$
142	141	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ F (X + s)) = (s \in (A, B) ⟼ ({F ↾}_{(A + X, B + X)}) (X + s))$
143		ioosscn	$⊢ (A + X, B + X) \subseteq ℂ$
144	143	a1i	$⊢ φ \to (A + X, B + X) \subseteq ℂ$
145		ioosscn	$⊢ (A, B) \subseteq ℂ$
146	145	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
147	144 6 146 128 138	fourierdlem23	$⊢ φ \to (s \in (A, B) ⟼ ({F ↾}_{(A + X, B + X)}) (X + s)) : (A, B) \underset{cn}{⟶} ℂ$
148	142 147	eqeltrd	$⊢ φ \to (s \in (A, B) ⟼ F (X + s)) : (A, B) \underset{cn}{⟶} ℂ$
149		0red	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to 0 \in ℝ$
150	26	ad2antrr	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to A \in ℝ$
151	21	adantl	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to s \in ℝ$
152		simplr	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to 0 \leq A$
153	38	adantlr	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to A < s$
154	149 150 151 152 153	lelttrd	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to 0 < s$
155	154	iftrued	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to if (0 < s, Y, W) = Y$
156	155	negeqd	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to - if (0 < s, Y, W) = - Y$
157	156	mpteq2dva	$⊢ (φ \land 0 \leq A) \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) = (s \in (A, B) ⟼ - Y)$
158	7	renegcld	$⊢ φ \to - Y \in ℝ$
159	158	recnd	$⊢ φ \to - Y \in ℂ$
160		ssid	$⊢ ℂ \subseteq ℂ$
161	160	a1i	$⊢ φ \to ℂ \subseteq ℂ$
162	146 159 161	constcncfg	$⊢ φ \to (s \in (A, B) ⟼ - Y) : (A, B) \underset{cn}{⟶} ℂ$
163	162	adantr	$⊢ (φ \land 0 \leq A) \to (s \in (A, B) ⟼ - Y) : (A, B) \underset{cn}{⟶} ℂ$
164	157 163	eqeltrd	$⊢ (φ \land 0 \leq A) \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) : (A, B) \underset{cn}{⟶} ℂ$
165		simpl	$⊢ (φ \land \neg 0 \leq A) \to φ$
166	26	rexrd	$⊢ φ \to A \in ℝ^{*}$
167	166	ad2antrr	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to A \in ℝ^{*}$
168	34	ad2antrr	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to B \in ℝ^{*}$
169		0red	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to 0 \in ℝ$
170		simpr	$⊢ (φ \land \neg 0 \leq A) \to \neg 0 \leq A$
171	26	adantr	$⊢ (φ \land \neg 0 \leq A) \to A \in ℝ$
172		0red	$⊢ (φ \land \neg 0 \leq A) \to 0 \in ℝ$
173	171 172	ltnled	$⊢ (φ \land \neg 0 \leq A) \to (A < 0 \leftrightarrow \neg 0 \leq A)$
174	170 173	mpbird	$⊢ (φ \land \neg 0 \leq A) \to A < 0$
175	174	adantr	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to A < 0$
176		simpr	$⊢ (φ \land \neg B \leq 0) \to \neg B \leq 0$
177		0red	$⊢ (φ \land \neg B \leq 0) \to 0 \in ℝ$
178	33	adantr	$⊢ (φ \land \neg B \leq 0) \to B \in ℝ$
179	177 178	ltnled	$⊢ (φ \land \neg B \leq 0) \to (0 < B \leftrightarrow \neg B \leq 0)$
180	176 179	mpbird	$⊢ (φ \land \neg B \leq 0) \to 0 < B$
181	180	adantlr	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to 0 < B$
182	167 168 169 175 181	eliood	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to 0 \in (A, B)$
183	5	ad2antrr	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to \neg 0 \in (A, B)$
184	182 183	condan	$⊢ (φ \land \neg 0 \leq A) \to B \leq 0$
185	21	adantl	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to s \in ℝ$
186		0red	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to 0 \in ℝ$
187	33	ad2antrr	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to B \in ℝ$
188	43	adantlr	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to s < B$
189		simplr	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to B \leq 0$
190	185 187 186 188 189	ltletrd	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to s < 0$
191	185 186 190	ltnsymd	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to \neg 0 < s$
192	191	iffalsed	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to if (0 < s, Y, W) = W$
193	192	negeqd	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to - if (0 < s, Y, W) = - W$
194	193	mpteq2dva	$⊢ (φ \land B \leq 0) \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) = (s \in (A, B) ⟼ - W)$
195	8	recnd	$⊢ φ \to W \in ℂ$
196	195	negcld	$⊢ φ \to - W \in ℂ$
197	146 196 161	constcncfg	$⊢ φ \to (s \in (A, B) ⟼ - W) : (A, B) \underset{cn}{⟶} ℂ$
198	197	adantr	$⊢ (φ \land B \leq 0) \to (s \in (A, B) ⟼ - W) : (A, B) \underset{cn}{⟶} ℂ$
199	194 198	eqeltrd	$⊢ (φ \land B \leq 0) \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) : (A, B) \underset{cn}{⟶} ℂ$
200	165 184 199	syl2anc	$⊢ (φ \land \neg 0 \leq A) \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) : (A, B) \underset{cn}{⟶} ℂ$
201	164 200	pm2.61dan	$⊢ φ \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) : (A, B) \underset{cn}{⟶} ℂ$
202	148 201	addcncf	$⊢ φ \to (s \in (A, B) ⟼ F (X + s) + (- if (0 < s, Y, W))) : (A, B) \underset{cn}{⟶} ℂ$
203	120 202	eqeltrd	$⊢ φ \to (s \in (A, B) ⟼ F (X + s) - if (0 < s, Y, W)) : (A, B) \underset{cn}{⟶} ℂ$
204		eqid	$⊢ (s \in (ℂ ∖ \{0\}) ⟼ \frac{1}{s}) = (s \in (ℂ ∖ \{0\}) ⟼ \frac{1}{s})$
205		1cnd	$⊢ φ \to 1 \in ℂ$
206	204	cdivcncf	$⊢ 1 \in ℂ \to (s \in (ℂ ∖ \{0\}) ⟼ \frac{1}{s}) : (ℂ ∖ \{0\}) \underset{cn}{⟶} ℂ$
207	205 206	syl	$⊢ φ \to (s \in (ℂ ∖ \{0\}) ⟼ \frac{1}{s}) : (ℂ ∖ \{0\}) \underset{cn}{⟶} ℂ$
208		velsn	$⊢ s \in \{0\} \leftrightarrow s = 0$
209	67 208	sylnibr	$⊢ (φ \land s \in (A, B)) \to \neg s \in \{0\}$
210	112 209	eldifd	$⊢ (φ \land s \in (A, B)) \to s \in (ℂ ∖ \{0\})$
211	210	ralrimiva	$⊢ φ \to \forall s \in (A, B) s \in (ℂ ∖ \{0\})$
212		dfss3	$⊢ (A, B) \subseteq ℂ ∖ \{0\} \leftrightarrow \forall s \in (A, B) s \in (ℂ ∖ \{0\})$
213	211 212	sylibr	$⊢ φ \to (A, B) \subseteq ℂ ∖ \{0\}$
214	22 68	rereccld	$⊢ (φ \land s \in (A, B)) \to \frac{1}{s} \in ℝ$
215	214	recnd	$⊢ (φ \land s \in (A, B)) \to \frac{1}{s} \in ℂ$
216	204 207 213 161 215	cncfmptssg	$⊢ φ \to (s \in (A, B) ⟼ \frac{1}{s}) : (A, B) \underset{cn}{⟶} ℂ$
217	203 216	mulcncf	$⊢ φ \to (s \in (A, B) ⟼ (F (X + s) - if (0 < s, Y, W)) (\frac{1}{s})) : (A, B) \underset{cn}{⟶} ℂ$
218	115 217	eqeltrd	$⊢ φ \to (s \in (A, B) ⟼ H (s)) : (A, B) \underset{cn}{⟶} ℂ$
219	67	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})}$
220	79	recnd	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \in ℂ$
221	112 220 86	divrecd	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2 \sin (\frac{s}{2})} = s (\frac{1}{2 \sin (\frac{s}{2})})$
222	90 219 221	3eqtrd	$⊢ (φ \land s \in (A, B)) \to K (s) = s (\frac{1}{2 \sin (\frac{s}{2})})$
223	222	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ K (s)) = (s \in (A, B) ⟼ s (\frac{1}{2 \sin (\frac{s}{2})}))$
224	219 221	eqtr2d	$⊢ (φ \land s \in (A, B)) \to s (\frac{1}{2 \sin (\frac{s}{2})}) = if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})$
225	224	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ s (\frac{1}{2 \sin (\frac{s}{2})})) = (s \in (A, B) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
226		eqid	$⊢ (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
227		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to [- π, π] \underset{cn}{⟶} ℝ \subseteq [- π, π] \underset{cn}{⟶} ℂ$
228	107 160 227	mp2an	$⊢ [- π, π] \underset{cn}{⟶} ℝ \subseteq [- π, π] \underset{cn}{⟶} ℂ$
229	226	fourierdlem62	$⊢ (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) : [- π, π] \underset{cn}{⟶} ℝ$
230	229	a1i	$⊢ φ \to (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) : [- π, π] \underset{cn}{⟶} ℝ$
231	228 230	sselid	$⊢ φ \to (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) : [- π, π] \underset{cn}{⟶} ℂ$
232	88	recnd	$⊢ (φ \land s \in (A, B)) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) \in ℂ$
233	226 231 52 161 232	cncfmptssg	$⊢ φ \to (s \in (A, B) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) : (A, B) \underset{cn}{⟶} ℂ$
234	225 233	eqeltrd	$⊢ φ \to (s \in (A, B) ⟼ s (\frac{1}{2 \sin (\frac{s}{2})})) : (A, B) \underset{cn}{⟶} ℂ$
235	223 234	eqeltrd	$⊢ φ \to (s \in (A, B) ⟼ K (s)) : (A, B) \underset{cn}{⟶} ℂ$
236	218 235	mulcncf	$⊢ φ \to (s \in (A, B) ⟼ H (s) K (s)) : (A, B) \underset{cn}{⟶} ℂ$
237	109 236	eqeltrd	$⊢ φ \to (s \in (A, B) ⟼ U (s)) : (A, B) \underset{cn}{⟶} ℂ$
238	102	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ S (s)) = (s \in (A, B) ⟼ \sin (N + (\frac{1}{2})) s)$
239		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
240	239	a1i	$⊢ φ \to \sin : ℂ \underset{cn}{⟶} ℂ$
241		halfre	$⊢ \frac{1}{2} \in ℝ$
242	241	a1i	$⊢ φ \to \frac{1}{2} \in ℝ$
243	12 242	readdcld	$⊢ φ \to N + (\frac{1}{2}) \in ℝ$
244	243	recnd	$⊢ φ \to N + (\frac{1}{2}) \in ℂ$
245	146 244 161	constcncfg	$⊢ φ \to (s \in (A, B) ⟼ N + (\frac{1}{2})) : (A, B) \underset{cn}{⟶} ℂ$
246	146 161	idcncfg	$⊢ φ \to (s \in (A, B) ⟼ s) : (A, B) \underset{cn}{⟶} ℂ$
247	245 246	mulcncf	$⊢ φ \to (s \in (A, B) ⟼ (N + (\frac{1}{2})) s) : (A, B) \underset{cn}{⟶} ℂ$
248	240 247	cncfmpt1f	$⊢ φ \to (s \in (A, B) ⟼ \sin (N + (\frac{1}{2})) s) : (A, B) \underset{cn}{⟶} ℂ$
249	238 248	eqeltrd	$⊢ φ \to (s \in (A, B) ⟼ S (s)) : (A, B) \underset{cn}{⟶} ℂ$
250	237 249	mulcncf	$⊢ φ \to (s \in (A, B) ⟼ U (s) S (s)) : (A, B) \underset{cn}{⟶} ℂ$
251		cncfcdm	$⊢ (ℝ \subseteq ℂ \land (s \in (A, B) ⟼ U (s) S (s)) : (A, B) \underset{cn}{⟶} ℂ) \to ((s \in (A, B) ⟼ U (s) S (s)) : (A, B) \underset{cn}{⟶} ℝ \leftrightarrow (s \in (A, B) ⟼ U (s) S (s)) : (A, B) ⟶ ℝ)$
252	108 250 251	syl2anc	$⊢ φ \to ((s \in (A, B) ⟼ U (s) S (s)) : (A, B) \underset{cn}{⟶} ℝ \leftrightarrow (s \in (A, B) ⟼ U (s) S (s)) : (A, B) ⟶ ℝ)$
253	106 252	mpbird	$⊢ φ \to (s \in (A, B) ⟼ U (s) S (s)) : (A, B) \underset{cn}{⟶} ℝ$
254	54 253	eqeltrd	$⊢ φ \to ({G ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℝ$

Metamath Proof Explorer

Theorem fourierdlem78

Proof