Metamath Proof Explorer

Theorem fourierdlem98

Description: F is continuous on the intervals induced by the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

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