Theorem fourierdlem110

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any 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	fourierdlem110.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	fourierdlem110.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	fourierdlem110.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
	fourierdlem110.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem110.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem110.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	fourierdlem110.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
	fourierdlem110.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
	fourierdlem110.fper	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
	fourierdlem110.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
	fourierdlem110.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
	fourierdlem110.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
Assertion	fourierdlem110	⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem110.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		fourierdlem110.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		fourierdlem110.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
4		fourierdlem110.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
5		fourierdlem110.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
6		fourierdlem110.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7		fourierdlem110.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
8		fourierdlem110.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
9		fourierdlem110.fper	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
10		fourierdlem110.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
11		fourierdlem110.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
12		fourierdlem110.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	a1i	⊢ ( 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) → ( ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
24	23	rabbiia	⊢ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
25	24	uneq2i	⊢ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
26	25	fveq2i	⊢ ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) = ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
27	26	oveq1i	⊢ ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
28		isoeq5	⊢ ( ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
29	25 28	ax-mp	⊢ ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
30		isoeq1	⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
31	29 30	syl5bb	⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
32	31	cbviotavw	⊢ ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
33		id	⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
34		oveq2	⊢ ( 𝑦 = 𝑥 → ( 𝐵 − 𝑦 ) = ( 𝐵 − 𝑥 ) )
35	34	oveq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐵 − 𝑦 ) / 𝑇 ) = ( ( 𝐵 − 𝑥 ) / 𝑇 ) )
36	35	fveq2d	⊢ ( 𝑦 = 𝑥 → ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) )
37	36	oveq1d	⊢ ( 𝑦 = 𝑥 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
38	33 37	oveq12d	⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
39	38	cbvmptv	⊢ ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
40		eqeq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 = 𝐵 ↔ 𝑤 = 𝐵 ) )
41		id	⊢ ( 𝑦 = 𝑤 → 𝑦 = 𝑤 )
42	40 41	ifbieq2d	⊢ ( 𝑦 = 𝑤 → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) )
43	42	cbvmptv	⊢ ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) = ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) )
44		fveq2	⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) = ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) )
45	44	fveq2d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) ‘ ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) = ( ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) ‘ ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) )
46	45	breq2d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) ‘ ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) ↔ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) ‘ ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ) )
47	46	rabbidv	⊢ ( 𝑧 = 𝑥 → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) ‘ ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) } = { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) ‘ ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } )
48	47	supeq1d	⊢ ( 𝑧 = 𝑥 → sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) ‘ ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) } , ℝ , < ) = sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) ‘ ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
49	48	cbvmptv	⊢ ( 𝑧 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) ‘ ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) } , ℝ , < ) ) = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) ‘ ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
50	1 2 3 4 5 6 7 8 9 10 11 12 13 18 27 32 39 43 49	fourierdlem109	⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )