fourierdlem66

Description: Value of the G function when the argument is not zero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem66.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem66.x	$⊢ φ \to X \in ℝ$
	fourierdlem66.y	$⊢ φ \to Y \in ℝ$
	fourierdlem66.w	$⊢ φ \to W \in ℝ$
	fourierdlem66.d	$⊢ D = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
	fourierdlem66.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
	fourierdlem66.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
	fourierdlem66.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
	fourierdlem66.s	$⊢ S = (s \in [- π, π] ⟼ \sin (n + (\frac{1}{2})) s)$
	fourierdlem66.g	$⊢ G = (s \in [- π, π] ⟼ U (s) S (s))$
	fourierdlem66.a	$⊢ A = [- π, π] ∖ \{0\}$
Assertion	fourierdlem66	$⊢ ((φ \land n \in ℕ) \land s \in A) \to G (s) = π (F (X + s) - if (0 < s, Y, W)) D (n) (s)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem66.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem66.x	$⊢ φ \to X \in ℝ$
3		fourierdlem66.y	$⊢ φ \to Y \in ℝ$
4		fourierdlem66.w	$⊢ φ \to W \in ℝ$
5		fourierdlem66.d	$⊢ D = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
6		fourierdlem66.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
7		fourierdlem66.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
8		fourierdlem66.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
9		fourierdlem66.s	$⊢ S = (s \in [- π, π] ⟼ \sin (n + (\frac{1}{2})) s)$
10		fourierdlem66.g	$⊢ G = (s \in [- π, π] ⟼ U (s) S (s))$
11		fourierdlem66.a	$⊢ A = [- π, π] ∖ \{0\}$
12	11	eqimssi	$⊢ A \subseteq [- π, π] ∖ \{0\}$
13		difss	$⊢ [- π, π] ∖ \{0\} \subseteq [- π, π]$
14	12 13	sstri	$⊢ A \subseteq [- π, π]$
15	14	a1i	$⊢ φ \to A \subseteq [- π, π]$
16	15	sselda	$⊢ (φ \land s \in A) \to s \in [- π, π]$
17	16	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to s \in [- π, π]$
18	1	adantr	$⊢ (φ \land n \in ℕ) \to F : ℝ ⟶ ℝ$
19	2	adantr	$⊢ (φ \land n \in ℕ) \to X \in ℝ$
20	3	adantr	$⊢ (φ \land n \in ℕ) \to Y \in ℝ$
21	4	adantr	$⊢ (φ \land n \in ℕ) \to W \in ℝ$
22	18 19 20 21 6 7 8	fourierdlem55	$⊢ (φ \land n \in ℕ) \to U : [- π, π] ⟶ ℝ$
23	22	adantr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to U : [- π, π] ⟶ ℝ$
24	23 17	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to U (s) \in ℝ$
25		nnre	$⊢ n \in ℕ \to n \in ℝ$
26	9	fourierdlem5	$⊢ n \in ℝ \to S : [- π, π] ⟶ ℝ$
27	25 26	syl	$⊢ n \in ℕ \to S : [- π, π] ⟶ ℝ$
28	27	ad2antlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to S : [- π, π] ⟶ ℝ$
29	28 17	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to S (s) \in ℝ$
30	24 29	remulcld	$⊢ ((φ \land n \in ℕ) \land s \in A) \to U (s) S (s) \in ℝ$
31	10	fvmpt2	$⊢ (s \in [- π, π] \land U (s) S (s) \in ℝ) \to G (s) = U (s) S (s)$
32	17 30 31	syl2anc	$⊢ ((φ \land n \in ℕ) \land s \in A) \to G (s) = U (s) S (s)$
33	1 2 3 4 6	fourierdlem9	$⊢ φ \to H : [- π, π] ⟶ ℝ$
34	33	adantr	$⊢ (φ \land s \in A) \to H : [- π, π] ⟶ ℝ$
35	34 16	ffvelrnd	$⊢ (φ \land s \in A) \to H (s) \in ℝ$
36	7	fourierdlem43	$⊢ K : [- π, π] ⟶ ℝ$
37	36	a1i	$⊢ (φ \land s \in A) \to K : [- π, π] ⟶ ℝ$
38	37 16	ffvelrnd	$⊢ (φ \land s \in A) \to K (s) \in ℝ$
39	35 38	remulcld	$⊢ (φ \land s \in A) \to H (s) K (s) \in ℝ$
40	8	fvmpt2	$⊢ (s \in [- π, π] \land H (s) K (s) \in ℝ) \to U (s) = H (s) K (s)$
41	16 39 40	syl2anc	$⊢ (φ \land s \in A) \to U (s) = H (s) K (s)$
42		0red	$⊢ (φ \land s \in A) \to 0 \in ℝ$
43	1	adantr	$⊢ (φ \land s \in A) \to F : ℝ ⟶ ℝ$
44	2	adantr	$⊢ (φ \land s \in A) \to X \in ℝ$
45		pire	$⊢ π \in ℝ$
46	45	renegcli	$⊢ - π \in ℝ$
47		iccssre	$⊢ (- π \in ℝ \land π \in ℝ) \to [- π, π] \subseteq ℝ$
48	46 45 47	mp2an	$⊢ [- π, π] \subseteq ℝ$
49	14	sseli	$⊢ s \in A \to s \in [- π, π]$
50	48 49	sselid	$⊢ s \in A \to s \in ℝ$
51	50	adantl	$⊢ (φ \land s \in A) \to s \in ℝ$
52	44 51	readdcld	$⊢ (φ \land s \in A) \to X + s \in ℝ$
53	43 52	ffvelrnd	$⊢ (φ \land s \in A) \to F (X + s) \in ℝ$
54	3 4	ifcld	$⊢ φ \to if (0 < s, Y, W) \in ℝ$
55	54	adantr	$⊢ (φ \land s \in A) \to if (0 < s, Y, W) \in ℝ$
56	53 55	resubcld	$⊢ (φ \land s \in A) \to F (X + s) - if (0 < s, Y, W) \in ℝ$
57		simpr	$⊢ (φ \land s \in A) \to s \in A$
58	12 57	sselid	$⊢ (φ \land s \in A) \to s \in ([- π, π] ∖ \{0\})$
59	58	eldifbd	$⊢ (φ \land s \in A) \to \neg s \in \{0\}$
60		velsn	$⊢ s \in \{0\} \leftrightarrow s = 0$
61	59 60	sylnib	$⊢ (φ \land s \in A) \to \neg s = 0$
62	61	neqned	$⊢ (φ \land s \in A) \to s \neq 0$
63	56 51 62	redivcld	$⊢ (φ \land s \in A) \to \frac{F (X + s) - if (0 < s, Y, W)}{s} \in ℝ$
64	42 63	ifcld	$⊢ (φ \land s \in A) \to if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}) \in ℝ$
65	6	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})$
66	16 64 65	syl2anc	$⊢ (φ \land s \in A) \to H (s) = if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})$
67	61	iffalsed	$⊢ (φ \land s \in A) \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}$
68	66 67	eqtrd	$⊢ (φ \land s \in A) \to H (s) = \frac{F (X + s) - if (0 < s, Y, W)}{s}$
69		1red	$⊢ (φ \land s \in A) \to 1 \in ℝ$
70		2re	$⊢ 2 \in ℝ$
71	70	a1i	$⊢ (φ \land s \in A) \to 2 \in ℝ$
72	51	rehalfcld	$⊢ (φ \land s \in A) \to \frac{s}{2} \in ℝ$
73	72	resincld	$⊢ (φ \land s \in A) \to \sin (\frac{s}{2}) \in ℝ$
74	71 73	remulcld	$⊢ (φ \land s \in A) \to 2 \sin (\frac{s}{2}) \in ℝ$
75		2cnd	$⊢ (φ \land s \in A) \to 2 \in ℂ$
76	73	recnd	$⊢ (φ \land s \in A) \to \sin (\frac{s}{2}) \in ℂ$
77		2ne0	$⊢ 2 \neq 0$
78	77	a1i	$⊢ (φ \land s \in A) \to 2 \neq 0$
79		fourierdlem44	$⊢ (s \in [- π, π] \land s \neq 0) \to \sin (\frac{s}{2}) \neq 0$
80	16 62 79	syl2anc	$⊢ (φ \land s \in A) \to \sin (\frac{s}{2}) \neq 0$
81	75 76 78 80	mulne0d	$⊢ (φ \land s \in A) \to 2 \sin (\frac{s}{2}) \neq 0$
82	51 74 81	redivcld	$⊢ (φ \land s \in A) \to \frac{s}{2 \sin (\frac{s}{2})} \in ℝ$
83	69 82	ifcld	$⊢ (φ \land s \in A) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) \in ℝ$
84	7	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})})$
85	16 83 84	syl2anc	$⊢ (φ \land s \in A) \to K (s) = if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})$
86	61	iffalsed	$⊢ (φ \land s \in A) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) = \frac{s}{2 \sin (\frac{s}{2})}$
87	85 86	eqtrd	$⊢ (φ \land s \in A) \to K (s) = \frac{s}{2 \sin (\frac{s}{2})}$
88	68 87	oveq12d	$⊢ (φ \land s \in A) \to H (s) K (s) = (\frac{F (X + s) - if (0 < s, Y, W)}{s}) (\frac{s}{2 \sin (\frac{s}{2})})$
89	56	recnd	$⊢ (φ \land s \in A) \to F (X + s) - if (0 < s, Y, W) \in ℂ$
90	51	recnd	$⊢ (φ \land s \in A) \to s \in ℂ$
91	75 76	mulcld	$⊢ (φ \land s \in A) \to 2 \sin (\frac{s}{2}) \in ℂ$
92	89 90 91 62 81	dmdcan2d	$⊢ (φ \land s \in A) \to (\frac{F (X + s) - if (0 < s, Y, W)}{s}) (\frac{s}{2 \sin (\frac{s}{2})}) = \frac{F (X + s) - if (0 < s, Y, W)}{2 \sin (\frac{s}{2})}$
93	41 88 92	3eqtrd	$⊢ (φ \land s \in A) \to U (s) = \frac{F (X + s) - if (0 < s, Y, W)}{2 \sin (\frac{s}{2})}$
94	93	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to U (s) = \frac{F (X + s) - if (0 < s, Y, W)}{2 \sin (\frac{s}{2})}$
95	25	ad2antlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to n \in ℝ$
96		1red	$⊢ ((φ \land n \in ℕ) \land s \in A) \to 1 \in ℝ$
97	96	rehalfcld	$⊢ ((φ \land n \in ℕ) \land s \in A) \to \frac{1}{2} \in ℝ$
98	95 97	readdcld	$⊢ ((φ \land n \in ℕ) \land s \in A) \to n + (\frac{1}{2}) \in ℝ$
99	50	adantl	$⊢ ((φ \land n \in ℕ) \land s \in A) \to s \in ℝ$
100	98 99	remulcld	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (n + (\frac{1}{2})) s \in ℝ$
101	100	resincld	$⊢ ((φ \land n \in ℕ) \land s \in A) \to \sin (n + (\frac{1}{2})) s \in ℝ$
102	9	fvmpt2	$⊢ (s \in [- π, π] \land \sin (n + (\frac{1}{2})) s \in ℝ) \to S (s) = \sin (n + (\frac{1}{2})) s$
103	17 101 102	syl2anc	$⊢ ((φ \land n \in ℕ) \land s \in A) \to S (s) = \sin (n + (\frac{1}{2})) s$
104	94 103	oveq12d	$⊢ ((φ \land n \in ℕ) \land s \in A) \to U (s) S (s) = (\frac{F (X + s) - if (0 < s, Y, W)}{2 \sin (\frac{s}{2})}) \sin (n + (\frac{1}{2})) s$
105	89	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to F (X + s) - if (0 < s, Y, W) \in ℂ$
106	91	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to 2 \sin (\frac{s}{2}) \in ℂ$
107	101	recnd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to \sin (n + (\frac{1}{2})) s \in ℂ$
108	81	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to 2 \sin (\frac{s}{2}) \neq 0$
109	105 106 107 108	div32d	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (\frac{F (X + s) - if (0 < s, Y, W)}{2 \sin (\frac{s}{2})}) \sin (n + (\frac{1}{2})) s = (F (X + s) - if (0 < s, Y, W)) (\frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2})})$
110	25	adantr	$⊢ (n \in ℕ \land s \in A) \to n \in ℝ$
111		halfre	$⊢ \frac{1}{2} \in ℝ$
112	111	a1i	$⊢ (n \in ℕ \land s \in A) \to \frac{1}{2} \in ℝ$
113	110 112	readdcld	$⊢ (n \in ℕ \land s \in A) \to n + (\frac{1}{2}) \in ℝ$
114	50	adantl	$⊢ (n \in ℕ \land s \in A) \to s \in ℝ$
115	113 114	remulcld	$⊢ (n \in ℕ \land s \in A) \to (n + (\frac{1}{2})) s \in ℝ$
116	115	resincld	$⊢ (n \in ℕ \land s \in A) \to \sin (n + (\frac{1}{2})) s \in ℝ$
117	116	recnd	$⊢ (n \in ℕ \land s \in A) \to \sin (n + (\frac{1}{2})) s \in ℂ$
118	70	a1i	$⊢ (n \in ℕ \land s \in A) \to 2 \in ℝ$
119	114	rehalfcld	$⊢ (n \in ℕ \land s \in A) \to \frac{s}{2} \in ℝ$
120	119	resincld	$⊢ (n \in ℕ \land s \in A) \to \sin (\frac{s}{2}) \in ℝ$
121	118 120	remulcld	$⊢ (n \in ℕ \land s \in A) \to 2 \sin (\frac{s}{2}) \in ℝ$
122	121	recnd	$⊢ (n \in ℕ \land s \in A) \to 2 \sin (\frac{s}{2}) \in ℂ$
123		picn	$⊢ π \in ℂ$
124	123	a1i	$⊢ (n \in ℕ \land s \in A) \to π \in ℂ$
125		2cnd	$⊢ s \in A \to 2 \in ℂ$
126		rehalfcl	$⊢ s \in ℝ \to \frac{s}{2} \in ℝ$
127		resincl	$⊢ \frac{s}{2} \in ℝ \to \sin (\frac{s}{2}) \in ℝ$
128	50 126 127	3syl	$⊢ s \in A \to \sin (\frac{s}{2}) \in ℝ$
129	128	recnd	$⊢ s \in A \to \sin (\frac{s}{2}) \in ℂ$
130	77	a1i	$⊢ s \in A \to 2 \neq 0$
131		eldifsni	$⊢ s \in ([- π, π] ∖ \{0\}) \to s \neq 0$
132	131 11	eleq2s	$⊢ s \in A \to s \neq 0$
133	49 132 79	syl2anc	$⊢ s \in A \to \sin (\frac{s}{2}) \neq 0$
134	125 129 130 133	mulne0d	$⊢ s \in A \to 2 \sin (\frac{s}{2}) \neq 0$
135	134	adantl	$⊢ (n \in ℕ \land s \in A) \to 2 \sin (\frac{s}{2}) \neq 0$
136		0re	$⊢ 0 \in ℝ$
137		pipos	$⊢ 0 < π$
138	136 137	gtneii	$⊢ π \neq 0$
139	138	a1i	$⊢ (n \in ℕ \land s \in A) \to π \neq 0$
140	117 122 124 135 139	divdiv1d	$⊢ (n \in ℕ \land s \in A) \to \frac{\frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2})}}{π} = \frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2}) π}$
141		2cnd	$⊢ (n \in ℕ \land s \in A) \to 2 \in ℂ$
142	129	adantl	$⊢ (n \in ℕ \land s \in A) \to \sin (\frac{s}{2}) \in ℂ$
143	141 142 124	mulassd	$⊢ (n \in ℕ \land s \in A) \to 2 \sin (\frac{s}{2}) π = 2 \sin (\frac{s}{2}) π$
144	143	oveq2d	$⊢ (n \in ℕ \land s \in A) \to \frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2}) π} = \frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2}) π}$
145	142 124	mulcomd	$⊢ (n \in ℕ \land s \in A) \to \sin (\frac{s}{2}) π = π \sin (\frac{s}{2})$
146	145	oveq2d	$⊢ (n \in ℕ \land s \in A) \to 2 \sin (\frac{s}{2}) π = 2 π \sin (\frac{s}{2})$
147	141 124 142	mulassd	$⊢ (n \in ℕ \land s \in A) \to 2 π \sin (\frac{s}{2}) = 2 π \sin (\frac{s}{2})$
148	146 147	eqtr4d	$⊢ (n \in ℕ \land s \in A) \to 2 \sin (\frac{s}{2}) π = 2 π \sin (\frac{s}{2})$
149	148	oveq2d	$⊢ (n \in ℕ \land s \in A) \to \frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2}) π} = \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
150	140 144 149	3eqtrd	$⊢ (n \in ℕ \land s \in A) \to \frac{\frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2})}}{π} = \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
151	150	oveq2d	$⊢ (n \in ℕ \land s \in A) \to π (\frac{\frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2})}}{π}) = π (\frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})$
152	116 121 135	redivcld	$⊢ (n \in ℕ \land s \in A) \to \frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2})} \in ℝ$
153	152	recnd	$⊢ (n \in ℕ \land s \in A) \to \frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2})} \in ℂ$
154	153 124 139	divcan2d	$⊢ (n \in ℕ \land s \in A) \to π (\frac{\frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2})}}{π}) = \frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2})}$
155	5	dirkerval2	$⊢ (n \in ℕ \land s \in ℝ) \to D (n) (s) = if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})$
156	50 155	sylan2	$⊢ (n \in ℕ \land s \in A) \to D (n) (s) = if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})$
157		fourierdlem24	$⊢ s \in ([- π, π] ∖ \{0\}) \to s \mod 2 π \neq 0$
158	157 11	eleq2s	$⊢ s \in A \to s \mod 2 π \neq 0$
159	158	neneqd	$⊢ s \in A \to \neg s \mod 2 π = 0$
160	159	adantl	$⊢ (n \in ℕ \land s \in A) \to \neg s \mod 2 π = 0$
161	160	iffalsed	$⊢ (n \in ℕ \land s \in A) \to if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}) = \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
162	156 161	eqtr2d	$⊢ (n \in ℕ \land s \in A) \to \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})} = D (n) (s)$
163	162	oveq2d	$⊢ (n \in ℕ \land s \in A) \to π (\frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}) = π D (n) (s)$
164	151 154 163	3eqtr3d	$⊢ (n \in ℕ \land s \in A) \to \frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2})} = π D (n) (s)$
165	164	oveq2d	$⊢ (n \in ℕ \land s \in A) \to (F (X + s) - if (0 < s, Y, W)) (\frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2})}) = (F (X + s) - if (0 < s, Y, W)) π D (n) (s)$
166	165	adantll	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (F (X + s) - if (0 < s, Y, W)) (\frac{\sin (n + (\frac{1}{2})) s}{2 \sin (\frac{s}{2})}) = (F (X + s) - if (0 < s, Y, W)) π D (n) (s)$
167	123	a1i	$⊢ ((φ \land n \in ℕ) \land s \in A) \to π \in ℂ$
168	5	dirkerre	$⊢ (n \in ℕ \land s \in ℝ) \to D (n) (s) \in ℝ$
169	50 168	sylan2	$⊢ (n \in ℕ \land s \in A) \to D (n) (s) \in ℝ$
170	169	recnd	$⊢ (n \in ℕ \land s \in A) \to D (n) (s) \in ℂ$
171	170	adantll	$⊢ ((φ \land n \in ℕ) \land s \in A) \to D (n) (s) \in ℂ$
172	105 167 171	mul12d	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (F (X + s) - if (0 < s, Y, W)) π D (n) (s) = π (F (X + s) - if (0 < s, Y, W)) D (n) (s)$
173	109 166 172	3eqtrd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (\frac{F (X + s) - if (0 < s, Y, W)}{2 \sin (\frac{s}{2})}) \sin (n + (\frac{1}{2})) s = π (F (X + s) - if (0 < s, Y, W)) D (n) (s)$
174	32 104 173	3eqtrd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to G (s) = π (F (X + s) - if (0 < s, Y, W)) D (n) (s)$

Metamath Proof Explorer

Theorem fourierdlem66

Proof