Theorem 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	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem66.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem66.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
	fourierdlem66.w	⊢ ( 𝜑 → 𝑊 ∈ ℝ )
	fourierdlem66.d	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
	fourierdlem66.h	⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
	fourierdlem66.k	⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
	fourierdlem66.u	⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
	fourierdlem66.s	⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) )
	fourierdlem66.g	⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
	fourierdlem66.a	⊢ 𝐴 = ( ( - π [,] π ) ∖ { 0 } )
Assertion	fourierdlem66	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑠 ) = ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )

Proof

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