Metamath Proof Explorer

Theorem fourierdlem108

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any positive value X . This lemma generalizes fourierdlem92 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem108.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem108.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem108.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem108.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
fourierdlem108.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem108.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem108.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem108.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
fourierdlem108.fper ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
fourierdlem108.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem108.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
fourierdlem108.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
Assertion fourierdlem108 ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 fourierdlem108.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem108.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem108.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
4 fourierdlem108.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
5 fourierdlem108.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
6 fourierdlem108.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7 fourierdlem108.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
8 fourierdlem108.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
9 fourierdlem108.fper ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
10 fourierdlem108.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
11 fourierdlem108.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
12 fourierdlem108.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
13 eqid ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = 𝐴 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = 𝐴 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
14 oveq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 + ( 𝑘 · 𝑇 ) ) = ( 𝑦 + ( 𝑘 · 𝑇 ) ) )
15 14 eleq1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
16 15 rexbidv ⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
17 16 cbvrabv ⊢ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
18 17 uneq2i ⊢ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
19 oveq1 ⊢ ( 𝑙 = 𝑘 → ( 𝑙 · 𝑇 ) = ( 𝑘 · 𝑇 ) )
20 19 oveq2d ⊢ ( 𝑙 = 𝑘 → ( 𝑤 + ( 𝑙 · 𝑇 ) ) = ( 𝑤 + ( 𝑘 · 𝑇 ) ) )
21 20 eleq1d ⊢ ( 𝑙 = 𝑘 → ( ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
22 21 cbvrexvw ⊢ ( ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 )
23 22 rgenw ⊢ ∀ 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 )
24 rabbi ⊢ ( ∀ 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) ↔ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
25 23 24 mpbi ⊢ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
26 25 uneq2i ⊢ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
27 26 fveq2i ⊢ ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) = ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
28 27 oveq1i ⊢ ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
29 isoeq5 ⊢ ( ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
30 26 29 ax-mp ⊢ ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
31 isoeq1 ⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
32 30 31 syl5bb ⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
33 32 cbviotavw ⊢ ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑤 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑤 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
34 id ⊢ ( 𝑤 = 𝑥 → 𝑤 = 𝑥 )
35 oveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐵 − 𝑤 ) = ( 𝐵 − 𝑥 ) )
36 35 oveq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝐵 − 𝑤 ) / 𝑇 ) = ( ( 𝐵 − 𝑥 ) / 𝑇 ) )
37 36 fveq2d ⊢ ( 𝑤 = 𝑥 → ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) )
38 37 oveq1d ⊢ ( 𝑤 = 𝑥 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
39 34 38 oveq12d ⊢ ( 𝑤 = 𝑥 → ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
40 39 cbvmptv ⊢ ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
41 eqeq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 = 𝐵 ↔ 𝑦 = 𝐵 ) )
42 id ⊢ ( 𝑤 = 𝑦 → 𝑤 = 𝑦 )
43 41 42 ifbieq2d ⊢ ( 𝑤 = 𝑦 → if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) = if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
44 43 cbvmptv ⊢ ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
45 fveq2 ⊢ ( 𝑧 = 𝑥 → ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) = ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) )
46 45 fveq2d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) = ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) )
47 46 breq2d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) ↔ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ) )
48 47 rabbidv ⊢ ( 𝑧 = 𝑥 → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) } = { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } )
49 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) )
50 49 breq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ↔ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ) )
51 50 cbvrabv ⊢ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) }
52 48 51 eqtrdi ⊢ ( 𝑧 = 𝑥 → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } )
53 52 supeq1d ⊢ ( 𝑧 = 𝑥 → sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) } , ℝ , < ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
54 53 cbvmptv ⊢ ( 𝑧 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) } , ℝ , < ) ) = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
55 1 2 3 4 5 6 7 8 9 10 11 12 13 18 28 33 40 44 54 fourierdlem107 ⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )