Metamath Proof Explorer

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 )