Metamath Proof Explorer


Theorem fourierdlem99

Description: limit for F at the upper bound of an interval for the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem99.f ( 𝜑𝐹 : ℝ ⟶ ℝ )
fourierdlem99.p 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem99.t 𝑇 = ( 𝐵𝐴 )
fourierdlem99.m ( 𝜑𝑀 ∈ ℕ )
fourierdlem99.q ( 𝜑𝑄 ∈ ( 𝑃𝑀 ) )
fourierdlem99.fper ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
fourierdlem99.qcn ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem99.l ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
fourierdlem99.c ( 𝜑𝐶 ∈ ℝ )
fourierdlem99.d ( 𝜑𝐷 ∈ ( 𝐶 (,) +∞ ) )
fourierdlem99.j ( 𝜑𝐽 ∈ ( 0 ..^ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) )
fourierdlem99.v 𝑉 = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ∈ ℤ ( 𝑦 + ( · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
Assertion fourierdlem99 ( 𝜑 → if ( ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) = ( 𝑄 ‘ ( ( ( 𝑦 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) } , ℝ , < ) ) ‘ ( 𝑉𝐽 ) ) + 1 ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 ) ‘ ( ( 𝑦 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) } , ℝ , < ) ) ‘ ( 𝑉𝐽 ) ) ) , ( 𝐹 ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑉𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) lim ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem99.f ( 𝜑𝐹 : ℝ ⟶ ℝ )
2 fourierdlem99.p 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
3 fourierdlem99.t 𝑇 = ( 𝐵𝐴 )
4 fourierdlem99.m ( 𝜑𝑀 ∈ ℕ )
5 fourierdlem99.q ( 𝜑𝑄 ∈ ( 𝑃𝑀 ) )
6 fourierdlem99.fper ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
7 fourierdlem99.qcn ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
8 fourierdlem99.l ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
9 fourierdlem99.c ( 𝜑𝐶 ∈ ℝ )
10 fourierdlem99.d ( 𝜑𝐷 ∈ ( 𝐶 (,) +∞ ) )
11 fourierdlem99.j ( 𝜑𝐽 ∈ ( 0 ..^ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) )
12 fourierdlem99.v 𝑉 = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ∈ ℤ ( 𝑦 + ( · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
13 ax-resscn ℝ ⊆ ℂ
14 13 a1i ( 𝜑 → ℝ ⊆ ℂ )
15 1 14 fssd ( 𝜑𝐹 : ℝ ⟶ ℂ )
16 eqid ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
17 oveq1 ( 𝑧 = 𝑦 → ( 𝑧 + ( 𝑙 · 𝑇 ) ) = ( 𝑦 + ( 𝑙 · 𝑇 ) ) )
18 17 eleq1d ( 𝑧 = 𝑦 → ( ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
19 18 rexbidv ( 𝑧 = 𝑦 → ( ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
20 19 cbvrabv { 𝑧 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 }
21 20 uneq2i ( { 𝐶 , 𝐷 } ∪ { 𝑧 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } )
22 21 eqcomi ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑧 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } )
23 oveq1 ( 𝑘 = 𝑙 → ( 𝑘 · 𝑇 ) = ( 𝑙 · 𝑇 ) )
24 23 oveq2d ( 𝑘 = 𝑙 → ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑦 + ( 𝑙 · 𝑇 ) ) )
25 24 eleq1d ( 𝑘 = 𝑙 → ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
26 25 cbvrexvw ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 )
27 26 a1i ( 𝑦 ∈ ( 𝐶 [,] 𝐷 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
28 27 rabbiia { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 }
29 28 uneq2i ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } )
30 29 fveq2i ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) )
31 30 oveq1i ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
32 oveq1 ( 𝑙 = → ( 𝑙 · 𝑇 ) = ( · 𝑇 ) )
33 32 oveq2d ( 𝑙 = → ( 𝑦 + ( 𝑙 · 𝑇 ) ) = ( 𝑦 + ( · 𝑇 ) ) )
34 33 eleq1d ( 𝑙 = → ( ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( · 𝑇 ) ) ∈ ran 𝑄 ) )
35 34 cbvrexvw ( ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ ∈ ℤ ( 𝑦 + ( · 𝑇 ) ) ∈ ran 𝑄 )
36 35 a1i ( 𝑦 ∈ ( 𝐶 [,] 𝐷 ) → ( ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ ∈ ℤ ( 𝑦 + ( · 𝑇 ) ) ∈ ran 𝑄 ) )
37 36 rabbiia { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ∈ ℤ ( 𝑦 + ( · 𝑇 ) ) ∈ ran 𝑄 }
38 37 uneq2i ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ∈ ℤ ( 𝑦 + ( · 𝑇 ) ) ∈ ran 𝑄 } )
39 isoeq5 ( ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ∈ ℤ ( 𝑦 + ( · 𝑇 ) ) ∈ ran 𝑄 } ) → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ∈ ℤ ( 𝑦 + ( · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
40 38 39 ax-mp ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ∈ ℤ ( 𝑦 + ( · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
41 40 iotabii ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ∈ ℤ ( 𝑦 + ( · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
42 isoeq1 ( 𝑓 = 𝑔 → ( 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
43 42 cbviotavw ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
44 41 43 12 3eqtr4ri 𝑉 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
45 id ( 𝑣 = 𝑥𝑣 = 𝑥 )
46 oveq2 ( 𝑣 = 𝑥 → ( 𝐵𝑣 ) = ( 𝐵𝑥 ) )
47 46 oveq1d ( 𝑣 = 𝑥 → ( ( 𝐵𝑣 ) / 𝑇 ) = ( ( 𝐵𝑥 ) / 𝑇 ) )
48 47 fveq2d ( 𝑣 = 𝑥 → ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) )
49 48 oveq1d ( 𝑣 = 𝑥 → ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) )
50 45 49 oveq12d ( 𝑣 = 𝑥 → ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
51 50 cbvmptv ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
52 eqeq1 ( 𝑢 = 𝑧 → ( 𝑢 = 𝐵𝑧 = 𝐵 ) )
53 id ( 𝑢 = 𝑧𝑢 = 𝑧 )
54 52 53 ifbieq2d ( 𝑢 = 𝑧 → if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) = if ( 𝑧 = 𝐵 , 𝐴 , 𝑧 ) )
55 54 cbvmptv ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) = ( 𝑧 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑧 = 𝐵 , 𝐴 , 𝑧 ) )
56 eqid ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) )
57 fveq2 ( 𝑗 = 𝑖 → ( 𝑄𝑗 ) = ( 𝑄𝑖 ) )
58 57 breq1d ( 𝑗 = 𝑖 → ( ( 𝑄𝑗 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) ↔ ( 𝑄𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) ) )
59 58 cbvrabv { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) }
60 fveq2 ( 𝑦 = 𝑥 → ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) = ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) )
61 60 fveq2d ( 𝑦 = 𝑥 → ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) = ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) )
62 61 breq2d ( 𝑦 = 𝑥 → ( ( 𝑄𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) ↔ ( 𝑄𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ) )
63 62 rabbidv ( 𝑦 = 𝑥 → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } )
64 59 63 syl5eq ( 𝑦 = 𝑥 → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } )
65 64 supeq1d ( 𝑦 = 𝑥 → sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) } , ℝ , < ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
66 65 cbvmptv ( 𝑦 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) } , ℝ , < ) ) = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
67 eqid ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 ) = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 )
68 2 3 4 5 15 6 7 8 9 10 16 22 31 44 51 55 11 56 66 67 fourierdlem91 ( 𝜑 → if ( ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) = ( 𝑄 ‘ ( ( ( 𝑦 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) } , ℝ , < ) ) ‘ ( 𝑉𝐽 ) ) + 1 ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 ) ‘ ( ( 𝑦 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑦 ) ) } , ℝ , < ) ) ‘ ( 𝑉𝐽 ) ) ) , ( 𝐹 ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑉𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) lim ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) )