Theorem fourierdlem88

Description: Given a piecewise continuous function F , a continuous function K and a continuous function S , the function G is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem88.1	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem88.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem88.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝑉 )
	fourierdlem88.y	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
	fourierdlem88.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
	fourierdlem88.h	⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
	fourierdlem88.k	⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
	fourierdlem88.u	⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
	fourierdlem88.n	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
	fourierdlem88.s	⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
	fourierdlem88.g	⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
	fourierdlem88.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	fourierdlem88.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
	fourierdlem88.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
	fourierdlem88.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
	fourierdlem88.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
	fourierdlem88.q	⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
	fourierdlem88.o	⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem88.i	⊢ 𝐼 = ( ℝ D 𝐹 )
	fourierdlem88.ifn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
	fourierdlem88.c	⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐼 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
	fourierdlem88.d	⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝐼 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
Assertion	fourierdlem88	⊢ ( 𝜑 → 𝐺 ∈ 𝐿1 )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem88.1	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2		fourierdlem88.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
3		fourierdlem88.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝑉 )
4		fourierdlem88.y	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
5		fourierdlem88.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
6		fourierdlem88.h	⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
7		fourierdlem88.k	⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
8		fourierdlem88.u	⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
9		fourierdlem88.n	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
10		fourierdlem88.s	⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
11		fourierdlem88.g	⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
12		fourierdlem88.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
13		fourierdlem88.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
14		fourierdlem88.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
15		fourierdlem88.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
16		fourierdlem88.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
17		fourierdlem88.q	⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
18		fourierdlem88.o	⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
19		fourierdlem88.i	⊢ 𝐼 = ( ℝ D 𝐹 )
20		fourierdlem88.ifn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
21		fourierdlem88.c	⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐼 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
22		fourierdlem88.d	⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝐼 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
23		pire	⊢ π ∈ ℝ
24	23	a1i	⊢ ( 𝜑 → π ∈ ℝ )
25	24	renegcld	⊢ ( 𝜑 → - π ∈ ℝ )
26	1	fourierdlem2	⊢ ( 𝑀 ∈ ℕ → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
27	12 26	syl	⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
28	13 27	mpbid	⊢ ( 𝜑 → ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
29	28	simpld	⊢ ( 𝜑 → 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
30		elmapi	⊢ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
31		frn	⊢ ( 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ → ran 𝑉 ⊆ ℝ )
32	29 30 31	3syl	⊢ ( 𝜑 → ran 𝑉 ⊆ ℝ )
33	32 3	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
34	25 24 33 1 18 12 13 17	fourierdlem14	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) )
35		ioossre	⊢ ( 𝑋 (,) +∞ ) ⊆ ℝ
36	35	a1i	⊢ ( 𝜑 → ( 𝑋 (,) +∞ ) ⊆ ℝ )
37	2 36	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) : ( 𝑋 (,) +∞ ) ⟶ ℝ )
38		ax-resscn	⊢ ℝ ⊆ ℂ
39	36 38	sstrdi	⊢ ( 𝜑 → ( 𝑋 (,) +∞ ) ⊆ ℂ )
40		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
41		pnfxr	⊢ +∞ ∈ ℝ*
42	41	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
43	33	ltpnfd	⊢ ( 𝜑 → 𝑋 < +∞ )
44	40 42 33 43	lptioo1cn	⊢ ( 𝜑 → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑋 (,) +∞ ) ) )
45	37 39 44 4	limcrecl	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
46		ioossre	⊢ ( -∞ (,) 𝑋 ) ⊆ ℝ
47	46	a1i	⊢ ( 𝜑 → ( -∞ (,) 𝑋 ) ⊆ ℝ )
48	2 47	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) : ( -∞ (,) 𝑋 ) ⟶ ℝ )
49	47 38	sstrdi	⊢ ( 𝜑 → ( -∞ (,) 𝑋 ) ⊆ ℂ )
50		mnfxr	⊢ -∞ ∈ ℝ*
51	50	a1i	⊢ ( 𝜑 → -∞ ∈ ℝ* )
52	33	mnfltd	⊢ ( 𝜑 → -∞ < 𝑋 )
53	40 51 33 52	lptioo2cn	⊢ ( 𝜑 → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( -∞ (,) 𝑋 ) ) )
54	48 49 53 5	limcrecl	⊢ ( 𝜑 → 𝑊 ∈ ℝ )
55	2 33 45 54 6 7 8	fourierdlem55	⊢ ( 𝜑 → 𝑈 : ( - π [,] π ) ⟶ ℝ )
56	55	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑈 ‘ 𝑠 ) ∈ ℝ )
57	10	fourierdlem5	⊢ ( 𝑁 ∈ ℝ → 𝑆 : ( - π [,] π ) ⟶ ℝ )
58	9 57	syl	⊢ ( 𝜑 → 𝑆 : ( - π [,] π ) ⟶ ℝ )
59	58	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑆 ‘ 𝑠 ) ∈ ℝ )
60	56 59	remulcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ∈ ℝ )
61	60	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ∈ ℂ )
62	61 11	fmptd	⊢ ( 𝜑 → 𝐺 : ( - π [,] π ) ⟶ ℂ )
63		ssid	⊢ ℂ ⊆ ℂ
64		cncfss	⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℝ ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
65	38 63 64	mp2an	⊢ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℝ ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ )
66	2	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : ℝ ⟶ ℝ )
67	18 12 34	fourierdlem15	⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
68	67	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
69		elfzofz	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
70	69	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
71	68 70	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( - π [,] π ) )
72		fzofzp1	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
73	72	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
74	68 73	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( - π [,] π ) )
75	33	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ )
76	1 12 13 3	fourierdlem12	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
77	75	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℂ )
78	77	addlidd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 0 + 𝑋 ) = 𝑋 )
79	23	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → π ∈ ℝ )
80	79	renegcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → - π ∈ ℝ )
81	80 75	readdcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( - π + 𝑋 ) ∈ ℝ )
82	79 75	readdcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( π + 𝑋 ) ∈ ℝ )
83	81 82	iccssred	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ⊆ ℝ )
84	1 12 13	fourierdlem15	⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
85	84	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
86	85 70	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
87	83 86	sseldd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
88	87 75	resubcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ )
89	17	fvmpt2	⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
90	70 88 89	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
91	90	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) = ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) + 𝑋 ) )
92	87	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℂ )
93	92 77	npcand	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) + 𝑋 ) = ( 𝑉 ‘ 𝑖 ) )
94	91 93	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) = ( 𝑉 ‘ 𝑖 ) )
95		fveq2	⊢ ( 𝑖 = 𝑗 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑗 ) )
96	95	oveq1d	⊢ ( 𝑖 = 𝑗 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
97	96	cbvmptv	⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
98	17 97	eqtri	⊢ 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
99	98	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) )
100		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → 𝑗 = ( 𝑖 + 1 ) )
101	100	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → ( 𝑉 ‘ 𝑗 ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
102	101	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
103	85 73	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
104	83 103	sseldd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
105	104 75	resubcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ )
106	99 102 73 105	fvmptd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
107	106	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑋 ) = ( ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) + 𝑋 ) )
108	104	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
109	108 77	npcand	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) + 𝑋 ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
110	107 109	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑋 ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
111	94 110	oveq12d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑋 ) ) = ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
112	78 111	eleq12d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 0 + 𝑋 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑋 ) ) ↔ 𝑋 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
113	76 112	mtbird	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ ( 0 + 𝑋 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑋 ) ) )
114		0red	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 0 ∈ ℝ )
115	90 88	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
116	106 105	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
117	114 115 116 75	eliooshift	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 0 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 0 + 𝑋 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑋 ) ) ) )
118	113 117	mtbird	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 0 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
119	111	reseq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑋 ) ) ) = ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
120	111	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑋 ) ) –cn→ ℂ ) = ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
121	14 119 120	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑋 ) ) ) ∈ ( ( ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑋 ) ) –cn→ ℂ ) )
122	45	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑌 ∈ ℝ )
123	54	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑊 ∈ ℝ )
124	9	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑁 ∈ ℝ )
125	66 71 74 75 118 121 122 123 6 7 8 124 10 11	fourierdlem78	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℝ ) )
126	65 125	sselid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
127		eqid	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) )
128		eqid	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) )
129		eqid	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
130	23	renegcli	⊢ - π ∈ ℝ
131	130	rexri	⊢ - π ∈ ℝ*
132	131	a1i	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → - π ∈ ℝ* )
133	23	rexri	⊢ π ∈ ℝ*
134	133	a1i	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → π ∈ ℝ* )
135	68	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
136		simplr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
137	132 134 135 136	fourierdlem8	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
138		ioossicc	⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
139	138	sseli	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
140	139	adantl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
141	137 140	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ( - π [,] π ) )
142	2 33 45 54 6	fourierdlem9	⊢ ( 𝜑 → 𝐻 : ( - π [,] π ) ⟶ ℝ )
143	142	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐻 : ( - π [,] π ) ⟶ ℝ )
144	143 141	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) ∈ ℝ )
145	7	fourierdlem43	⊢ 𝐾 : ( - π [,] π ) ⟶ ℝ
146	145	a1i	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐾 : ( - π [,] π ) ⟶ ℝ )
147	146 141	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐾 ‘ 𝑠 ) ∈ ℝ )
148	144 147	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ∈ ℝ )
149	8	fvmpt2	⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ∈ ℝ ) → ( 𝑈 ‘ 𝑠 ) = ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
150	141 148 149	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑈 ‘ 𝑠 ) = ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
151	150 148	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑈 ‘ 𝑠 ) ∈ ℝ )
152	151	recnd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑈 ‘ 𝑠 ) ∈ ℂ )
153	9 10	fourierdlem18	⊢ ( 𝜑 → 𝑆 ∈ ( ( - π [,] π ) –cn→ ℝ ) )
154		cncff	⊢ ( 𝑆 ∈ ( ( - π [,] π ) –cn→ ℝ ) → 𝑆 : ( - π [,] π ) ⟶ ℝ )
155	153 154	syl	⊢ ( 𝜑 → 𝑆 : ( - π [,] π ) ⟶ ℝ )
156	155	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑆 : ( - π [,] π ) ⟶ ℝ )
157	156	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑆 : ( - π [,] π ) ⟶ ℝ )
158	157 141	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑠 ) ∈ ℝ )
159	158	recnd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑠 ) ∈ ℂ )
160		eqid	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) )
161		eqid	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) )
162		eqid	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
163	144	recnd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) ∈ ℂ )
164	147	recnd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐾 ‘ 𝑠 ) ∈ ℂ )
165	38	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ℝ ⊆ ℂ )
166	20 165	fssd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
167		eqid	⊢ if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐷 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) = if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐷 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) )
168	33 1 2 3 4 54 6 12 13 15 17 18 19 166 22 167	fourierdlem75	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐷 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
169	142	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐻 : ( - π [,] π ) ⟶ ℝ )
170	131	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → - π ∈ ℝ* )
171	133	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → π ∈ ℝ* )
172		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
173	170 171 68 172	fourierdlem8	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
174	138 173	sstrid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
175	169 174	feqresmpt	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
176	175	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
177	168 176	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐷 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
178		limcresi	⊢ ( 𝐾 limℂ ( 𝑄 ‘ 𝑖 ) ) ⊆ ( ( 𝐾 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) )
179	7	fourierdlem62	⊢ 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ )
180	179	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ ) )
181	180 71	cnlimci	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( 𝐾 limℂ ( 𝑄 ‘ 𝑖 ) ) )
182	178 181	sselid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( ( 𝐾 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
183	145	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐾 : ( - π [,] π ) ⟶ ℝ )
184	183 174	feqresmpt	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐾 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) ) )
185	184	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐾 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
186	182 185	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
187	160 161 162 163 164 177 186	mullimc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐷 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
188	150	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) = ( 𝑈 ‘ 𝑠 ) )
189	188	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) ) )
190	189	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
191	187 190	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐷 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
192		limcresi	⊢ ( 𝑆 limℂ ( 𝑄 ‘ 𝑖 ) ) ⊆ ( ( 𝑆 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) )
193	153	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑆 ∈ ( ( - π [,] π ) –cn→ ℝ ) )
194	193 71	cnlimci	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( 𝑆 limℂ ( 𝑄 ‘ 𝑖 ) ) )
195	192 194	sselid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( ( 𝑆 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
196	156 174	feqresmpt	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) ) )
197	196	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
198	195 197	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
199	127 128 129 152 159 191 198	mullimc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐷 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝑆 ‘ ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
200	60 11	fmptd	⊢ ( 𝜑 → 𝐺 : ( - π [,] π ) ⟶ ℝ )
201	200	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐺 : ( - π [,] π ) ⟶ ℝ )
202	201 174	feqresmpt	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
203	151 158	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ∈ ℝ )
204	11	fvmpt2	⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ∈ ℝ ) → ( 𝐺 ‘ 𝑠 ) = ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
205	141 203 204	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐺 ‘ 𝑠 ) = ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
206	205	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐺 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) )
207	202 206	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) = ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
208	207	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
209	199 208	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐷 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝑆 ‘ ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
210		eqid	⊢ if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐶 , ( ( 𝐿 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐶 , ( ( 𝐿 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
211	33 1 2 3 45 5 6 12 13 16 17 18 19 20 21 210	fourierdlem74	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐶 , ( ( 𝐿 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
212	175	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
213	211 212	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐶 , ( ( 𝐿 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
214		limcresi	⊢ ( 𝐾 limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝐾 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
215	180 74	cnlimci	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐾 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ ( 𝐾 limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
216	214 215	sselid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐾 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ ( ( 𝐾 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
217	184	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐾 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
218	216 217	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐾 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
219	160 161 162 163 164 213 218	mullimc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐶 , ( ( 𝐿 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
220	189	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
221	219 220	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐶 , ( ( 𝐿 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
222		limcresi	⊢ ( 𝑆 limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑆 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
223	193 74	cnlimci	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ ( 𝑆 limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
224	222 223	sselid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ ( ( 𝑆 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
225	196	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
226	224 225	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
227	127 128 129 152 159 221 226	mullimc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐶 , ( ( 𝐿 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) · ( 𝑆 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
228	207	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
229	227 228	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐶 , ( ( 𝐿 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) · ( 𝑆 ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
230	18 12 34 62 126 209 229	fourierdlem69	⊢ ( 𝜑 → 𝐺 ∈ 𝐿1 )