Theorem fourierdlem95

Description: Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem95.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem95.xre	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem95.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem95.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	fourierdlem95.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
	fourierdlem95.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝑉 )
	fourierdlem95.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
	fourierdlem95.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
	fourierdlem95.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
	fourierdlem95.h	⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
	fourierdlem95.k	⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
	fourierdlem95.u	⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
	fourierdlem95.s	⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) )
	fourierdlem95.g	⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
	fourierdlem95.i	⊢ 𝐼 = ( ℝ D 𝐹 )
	fourierdlem95.ifn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
	fourierdlem95.b	⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝐼 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
	fourierdlem95.c	⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐼 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
	fourierdlem95.y	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
	fourierdlem95.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
	fourierdlem95.admvol	⊢ ( 𝜑 → 𝐴 ∈ dom vol )
	fourierdlem95.ass	⊢ ( 𝜑 → 𝐴 ⊆ ( ( - π [,] π ) ∖ { 0 } ) )
	fourierlemenplusacver2eqitgdirker.e	⊢ 𝐸 = ( 𝑛 ∈ ℕ ↦ ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) )
	fourierdlem95.d	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
	fourierdlem95.o	⊢ ( 𝜑 → 𝑂 ∈ ℝ )
	fourierdlem95.ifeqo	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑂 )
	fourierdlem95.itgdirker	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 = ( 1 / 2 ) )
Assertion	fourierdlem95	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸 ‘ 𝑛 ) + ( 𝑂 / 2 ) ) = ∫ 𝐴 ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem95.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		fourierdlem95.xre	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3		fourierdlem95.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
4		fourierdlem95.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5		fourierdlem95.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
6		fourierdlem95.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝑉 )
7		fourierdlem95.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
8		fourierdlem95.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
9		fourierdlem95.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
10		fourierdlem95.h	⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
11		fourierdlem95.k	⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
12		fourierdlem95.u	⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
13		fourierdlem95.s	⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) )
14		fourierdlem95.g	⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
15		fourierdlem95.i	⊢ 𝐼 = ( ℝ D 𝐹 )
16		fourierdlem95.ifn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
17		fourierdlem95.b	⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝐼 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
18		fourierdlem95.c	⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐼 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
19		fourierdlem95.y	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
20		fourierdlem95.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
21		fourierdlem95.admvol	⊢ ( 𝜑 → 𝐴 ∈ dom vol )
22		fourierdlem95.ass	⊢ ( 𝜑 → 𝐴 ⊆ ( ( - π [,] π ) ∖ { 0 } ) )
23		fourierlemenplusacver2eqitgdirker.e	⊢ 𝐸 = ( 𝑛 ∈ ℕ ↦ ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) )
24		fourierdlem95.d	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
25		fourierdlem95.o	⊢ ( 𝜑 → 𝑂 ∈ ℝ )
26		fourierdlem95.ifeqo	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑂 )
27		fourierdlem95.itgdirker	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 = ( 1 / 2 ) )
28		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
29	22	difss2d	⊢ ( 𝜑 → 𝐴 ⊆ ( - π [,] π ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ( - π [,] π ) )
31	30	sselda	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ( - π [,] π ) )
32	1	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 : ℝ ⟶ ℝ )
33	2	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ ℝ )
34		ioossre	⊢ ( 𝑋 (,) +∞ ) ⊆ ℝ
35	34	a1i	⊢ ( 𝜑 → ( 𝑋 (,) +∞ ) ⊆ ℝ )
36	1 35	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) : ( 𝑋 (,) +∞ ) ⟶ ℝ )
37		ioosscn	⊢ ( 𝑋 (,) +∞ ) ⊆ ℂ
38	37	a1i	⊢ ( 𝜑 → ( 𝑋 (,) +∞ ) ⊆ ℂ )
39		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
40		pnfxr	⊢ +∞ ∈ ℝ*
41	40	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
42	2	ltpnfd	⊢ ( 𝜑 → 𝑋 < +∞ )
43	39 41 2 42	lptioo1cn	⊢ ( 𝜑 → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑋 (,) +∞ ) ) )
44	36 38 43 19	limcrecl	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑌 ∈ ℝ )
46		ioossre	⊢ ( -∞ (,) 𝑋 ) ⊆ ℝ
47	46	a1i	⊢ ( 𝜑 → ( -∞ (,) 𝑋 ) ⊆ ℝ )
48	1 47	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) : ( -∞ (,) 𝑋 ) ⟶ ℝ )
49		ioosscn	⊢ ( -∞ (,) 𝑋 ) ⊆ ℂ
50	49	a1i	⊢ ( 𝜑 → ( -∞ (,) 𝑋 ) ⊆ ℂ )
51		mnfxr	⊢ -∞ ∈ ℝ*
52	51	a1i	⊢ ( 𝜑 → -∞ ∈ ℝ* )
53	2	mnfltd	⊢ ( 𝜑 → -∞ < 𝑋 )
54	39 52 2 53	lptioo2cn	⊢ ( 𝜑 → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( -∞ (,) 𝑋 ) ) )
55	48 50 54 20	limcrecl	⊢ ( 𝜑 → 𝑊 ∈ ℝ )
56	55	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ ℝ )
57	28	nnred	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ )
58	32 33 45 56 10 11 12 57 13 14	fourierdlem67	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 : ( - π [,] π ) ⟶ ℝ )
59	58	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝐺 ‘ 𝑠 ) ∈ ℝ )
60	31 59	syldan	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑠 ) ∈ ℝ )
61	21	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ dom vol )
62	58	feqmptd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
63	6	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ ran 𝑉 )
64	19	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
65	20	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
66	4	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 ∈ ℕ )
67	5	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
68	7	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
69	8	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
70	9	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
71		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝑉 ‘ 𝑗 ) = ( 𝑉 ‘ 𝑖 ) )
72	71	oveq1d	⊢ ( 𝑗 = 𝑖 → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
73	72	cbvmptv	⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
74		eqid	⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
75	16	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
76	17	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ( ( 𝐼 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
77	18	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ( ( 𝐼 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
78	3 32 63 64 65 10 11 12 57 13 14 66 67 68 69 70 73 74 15 75 76 77	fourierdlem88	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 ∈ 𝐿1 )
79	62 78	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ ( - π [,] π ) ↦ ( 𝐺 ‘ 𝑠 ) ) ∈ 𝐿1 )
80	30 61 59 79	iblss	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑠 ) ) ∈ 𝐿1 )
81	60 80	itgrecl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 ∈ ℝ )
82		pire	⊢ π ∈ ℝ
83	82	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ∈ ℝ )
84		pipos	⊢ 0 < π
85	82 84	gt0ne0ii	⊢ π ≠ 0
86	85	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ≠ 0 )
87	81 83 86	redivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) ∈ ℝ )
88	23	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) ∈ ℝ ) → ( 𝐸 ‘ 𝑛 ) = ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) )
89	28 87 88	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑛 ) = ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) )
90	25	recnd	⊢ ( 𝜑 → 𝑂 ∈ ℂ )
91		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
92		2ne0	⊢ 2 ≠ 0
93	92	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
94	90 91 93	divrecd	⊢ ( 𝜑 → ( 𝑂 / 2 ) = ( 𝑂 · ( 1 / 2 ) ) )
95	94	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑂 / 2 ) = ( 𝑂 · ( 1 / 2 ) ) )
96	27	eqcomd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 2 ) = ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 )
97	96	oveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑂 · ( 1 / 2 ) ) = ( 𝑂 · ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 ) )
98	95 97	eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑂 / 2 ) = ( 𝑂 · ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 ) )
99	89 98	oveq12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸 ‘ 𝑛 ) + ( 𝑂 / 2 ) ) = ( ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) + ( 𝑂 · ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 ) ) )
100	22	sselda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) )
101	100	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) )
102		eqid	⊢ ( ( - π [,] π ) ∖ { 0 } ) = ( ( - π [,] π ) ∖ { 0 } )
103	1 2 44 55 24 10 11 12 13 14 102	fourierdlem66	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ) → ( 𝐺 ‘ 𝑠 ) = ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
104	101 103	syldan	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑠 ) = ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
105	104	itgeq2dv	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 = ∫ 𝐴 ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 )
106	105	oveq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) = ( ∫ 𝐴 ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 / π ) )
107	83	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ∈ ℂ )
108	1	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝐹 : ℝ ⟶ ℝ )
109	2	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑋 ∈ ℝ )
110		difss	⊢ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( - π [,] π )
111	82	renegcli	⊢ - π ∈ ℝ
112		iccssre	⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
113	111 82 112	mp2an	⊢ ( - π [,] π ) ⊆ ℝ
114	110 113	sstri	⊢ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ℝ
115	114 100	sselid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℝ )
116	109 115	readdcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
117	108 116	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
118	44 55	ifcld	⊢ ( 𝜑 → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
119	118	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
120	117 119	resubcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℝ )
121	120	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℝ )
122	28	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑛 ∈ ℕ )
123	115	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℝ )
124	24	dirkerre	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℝ )
125	122 123 124	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℝ )
126	121 125	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ℝ )
127	104	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( 𝐺 ‘ 𝑠 ) )
128	127	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) / π ) = ( ( 𝐺 ‘ 𝑠 ) / π ) )
129		picn	⊢ π ∈ ℂ
130	129	a1i	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → π ∈ ℂ )
131	126	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ℂ )
132	85	a1i	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → π ≠ 0 )
133	130 131 130 132	div23d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) / π ) = ( ( π / π ) · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
134	60	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑠 ) ∈ ℂ )
135	134 130 132	divrec2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑠 ) / π ) = ( ( 1 / π ) · ( 𝐺 ‘ 𝑠 ) ) )
136	128 133 135	3eqtr3rd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 1 / π ) · ( 𝐺 ‘ 𝑠 ) ) = ( ( π / π ) · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
137	129 85	dividi	⊢ ( π / π ) = 1
138	137	a1i	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( π / π ) = 1 )
139	138	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( π / π ) · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( 1 · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
140	131	mullidd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 1 · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
141	136 139 140	3eqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) = ( ( 1 / π ) · ( 𝐺 ‘ 𝑠 ) ) )
142	141	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( 𝑠 ∈ 𝐴 ↦ ( ( 1 / π ) · ( 𝐺 ‘ 𝑠 ) ) ) )
143	107 86	reccld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / π ) ∈ ℂ )
144	143 60 80	iblmulc2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( ( 1 / π ) · ( 𝐺 ‘ 𝑠 ) ) ) ∈ 𝐿1 )
145	142 144	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) ∈ 𝐿1 )
146	107 126 145	itgmulc2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( π · ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) = ∫ 𝐴 ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 )
147	146	eqcomd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 = ( π · ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) )
148	147	oveq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐴 ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 / π ) = ( ( π · ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) / π ) )
149	126 145	itgcl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ∈ ℂ )
150	149 107 86	divcan3d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( π · ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) / π ) = ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )
151	106 148 150	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) = ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )
152	90	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑂 ∈ ℂ )
153	113	sseli	⊢ ( 𝑠 ∈ ( - π [,] π ) → 𝑠 ∈ ℝ )
154	153 124	sylan2	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℝ )
155	154	adantll	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℝ )
156	111	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → - π ∈ ℝ )
157		ax-resscn	⊢ ℝ ⊆ ℂ
158	157	a1i	⊢ ( 𝑛 ∈ ℕ → ℝ ⊆ ℂ )
159		ssid	⊢ ℂ ⊆ ℂ
160		cncfss	⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( - π [,] π ) –cn→ ℝ ) ⊆ ( ( - π [,] π ) –cn→ ℂ ) )
161	158 159 160	sylancl	⊢ ( 𝑛 ∈ ℕ → ( ( - π [,] π ) –cn→ ℝ ) ⊆ ( ( - π [,] π ) –cn→ ℂ ) )
162		eqid	⊢ ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) = ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) )
163	24	dirkerf	⊢ ( 𝑛 ∈ ℕ → ( 𝐷 ‘ 𝑛 ) : ℝ ⟶ ℝ )
164	163	feqmptd	⊢ ( 𝑛 ∈ ℕ → ( 𝐷 ‘ 𝑛 ) = ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
165	24	dirkercncf	⊢ ( 𝑛 ∈ ℕ → ( 𝐷 ‘ 𝑛 ) ∈ ( ℝ –cn→ ℝ ) )
166	164 165	eqeltrrd	⊢ ( 𝑛 ∈ ℕ → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℝ ) )
167	113	a1i	⊢ ( 𝑛 ∈ ℕ → ( - π [,] π ) ⊆ ℝ )
168		ssid	⊢ ℝ ⊆ ℝ
169	168	a1i	⊢ ( 𝑛 ∈ ℕ → ℝ ⊆ ℝ )
170	162 166 167 169 154	cncfmptssg	⊢ ( 𝑛 ∈ ℕ → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℝ ) )
171	161 170	sseldd	⊢ ( 𝑛 ∈ ℕ → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℂ ) )
172	171	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℂ ) )
173		cniccibl	⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ∧ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℂ ) ) → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ 𝐿1 )
174	156 83 172 173	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ 𝐿1 )
175	30 61 155 174	iblss	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ 𝐿1 )
176	152 125 175	itgmulc2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑂 · ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 ) = ∫ 𝐴 ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )
177	151 176	oveq12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ∫ 𝐴 ( 𝐺 ‘ 𝑠 ) d 𝑠 / π ) + ( 𝑂 · ∫ 𝐴 ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) d 𝑠 ) ) = ( ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 + ∫ 𝐴 ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) )
178	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑂 ∈ ℝ )
179	178 125	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ℝ )
180	152 125 175	iblmulc2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑠 ∈ 𝐴 ↦ ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) ∈ 𝐿1 )
181	126 145 179 180	itgadd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 = ( ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 + ∫ 𝐴 ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) )
182	26	eqcomd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑂 = if ( 0 < 𝑠 , 𝑌 , 𝑊 ) )
183	182	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑂 = if ( 0 < 𝑠 , 𝑌 , 𝑊 ) )
184	183	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) = ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
185	184	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
186	117	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
187	186	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
188	119	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ )
189	188	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ )
190	125	recnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℂ )
191	187 189 190	subdird	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) − ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
192	191	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) − ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) + ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
193	187 190	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ℂ )
194	189 190	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ∈ ℂ )
195	193 194	npcand	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) − ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) + ( if ( 0 < 𝑠 , 𝑌 , 𝑊 ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
196	185 192 195	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
197	196	itgeq2dv	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∫ 𝐴 ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) + ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) d 𝑠 = ∫ 𝐴 ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )
198	181 197	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫ 𝐴 ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 + ∫ 𝐴 ( 𝑂 · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 ) = ∫ 𝐴 ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )
199	99 177 198	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸 ‘ 𝑛 ) + ( 𝑂 / 2 ) ) = ∫ 𝐴 ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) d 𝑠 )