Theorem fourierdlem100

Description: A piecewise continuous function is integrable on any closed interval. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierlemiblglemlem.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem100.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
	fourierdlem100.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	fourierdlem100.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
	fourierdlem100.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
	fourierdlem100.per	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
	fourierdlem100.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
	fourierdlem100.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
	fourierdlem100.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
	fourierdlem100.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	fourierdlem100.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
	fourierdlem100.o	⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem100.n	⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
	fourierdlem100.h	⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
	fourierdlem100.s	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
	fourierdlem100.e	⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
	fourierdlem100.j	⊢ 𝐽 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
	fourierdlem100.i	⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
Assertion	fourierdlem100	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )

Proof

Step	Hyp	Ref	Expression
1		fourierlemiblglemlem.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2		fourierdlem100.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
3		fourierdlem100.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4		fourierdlem100.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5		fourierdlem100.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
6		fourierdlem100.per	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
7		fourierdlem100.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
8		fourierdlem100.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
9		fourierdlem100.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
10		fourierdlem100.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
11		fourierdlem100.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
12		fourierdlem100.o	⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
13		fourierdlem100.n	⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
14		fourierdlem100.h	⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
15		fourierdlem100.s	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
16		fourierdlem100.e	⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
17		fourierdlem100.j	⊢ 𝐽 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
18		fourierdlem100.i	⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
19		elioore	⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) → 𝐷 ∈ ℝ )
20	11 19	syl	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
21	10 20	iccssred	⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℝ )
22	5 21	feqresmpt	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) = ( 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
23		fveq2	⊢ ( 𝑖 = 𝑗 → ( 𝑝 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑗 ) )
24		oveq1	⊢ ( 𝑖 = 𝑗 → ( 𝑖 + 1 ) = ( 𝑗 + 1 ) )
25	24	fveq2d	⊢ ( 𝑖 = 𝑗 → ( 𝑝 ‘ ( 𝑖 + 1 ) ) = ( 𝑝 ‘ ( 𝑗 + 1 ) ) )
26	23 25	breq12d	⊢ ( 𝑖 = 𝑗 → ( ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) )
27	26	cbvralvw	⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) )
28	27	anbi2i	⊢ ( ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) )
29	28	a1i	⊢ ( 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) → ( ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) ) )
30	29	rabbiia	⊢ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } = { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) }
31	30	mpteq2i	⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) } )
32	12 31	eqtri	⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) } )
33		elioo4g	⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) ↔ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) ) )
34	11 33	sylib	⊢ ( 𝜑 → ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) ) )
35	34	simprd	⊢ ( 𝜑 → ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) )
36	35	simpld	⊢ ( 𝜑 → 𝐶 < 𝐷 )
37		id	⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
38	2	eqcomi	⊢ ( 𝐵 − 𝐴 ) = 𝑇
39	38	oveq2i	⊢ ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( 𝑘 · 𝑇 )
40	39	a1i	⊢ ( 𝑦 = 𝑥 → ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( 𝑘 · 𝑇 ) )
41	37 40	oveq12d	⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
42	41	eleq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
43	42	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
44	43	cbvrabv	⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } = { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
45	44	uneq2i	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
46	39	eqcomi	⊢ ( 𝑘 · 𝑇 ) = ( 𝑘 · ( 𝐵 − 𝐴 ) )
47	46	oveq2i	⊢ ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) )
48	47	eleq1i	⊢ ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
49	48	rexbii	⊢ ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
50	49	rgenw	⊢ ∀ 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
51		rabbi	⊢ ( ∀ 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) ↔ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
52	50 51	mpbi	⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 }
53	52	uneq2i	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
54	14 53	eqtri	⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
55	54	fveq2i	⊢ ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
56	55	oveq1i	⊢ ( ( ♯ ‘ 𝐻 ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
57	13 56	eqtri	⊢ 𝑁 = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
58		isoeq5	⊢ ( 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) → ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ) )
59	54 58	ax-mp	⊢ ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
60	59	iotabii	⊢ ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
61	15 60	eqtri	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
62	2 1 3 4 10 20 36 12 45 57 61	fourierdlem54	⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ) )
63	62	simpld	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) )
64	63	simpld	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
65	63	simprd	⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
66	5 21	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) : ( 𝐶 [,] 𝐷 ) ⟶ ℂ )
67		ioossicc	⊢ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
68	10	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ∈ ℝ )
69	68	rexrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ∈ ℝ* )
70	11	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
71	70 19	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐷 ∈ ℝ )
72	71	rexrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐷 ∈ ℝ* )
73	12 64 65	fourierdlem15	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐶 [,] 𝐷 ) )
74	73	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐶 [,] 𝐷 ) )
75		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
76	69 72 74 75	fourierdlem8	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐶 [,] 𝐷 ) )
77	67 76	sstrid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐶 [,] 𝐷 ) )
78	77	resabs1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
79	3	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑀 ∈ ℕ )
80	4	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
81	5	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 : ℝ ⟶ ℂ )
82	6	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
83	7	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
84		eqid	⊢ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
85		eqid	⊢ ( 𝐹 ↾ ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( 𝐹 ↾ ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
86		eqid	⊢ ( 𝑦 ∈ ( ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ ( 𝑦 − ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ) = ( 𝑦 ∈ ( ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ ( 𝑦 − ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) )
87	1 2 79 80 81 82 83 68 70 12 14 13 15 16 17 75 84 85 86 18	fourierdlem90	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
88	78 87	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
89	8	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
90		eqid	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 ) = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 )
91	1 2 79 80 81 82 83 89 68 70 12 14 13 15 16 17 75 84 18 90	fourierdlem89	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 ) ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( 𝐹 ‘ ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
92	78	eqcomd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
93	92	oveq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) = ( ( ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
94	91 93	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 ) ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( 𝐹 ‘ ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ) ∈ ( ( ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
95	9	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
96		eqid	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 ) = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 )
97	1 2 79 80 81 82 83 95 68 70 12 14 13 15 16 17 75 84 18 96	fourierdlem91	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 ) ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( 𝐹 ‘ ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
98	92	oveq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( ( ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
99	97 98	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 ) ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( 𝐹 ‘ ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∈ ( ( ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
100	32 64 65 66 88 94 99	fourierdlem69	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐶 [,] 𝐷 ) ) ∈ 𝐿1 )
101	22 100	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )