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