Metamath Proof Explorer

Theorem fourierdlem113

Description: Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem113.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem113.t ⊢ 𝑇 = ( 2 · π )
fourierdlem113.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
fourierdlem113.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem113.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
fourierdlem113.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
fourierdlem113.p ⊢ 𝑃 = ( 𝑛 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑛 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑛 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑛 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem113.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem113.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem113.dvcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem113.dvlb ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ≠ ∅ )
fourierdlem113.dvub ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ≠ ∅ )
fourierdlem113.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
fourierdlem113.b ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
fourierdlem113.15 ⊢ 𝑆 = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) )
fourierdlem113.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem113.exq ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ran 𝑄 )
Assertion fourierdlem113 ( 𝜑 → ( seq 1 ( + , 𝑆 ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) ) ∧ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝐿 + 𝑅 ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem113.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem113.t ⊢ 𝑇 = ( 2 · π )
3 fourierdlem113.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
4 fourierdlem113.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
5 fourierdlem113.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
6 fourierdlem113.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
7 fourierdlem113.p ⊢ 𝑃 = ( 𝑛 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑛 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑛 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑛 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
8 fourierdlem113.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
9 fourierdlem113.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
10 fourierdlem113.dvcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
11 fourierdlem113.dvlb ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ≠ ∅ )
12 fourierdlem113.dvub ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ≠ ∅ )
13 fourierdlem113.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
14 fourierdlem113.b ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
15 fourierdlem113.15 ⊢ 𝑆 = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) )
16 fourierdlem113.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
17 fourierdlem113.exq ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ran 𝑄 )
18 oveq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 mod ( 2 · π ) ) = ( 𝑦 mod ( 2 · π ) ) )
19 18 eqeq1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 mod ( 2 · π ) ) = 0 ↔ ( 𝑦 mod ( 2 · π ) ) = 0 ) )
20 oveq2 ⊢ ( 𝑤 = 𝑦 → ( ( 𝑘 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑘 + ( 1 / 2 ) ) · 𝑦 ) )
21 20 fveq2d ⊢ ( 𝑤 = 𝑦 → ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑤 ) ) = ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑦 ) ) )
22 fvoveq1 ⊢ ( 𝑤 = 𝑦 → ( sin ‘ ( 𝑤 / 2 ) ) = ( sin ‘ ( 𝑦 / 2 ) ) )
23 22 oveq2d ⊢ ( 𝑤 = 𝑦 → ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
24 21 23 oveq12d ⊢ ( 𝑤 = 𝑦 → ( ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) )
25 19 24 ifbieq2d ⊢ ( 𝑤 = 𝑦 → if ( ( 𝑤 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ) = if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) )
26 25 cbvmptv ⊢ ( 𝑤 ∈ ℝ ↦ if ( ( 𝑤 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ) ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) )
27 oveq2 ⊢ ( 𝑘 = 𝑚 → ( 2 · 𝑘 ) = ( 2 · 𝑚 ) )
28 27 oveq1d ⊢ ( 𝑘 = 𝑚 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑚 ) + 1 ) )
29 28 oveq1d ⊢ ( 𝑘 = 𝑚 → ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · π ) ) = ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) )
30 oveq1 ⊢ ( 𝑘 = 𝑚 → ( 𝑘 + ( 1 / 2 ) ) = ( 𝑚 + ( 1 / 2 ) ) )
31 30 fvoveq1d ⊢ ( 𝑘 = 𝑚 → ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑦 ) ) = ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑦 ) ) )
32 31 oveq1d ⊢ ( 𝑘 = 𝑚 → ( ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) )
33 29 32 ifeq12d ⊢ ( 𝑘 = 𝑚 → if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) )
34 33 mpteq2dv ⊢ ( 𝑘 = 𝑚 → ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
35 26 34 eqtrid ⊢ ( 𝑘 = 𝑚 → ( 𝑤 ∈ ℝ ↦ if ( ( 𝑤 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ) ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
36 35 cbvmptv ⊢ ( 𝑘 ∈ ℕ ↦ ( 𝑤 ∈ ℝ ↦ if ( ( 𝑤 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑘 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
37 oveq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 + ( 𝑗 · 𝑇 ) ) = ( 𝑦 + ( 𝑗 · 𝑇 ) ) )
38 37 eleq1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ) )
39 38 rexbidv ⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ) )
40 39 cbvrabv ⊢ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 }
41 40 uneq2i ⊢ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } )
42 41 fveq2i ⊢ ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) = ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) )
43 42 oveq1i ⊢ ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
44 oveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 · 𝑇 ) = ( 𝑗 · 𝑇 ) )
45 44 oveq2d ⊢ ( 𝑘 = 𝑗 → ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑦 + ( 𝑗 · 𝑇 ) ) )
46 45 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ) )
47 46 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 )
48 47 rabbii ⊢ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 }
49 48 uneq2i ⊢ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } )
50 isoeq5 ⊢ ( ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
51 49 50 ax-mp ⊢ ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
52 51 a1i ⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
53 44 oveq2d ⊢ ( 𝑘 = 𝑗 → ( 𝑤 + ( 𝑘 · 𝑇 ) ) = ( 𝑤 + ( 𝑗 · 𝑇 ) ) )
54 53 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ) )
55 54 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 )
56 55 rabbii ⊢ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 }
57 56 uneq2i ⊢ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } )
58 57 fveq2i ⊢ ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) = ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) )
59 58 oveq1i ⊢ ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
60 59 oveq2i ⊢ ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) = ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) )
61 isoeq4 ⊢ ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) = ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
62 60 61 ax-mp ⊢ ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
63 62 a1i ⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
64 isoeq1 ⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
65 52 63 64 3bitrd ⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
66 65 cbviotavw ⊢ ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
67 pire ⊢ π ∈ ℝ
68 67 renegcli ⊢ - π ∈ ℝ
69 68 a1i ⊢ ( 𝜑 → - π ∈ ℝ )
70 67 a1i ⊢ ( 𝜑 → π ∈ ℝ )
71 negpilt0 ⊢ - π < 0
72 71 a1i ⊢ ( 𝜑 → - π < 0 )
73 pipos ⊢ 0 < π
74 73 a1i ⊢ ( 𝜑 → 0 < π )
75 picn ⊢ π ∈ ℂ
76 75 2timesi ⊢ ( 2 · π ) = ( π + π )
77 75 75 subnegi ⊢ ( π − - π ) = ( π + π )
78 76 2 77 3eqtr4i ⊢ 𝑇 = ( π − - π )
79 7 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
80 8 79 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
81 9 80 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
82 81 simpld ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
83 elmapi ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
84 82 83 syl ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
85 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
86 rnffi ⊢ ( ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ∧ ( 0 ... 𝑀 ) ∈ Fin ) → ran 𝑄 ∈ Fin )
87 84 85 86 syl2anc ⊢ ( 𝜑 → ran 𝑄 ∈ Fin )
88 7 8 9 fourierdlem15 ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
89 88 frnd ⊢ ( 𝜑 → ran 𝑄 ⊆ ( - π [,] π ) )
90 81 simprd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
91 90 simplrd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = π )
92 88 ffund ⊢ ( 𝜑 → Fun 𝑄 )
93 8 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
94 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
95 93 94 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
96 eluzfz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
97 95 96 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
98 88 fdmd ⊢ ( 𝜑 → dom 𝑄 = ( 0 ... 𝑀 ) )
99 98 eqcomd ⊢ ( 𝜑 → ( 0 ... 𝑀 ) = dom 𝑄 )
100 97 99 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ dom 𝑄 )
101 fvelrn ⊢ ( ( Fun 𝑄 ∧ 𝑀 ∈ dom 𝑄 ) → ( 𝑄 ‘ 𝑀 ) ∈ ran 𝑄 )
102 92 100 101 syl2anc ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ran 𝑄 )
103 91 102 eqeltrrd ⊢ ( 𝜑 → π ∈ ran 𝑄 )
104 eqid ⊢ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
105 isoeq1 ⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
106 41 57 49 3eqtr4ri ⊢ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
107 isoeq5 ⊢ ( ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) → ( 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
108 106 107 ax-mp ⊢ ( 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
109 105 108 bitrdi ⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
110 109 cbviotavw ⊢ ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
111 eqid ⊢ { 𝑤 ∈ ( ( - π + 𝑋 ) (,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑤 ∈ ( ( - π + 𝑋 ) (,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
112 69 70 72 74 78 87 89 103 16 4 17 104 110 111 fourierdlem51 ⊢ ( 𝜑 → 𝑋 ∈ ran ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑤 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( - π + 𝑋 ) , ( π + 𝑋 ) } ∪ { 𝑦 ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
113 ax-resscn ⊢ ℝ ⊆ ℂ
114 113 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ℝ ⊆ ℂ )
115 ioossre ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
116 115 a1i ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
117 1 116 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
118 113 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
119 117 118 fssd ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
120 119 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
121 115 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
122 1 118 fssd ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
123 122 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : ℝ ⟶ ℂ )
124 ssidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ℝ ⊆ ℝ )
125 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
126 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
127 125 126 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
128 114 123 124 121 127 syl22anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
129 128 dmeqd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = dom ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
130 ioontr ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
131 130 reseq2i ⊢ ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
132 131 dmeqi ⊢ dom ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
133 132 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
134 cncff ⊢ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
135 fdm ⊢ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ → dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
136 10 134 135 3syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
137 129 133 136 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
138 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ ∧ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ ) ∧ dom ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
139 114 120 121 137 138 syl31anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
140 121 114 sstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
141 84 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
142 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
143 142 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
144 141 143 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
145 144 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
146 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
147 146 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
148 141 147 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
149 81 simprrd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
150 149 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
151 125 145 148 150 lptioo1cn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
152 117 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
153 ssidd ⊢ ( 𝜑 → ℝ ⊆ ℝ )
154 118 122 153 dvbss ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) ⊆ ℝ )
155 dvfre ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
156 1 153 155 syl2anc ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
157 0re ⊢ 0 ∈ ℝ
158 68 157 67 lttri ⊢ ( ( - π < 0 ∧ 0 < π ) → - π < π )
159 71 73 158 mp2an ⊢ - π < π
160 159 a1i ⊢ ( 𝜑 → - π < π )
161 90 simplld ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = - π )
162 10 134 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
163 162 140 151 11 125 ellimciota ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℩ 𝑥 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
164 148 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
165 125 164 144 150 lptioo2cn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
166 162 140 165 12 125 ellimciota ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℩ 𝑥 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
167 122 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝐹 : ℝ ⟶ ℂ )
168 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
169 168 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℝ )
170 2pire ⊢ ( 2 · π ) ∈ ℝ
171 170 a1i ⊢ ( 𝜑 → ( 2 · π ) ∈ ℝ )
172 2 171 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
173 172 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑇 ∈ ℝ )
174 169 173 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
175 167 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℂ )
176 173 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑇 ∈ ℝ )
177 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑘 ∈ ℤ )
178 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
179 3 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
180 175 176 177 178 179 fperiodmul ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑡 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑡 ) )
181 eqid ⊢ ( ℝ D 𝐹 ) = ( ℝ D 𝐹 )
182 167 174 180 181 fperdvper ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ dom ( ℝ D 𝐹 ) ) → ( ( 𝑡 + ( 𝑘 · 𝑇 ) ) ∈ dom ( ℝ D 𝐹 ) ∧ ( ( ℝ D 𝐹 ) ‘ ( 𝑡 + ( 𝑘 · 𝑇 ) ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
183 182 an32s ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom ( ℝ D 𝐹 ) ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑡 + ( 𝑘 · 𝑇 ) ) ∈ dom ( ℝ D 𝐹 ) ∧ ( ( ℝ D 𝐹 ) ‘ ( 𝑡 + ( 𝑘 · 𝑇 ) ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
184 183 simpld ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom ( ℝ D 𝐹 ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝑡 + ( 𝑘 · 𝑇 ) ) ∈ dom ( ℝ D 𝐹 ) )
185 183 simprd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom ( ℝ D 𝐹 ) ) ∧ 𝑘 ∈ ℤ ) → ( ( ℝ D 𝐹 ) ‘ ( 𝑡 + ( 𝑘 · 𝑇 ) ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
186 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) )
187 fvoveq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑄 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
188 186 187 oveq12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑄 ‘ 𝑗 ) (,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
189 188 cbvmptv ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑗 ) (,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
190 eqid ⊢ ( 𝑡 ∈ ℝ ↦ ( 𝑡 + ( ( ⌊ ‘ ( ( π − 𝑡 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( 𝑡 + ( ( ⌊ ‘ ( ( π − 𝑡 ) / 𝑇 ) ) · 𝑇 ) ) )
191 154 156 69 70 160 78 8 84 161 91 10 163 166 184 185 189 190 fourierdlem71 ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
192 191 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
193 nfv ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) )
194 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧
195 193 194 nfan ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
196 128 131 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
197 196 fveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) = ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) )
198 fvres ⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
199 197 198 sylan9eq ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
200 199 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
201 200 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
202 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
203 ssdmres ⊢ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom ( ℝ D 𝐹 ) ↔ dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
204 136 203 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom ( ℝ D 𝐹 ) )
205 204 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom ( ℝ D 𝐹 ) )
206 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
207 205 206 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ dom ( ℝ D 𝐹 ) )
208 rspa ⊢ ( ( ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ∧ 𝑡 ∈ dom ( ℝ D 𝐹 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
209 202 207 208 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
210 201 209 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
211 195 210 ralrimia ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) → ∀ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
212 211 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 → ∀ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) )
213 212 reximdv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 → ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) )
214 192 213 mpd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
215 148 144 152 137 214 ioodvbdlimc1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ≠ ∅ )
216 120 140 151 215 125 ellimciota ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℩ 𝑦 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
217 148 144 152 137 214 ioodvbdlimc2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ≠ ∅ )
218 120 140 165 217 125 ellimciota ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℩ 𝑦 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
219 resindm ⊢ ( ( ℝ D 𝐹 ) ↾ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( -∞ (,) 𝑋 ) )
220 219 a1i ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( -∞ (,) 𝑋 ) ) )
221 inss2 ⊢ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ dom ( ℝ D 𝐹 )
222 221 a1i ⊢ ( 𝜑 → ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ dom ( ℝ D 𝐹 ) )
223 156 222 fssresd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ) : ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ⟶ ℝ )
224 220 223 feq1dd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( -∞ (,) 𝑋 ) ) : ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ⟶ ℝ )
225 224 118 fssd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( -∞ (,) 𝑋 ) ) : ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ⟶ ℂ )
226 ioosscn ⊢ ( -∞ (,) 𝑋 ) ⊆ ℂ
227 ssinss1 ⊢ ( ( -∞ (,) 𝑋 ) ⊆ ℂ → ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ ℂ )
228 226 227 ax-mp ⊢ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ ℂ
229 228 a1i ⊢ ( 𝜑 → ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ ℂ )
230 3simpb ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝜑 ∧ 𝑘 ∈ ℤ ) )
231 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ∧ 𝑘 ∈ ℤ ) → 𝑥 ∈ dom ( ℝ D 𝐹 ) )
232 167 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℂ )
233 173 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ )
234 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) → 𝑘 ∈ ℤ )
235 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
236 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ℝ ↔ 𝑦 ∈ ℝ ) )
237 236 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ↔ ( 𝜑 ∧ 𝑦 ∈ ℝ ) ) )
238 fvoveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) )
239 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
240 238 239 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) ) )
241 237 240 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) ) ) )
242 241 3 chvarvv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) )
243 242 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) )
244 232 233 234 235 243 fperiodmul ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
245 167 174 244 181 fperdvper ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ dom ( ℝ D 𝐹 ) ∧ ( ( ℝ D 𝐹 ) ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
246 230 231 245 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ dom ( ℝ D 𝐹 ) ∧ ( ( ℝ D 𝐹 ) ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
247 246 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ dom ( ℝ D 𝐹 ) )
248 oveq2 ⊢ ( 𝑤 = 𝑥 → ( π − 𝑤 ) = ( π − 𝑥 ) )
249 248 fvoveq1d ⊢ ( 𝑤 = 𝑥 → ( ⌊ ‘ ( ( π − 𝑤 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) )
250 249 oveq1d ⊢ ( 𝑤 = 𝑥 → ( ( ⌊ ‘ ( ( π − 𝑤 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
251 250 cbvmptv ⊢ ( 𝑤 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
252 eqid ⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( 𝑤 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( 𝑤 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑥 ) ) )
253 69 70 160 78 247 4 251 252 7 8 9 204 fourierdlem41 ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ( 𝑦 < 𝑋 ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) ∧ ∃ 𝑦 ∈ ℝ ( 𝑋 < 𝑦 ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) ) )
254 253 simpld ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ( 𝑦 < 𝑋 ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) )
255 125 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
256 mnfxr ⊢ -∞ ∈ ℝ*
257 rexr ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
258 257 mnfled ⊢ ( 𝑦 ∈ ℝ → -∞ ≤ 𝑦 )
259 iooss1 ⊢ ( ( -∞ ∈ ℝ* ∧ -∞ ≤ 𝑦 ) → ( 𝑦 (,) 𝑋 ) ⊆ ( -∞ (,) 𝑋 ) )
260 256 258 259 sylancr ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 (,) 𝑋 ) ⊆ ( -∞ (,) 𝑋 ) )
261 260 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) → ( 𝑦 (,) 𝑋 ) ⊆ ( -∞ (,) 𝑋 ) )
262 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) → ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) )
263 261 262 ssind ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) → ( 𝑦 (,) 𝑋 ) ⊆ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) )
264 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
265 264 lpss3 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ ℂ ∧ ( 𝑦 (,) 𝑋 ) ⊆ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ) → ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑦 (,) 𝑋 ) ) ⊆ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ) )
266 255 228 263 265 mp3an12i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) → ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑦 (,) 𝑋 ) ) ⊆ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ) )
267 266 3adant3l ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑦 < 𝑋 ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑦 (,) 𝑋 ) ) ⊆ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ) )
268 257 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑦 < 𝑋 ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → 𝑦 ∈ ℝ* )
269 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑦 < 𝑋 ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → 𝑋 ∈ ℝ )
270 simp3l ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑦 < 𝑋 ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → 𝑦 < 𝑋 )
271 125 268 269 270 lptioo2cn ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑦 < 𝑋 ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑦 (,) 𝑋 ) ) )
272 267 271 sseldd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑦 < 𝑋 ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ) )
273 272 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ( 𝑦 < 𝑋 ∧ ( 𝑦 (,) 𝑋 ) ⊆ dom ( ℝ D 𝐹 ) ) → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ) ) )
274 254 273 mpd ⊢ ( 𝜑 → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( -∞ (,) 𝑋 ) ∩ dom ( ℝ D 𝐹 ) ) ) )
275 246 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( ( ℝ D 𝐹 ) ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
276 oveq2 ⊢ ( 𝑦 = 𝑥 → ( π − 𝑦 ) = ( π − 𝑥 ) )
277 276 fvoveq1d ⊢ ( 𝑦 = 𝑥 → ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) )
278 277 oveq1d ⊢ ( 𝑦 = 𝑥 → ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
279 278 cbvmptv ⊢ ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
280 id ⊢ ( 𝑧 = 𝑥 → 𝑧 = 𝑥 )
281 fveq2 ⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑧 ) = ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑥 ) )
282 280 281 oveq12d ⊢ ( 𝑧 = 𝑥 → ( 𝑧 + ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑧 ) ) = ( 𝑥 + ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑥 ) ) )
283 282 cbvmptv ⊢ ( 𝑧 ∈ ℝ ↦ ( 𝑧 + ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑧 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑥 ) ) )
284 69 70 160 7 78 8 9 154 156 247 275 10 166 4 279 283 fourierdlem49 ⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ≠ ∅ )
285 225 229 274 284 125 ellimciota ⊢ ( 𝜑 → ( ℩ 𝑥 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∈ ( ( ( ℝ D 𝐹 ) ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
286 resindm ⊢ ( ( ℝ D 𝐹 ) ↾ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝑋 (,) +∞ ) )
287 286 a1i ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝑋 (,) +∞ ) ) )
288 inss2 ⊢ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ dom ( ℝ D 𝐹 )
289 288 a1i ⊢ ( 𝜑 → ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ dom ( ℝ D 𝐹 ) )
290 156 289 fssresd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ) : ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ⟶ ℝ )
291 287 290 feq1dd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝑋 (,) +∞ ) ) : ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ⟶ ℝ )
292 291 118 fssd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝑋 (,) +∞ ) ) : ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ⟶ ℂ )
293 ioosscn ⊢ ( 𝑋 (,) +∞ ) ⊆ ℂ
294 ssinss1 ⊢ ( ( 𝑋 (,) +∞ ) ⊆ ℂ → ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ ℂ )
295 293 294 ax-mp ⊢ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ ℂ
296 295 a1i ⊢ ( 𝜑 → ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ ℂ )
297 253 simprd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ( 𝑋 < 𝑦 ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) )
298 pnfxr ⊢ +∞ ∈ ℝ*
299 257 pnfged ⊢ ( 𝑦 ∈ ℝ → 𝑦 ≤ +∞ )
300 iooss2 ⊢ ( ( +∞ ∈ ℝ* ∧ 𝑦 ≤ +∞ ) → ( 𝑋 (,) 𝑦 ) ⊆ ( 𝑋 (,) +∞ ) )
301 298 299 300 sylancr ⊢ ( 𝑦 ∈ ℝ → ( 𝑋 (,) 𝑦 ) ⊆ ( 𝑋 (,) +∞ ) )
302 301 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) → ( 𝑋 (,) 𝑦 ) ⊆ ( 𝑋 (,) +∞ ) )
303 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) → ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) )
304 302 303 ssind ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) → ( 𝑋 (,) 𝑦 ) ⊆ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) )
305 264 lpss3 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ⊆ ℂ ∧ ( 𝑋 (,) 𝑦 ) ⊆ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ) → ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑋 (,) 𝑦 ) ) ⊆ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ) )
306 255 295 304 305 mp3an12i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) → ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑋 (,) 𝑦 ) ) ⊆ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ) )
307 306 3adant3l ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑋 < 𝑦 ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑋 (,) 𝑦 ) ) ⊆ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ) )
308 257 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑋 < 𝑦 ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → 𝑦 ∈ ℝ* )
309 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑋 < 𝑦 ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → 𝑋 ∈ ℝ )
310 simp3l ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑋 < 𝑦 ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → 𝑋 < 𝑦 )
311 125 308 309 310 lptioo1cn ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑋 < 𝑦 ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑋 (,) 𝑦 ) ) )
312 307 311 sseldd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ( 𝑋 < 𝑦 ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) ) → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ) )
313 312 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ( 𝑋 < 𝑦 ∧ ( 𝑋 (,) 𝑦 ) ⊆ dom ( ℝ D 𝐹 ) ) → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ) ) )
314 297 313 mpd ⊢ ( 𝜑 → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝑋 (,) +∞ ) ∩ dom ( ℝ D 𝐹 ) ) ) )
315 biid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑄 ‘ 𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑄 ‘ 𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
316 69 70 160 7 78 8 9 156 247 275 10 163 4 279 283 315 fourierdlem48 ⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ≠ ∅ )
317 292 296 314 316 125 ellimciota ⊢ ( 𝜑 → ( ℩ 𝑥 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) ∈ ( ( ( ℝ D 𝐹 ) ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
318 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) )
319 fvoveq1 ⊢ ( 𝑛 = 𝑘 → ( cos ‘ ( 𝑛 · 𝑋 ) ) = ( cos ‘ ( 𝑘 · 𝑋 ) ) )
320 318 319 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) )
321 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐵 ‘ 𝑛 ) = ( 𝐵 ‘ 𝑘 ) )
322 fvoveq1 ⊢ ( 𝑛 = 𝑘 → ( sin ‘ ( 𝑛 · 𝑋 ) ) = ( sin ‘ ( 𝑘 · 𝑋 ) ) )
323 321 322 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) = ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) )
324 320 323 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) )
325 324 cbvsumv ⊢ Σ 𝑛 ∈ ( 1 ... 𝑚 ) ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑚 ) ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) )
326 oveq2 ⊢ ( 𝑗 = 𝑚 → ( 1 ... 𝑗 ) = ( 1 ... 𝑚 ) )
327 326 eqcomd ⊢ ( 𝑗 = 𝑚 → ( 1 ... 𝑚 ) = ( 1 ... 𝑗 ) )
328 327 sumeq1d ⊢ ( 𝑗 = 𝑚 → Σ 𝑘 ∈ ( 1 ... 𝑚 ) ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑗 ) ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) )
329 325 328 eqtr2id ⊢ ( 𝑗 = 𝑚 → Σ 𝑘 ∈ ( 1 ... 𝑗 ) ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... 𝑚 ) ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) )
330 329 oveq2d ⊢ ( 𝑗 = 𝑚 → ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑗 ) ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) ) = ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑚 ) ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) )
331 330 cbvmptv ⊢ ( 𝑗 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑗 ) ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑚 ) ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) )
332 1 fdmd ⊢ ( 𝜑 → dom 𝐹 = ℝ )
333 332 eqimssd ⊢ ( 𝜑 → dom 𝐹 ⊆ ℝ )
334 1 ffdmd ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
335 333 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ dom 𝐹 ) → 𝑡 ∈ ℝ )
336 335 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → 𝑡 ∈ ℝ )
337 168 adantl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℝ )
338 173 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → 𝑇 ∈ ℝ )
339 337 338 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
340 336 339 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑡 + ( 𝑘 · 𝑇 ) ) ∈ ℝ )
341 332 eqcomd ⊢ ( 𝜑 → ℝ = dom 𝐹 )
342 341 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ℝ = dom 𝐹 )
343 340 342 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑡 + ( 𝑘 · 𝑇 ) ) ∈ dom 𝐹 )
344 id ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝜑 ∧ 𝑘 ∈ ℤ ) )
345 344 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝜑 ∧ 𝑘 ∈ ℤ ) )
346 345 336 180 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑡 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑡 ) )
347 333 334 69 70 160 78 8 84 161 91 139 216 218 343 346 189 190 fourierdlem71 ⊢ ( 𝜑 → ∃ 𝑢 ∈ ℝ ∀ 𝑡 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑢 )
348 332 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑡 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑢 ↔ ∀ 𝑡 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑢 ) )
349 348 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ℝ ∀ 𝑡 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑢 ↔ ∃ 𝑢 ∈ ℝ ∀ 𝑡 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑢 ) )
350 347 349 mpbid ⊢ ( 𝜑 → ∃ 𝑢 ∈ ℝ ∀ 𝑡 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑢 )
351 1 36 7 8 9 43 66 4 112 2 3 139 216 218 10 285 317 5 6 13 14 331 15 350 191 4 fourierdlem112 ⊢ ( 𝜑 → ( seq 1 ( + , 𝑆 ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) ) ∧ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝐿 + 𝑅 ) / 2 ) ) )