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 syl5eq ( 𝑘 = 𝑚 → ( 𝑤 ∈ ℝ ↦ 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 ) ) )