This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem107

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. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem107.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem107.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem107.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem107.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
fourierdlem107.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem107.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem107.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem107.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
fourierdlem107.fper ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
fourierdlem107.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem107.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
fourierdlem107.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
fourierdlem107.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = 𝐴 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem107.h ⊢ 𝐻 = ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
fourierdlem107.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
fourierdlem107.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
fourierdlem107.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem107.z ⊢ 𝑍 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
fourierdlem107.i ⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
Assertion fourierdlem107 ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 fourierdlem107.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem107.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem107.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
4 fourierdlem107.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
5 fourierdlem107.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
6 fourierdlem107.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7 fourierdlem107.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
8 fourierdlem107.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
9 fourierdlem107.fper ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
10 fourierdlem107.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
11 fourierdlem107.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
12 fourierdlem107.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
13 fourierdlem107.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = 𝐴 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
14 fourierdlem107.h ⊢ 𝐻 = ( { ( 𝐴 − 𝑋 ) , 𝐴 } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
15 fourierdlem107.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
16 fourierdlem107.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
17 fourierdlem107.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
18 fourierdlem107.z ⊢ 𝑍 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
19 fourierdlem107.i ⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
20 3 oveq2i ⊢ ( ( 𝐴 − 𝑋 ) + 𝑇 ) = ( ( 𝐴 − 𝑋 ) + ( 𝐵 − 𝐴 ) )
21 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
22 4 rpred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
23 22 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
24 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
25 21 23 24 21 subadd4b ⊢ ( 𝜑 → ( ( 𝐴 − 𝑋 ) + ( 𝐵 − 𝐴 ) ) = ( ( 𝐴 − 𝐴 ) + ( 𝐵 − 𝑋 ) ) )
26 20 25 eqtrid ⊢ ( 𝜑 → ( ( 𝐴 − 𝑋 ) + 𝑇 ) = ( ( 𝐴 − 𝐴 ) + ( 𝐵 − 𝑋 ) ) )
27 21 subidd ⊢ ( 𝜑 → ( 𝐴 − 𝐴 ) = 0 )
28 27 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 − 𝐴 ) + ( 𝐵 − 𝑋 ) ) = ( 0 + ( 𝐵 − 𝑋 ) ) )
29 2 22 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ )
30 29 recnd ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℂ )
31 30 addlidd ⊢ ( 𝜑 → ( 0 + ( 𝐵 − 𝑋 ) ) = ( 𝐵 − 𝑋 ) )
32 26 28 31 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 − 𝑋 ) + 𝑇 ) = ( 𝐵 − 𝑋 ) )
33 3 oveq2i ⊢ ( 𝐴 + 𝑇 ) = ( 𝐴 + ( 𝐵 − 𝐴 ) )
34 21 24 pncan3d ⊢ ( 𝜑 → ( 𝐴 + ( 𝐵 − 𝐴 ) ) = 𝐵 )
35 33 34 eqtrid ⊢ ( 𝜑 → ( 𝐴 + 𝑇 ) = 𝐵 )
36 32 35 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑋 ) + 𝑇 ) [,] ( 𝐴 + 𝑇 ) ) = ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) )
37 36 eqcomd ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) = ( ( ( 𝐴 − 𝑋 ) + 𝑇 ) [,] ( 𝐴 + 𝑇 ) ) )
38 37 itgeq1d ⊢ ( 𝜑 → ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( ( 𝐴 − 𝑋 ) + 𝑇 ) [,] ( 𝐴 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
39 1 22 resubcld ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ∈ ℝ )
40 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑝 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑗 ) )
41 oveq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 + 1 ) = ( 𝑗 + 1 ) )
42 41 fveq2d ⊢ ( 𝑖 = 𝑗 → ( 𝑝 ‘ ( 𝑖 + 1 ) ) = ( 𝑝 ‘ ( 𝑗 + 1 ) ) )
43 40 42 breq12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) )
44 43 cbvralvw ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) )
45 44 a1i ⊢ ( 𝑚 ∈ ℕ → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) )
46 45 anbi2d ⊢ ( 𝑚 ∈ ℕ → ( ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = 𝐴 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = 𝐴 ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) ) )
47 46 rabbidv ⊢ ( 𝑚 ∈ ℕ → { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = 𝐴 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } = { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = 𝐴 ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) } )
48 47 mpteq2ia ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = 𝐴 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = 𝐴 ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) } )
49 13 48 eqtri ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = 𝐴 ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) } )
50 1 4 ltsubrpd ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) < 𝐴 )
51 3 5 6 7 39 1 50 13 14 15 16 fourierdlem54 ⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) )
52 51 simpld ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) )
53 52 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
54 2 1 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
55 3 54 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
56 52 simprd ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
57 39 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ) → ( 𝐴 − 𝑋 ) ∈ ℝ )
58 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ) → 𝐴 ∈ ℝ )
59 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ) → 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) )
60 eliccre ⊢ ( ( ( 𝐴 − 𝑋 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ) → 𝑥 ∈ ℝ )
61 57 58 59 60 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ) → 𝑥 ∈ ℝ )
62 61 9 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
63 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑆 ‘ 𝑖 ) = ( 𝑆 ‘ 𝑗 ) )
64 63 oveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑆 ‘ 𝑖 ) + 𝑇 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
65 64 cbvmptv ⊢ ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑖 ) + 𝑇 ) ) = ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
66 eqid ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( ( 𝐴 − 𝑋 ) + 𝑇 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐴 + 𝑇 ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( ( 𝐴 − 𝑋 ) + 𝑇 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐴 + 𝑇 ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) } )
67 6 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑀 ∈ ℕ )
68 7 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
69 8 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 : ℝ ⟶ ℂ )
70 9 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
71 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
72 39 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 − 𝑋 ) ∈ ℝ )
73 72 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 − 𝑋 ) ∈ ℝ* )
74 pnfxr ⊢ +∞ ∈ ℝ*
75 74 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → +∞ ∈ ℝ* )
76 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ℝ )
77 50 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 − 𝑋 ) < 𝐴 )
78 1 ltpnfd ⊢ ( 𝜑 → 𝐴 < +∞ )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 < +∞ )
80 73 75 76 77 79 eliood ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ( ( 𝐴 − 𝑋 ) (,) +∞ ) )
81 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
82 eqid ⊢ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
83 eqid ⊢ ( 𝐹 ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( 𝐹 ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
84 eqid ⊢ ( 𝑦 ∈ ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ ( 𝑦 − ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ) = ( 𝑦 ∈ ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ ( 𝑦 − ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) )
85 5 3 67 68 69 70 71 72 80 13 14 15 16 17 18 81 82 83 84 19 fourierdlem90 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
86 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
87 eqid ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 ) = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 )
88 5 3 67 68 69 70 71 86 72 80 13 14 15 16 17 18 81 82 19 87 fourierdlem89 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 ) ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
89 12 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
90 eqid ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 ) = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 )
91 5 3 67 68 69 70 71 89 72 80 13 14 15 16 17 18 81 82 19 90 fourierdlem91 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 ) ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( 𝐹 ‘ ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
92 39 1 49 53 55 56 62 65 66 8 85 88 91 fourierdlem92 ⊢ ( 𝜑 → ∫ ( ( ( 𝐴 − 𝑋 ) + 𝑇 ) [,] ( 𝐴 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
93 38 92 eqtrd ⊢ ( 𝜑 → ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
94 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ) → 𝐹 : ℝ ⟶ ℂ )
95 29 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ) → ( 𝐵 − 𝑋 ) ∈ ℝ )
96 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
97 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ) → 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) )
98 eliccre ⊢ ( ( ( 𝐵 − 𝑋 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
99 95 96 97 98 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
100 94 99 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
101 29 rexrd ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ* )
102 74 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
103 2 4 ltsubrpd ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) < 𝐵 )
104 2 ltpnfd ⊢ ( 𝜑 → 𝐵 < +∞ )
105 101 102 2 103 104 eliood ⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝐵 − 𝑋 ) (,) +∞ ) )
106 5 3 6 7 8 9 10 11 12 29 105 fourierdlem105 ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
107 100 106 itgcl ⊢ ( 𝜑 → ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
108 93 107 eqeltrrd ⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
109 108 subidd ⊢ ( 𝜑 → ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = 0 )
110 109 eqcomd ⊢ ( 𝜑 → 0 = ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
111 110 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 0 = ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
112 39 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝐴 − 𝑋 ) ∈ ℝ )
113 1 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 𝐴 ∈ ℝ )
114 29 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝐵 − 𝑋 ) ∈ ℝ )
115 5 6 7 fourierdlem11 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
116 115 simp3d ⊢ ( 𝜑 → 𝐴 < 𝐵 )
117 1 2 116 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
118 117 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 𝐴 ≤ 𝐵 )
119 1 2 22 lesub1d ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 − 𝑋 ) ≤ ( 𝐵 − 𝑋 ) ) )
120 119 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 − 𝑋 ) ≤ ( 𝐵 − 𝑋 ) ) )
121 118 120 mpbid ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝐴 − 𝑋 ) ≤ ( 𝐵 − 𝑋 ) )
122 2 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 𝐵 ∈ ℝ )
123 22 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 𝑋 ∈ ℝ )
124 simpr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 𝑇 < 𝑋 )
125 3 124 eqbrtrrid ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝐵 − 𝐴 ) < 𝑋 )
126 122 113 123 125 ltsub23d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝐵 − 𝑋 ) < 𝐴 )
127 114 113 126 ltled ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝐵 − 𝑋 ) ≤ 𝐴 )
128 112 113 114 121 127 eliccd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝐵 − 𝑋 ) ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) )
129 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ) → 𝐹 : ℝ ⟶ ℂ )
130 129 61 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
131 130 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑇 < 𝑋 ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
132 39 rexrd ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ∈ ℝ* )
133 1 2 22 116 ltsub1dd ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) < ( 𝐵 − 𝑋 ) )
134 29 ltpnfd ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) < +∞ )
135 132 102 29 133 134 eliood ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ( ( 𝐴 − 𝑋 ) (,) +∞ ) )
136 5 3 6 7 8 9 10 11 12 39 135 fourierdlem105 ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
137 136 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
138 6 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 𝑀 ∈ ℕ )
139 7 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
140 8 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 𝐹 : ℝ ⟶ ℂ )
141 9 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑇 < 𝑋 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
142 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑇 < 𝑋 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
143 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑇 < 𝑋 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
144 12 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑇 < 𝑋 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
145 101 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝐵 − 𝑋 ) ∈ ℝ* )
146 74 a1i ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → +∞ ∈ ℝ* )
147 113 ltpnfd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 𝐴 < +∞ )
148 145 146 113 126 147 eliood ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 𝐴 ∈ ( ( 𝐵 − 𝑋 ) (,) +∞ ) )
149 5 3 138 139 140 141 142 143 144 114 148 fourierdlem105 ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
150 112 113 128 131 137 149 itgspliticc ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
151 150 oveq1d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
152 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝐹 : ℝ ⟶ ℂ )
153 39 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐴 − 𝑋 ) ∈ ℝ )
154 29 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐵 − 𝑋 ) ∈ ℝ )
155 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) )
156 eliccre ⊢ ( ( ( 𝐴 − 𝑋 ) ∈ ℝ ∧ ( 𝐵 − 𝑋 ) ∈ ℝ ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑥 ∈ ℝ )
157 153 154 155 156 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → 𝑥 ∈ ℝ )
158 152 157 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
159 158 136 itgcl ⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
161 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ) → 𝐹 : ℝ ⟶ ℂ )
162 29 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ) → ( 𝐵 − 𝑋 ) ∈ ℝ )
163 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ) → 𝐴 ∈ ℝ )
164 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ) → 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) )
165 eliccre ⊢ ( ( ( 𝐵 − 𝑋 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ) → 𝑥 ∈ ℝ )
166 162 163 164 165 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ) → 𝑥 ∈ ℝ )
167 161 166 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
168 167 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑇 < 𝑋 ) ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
169 168 149 itgcl ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
170 108 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
171 160 169 170 addsubassd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
172 111 151 171 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 0 = ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
173 172 oveq2d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − 0 ) = ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) ) )
174 160 subid1d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − 0 ) = ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
175 159 subidd ⊢ ( 𝜑 → ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = 0 )
176 175 oveq1d ⊢ ( 𝜑 → ( ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( 0 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
177 176 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( 0 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
178 169 170 subcld ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ∈ ℂ )
179 160 160 178 subsub4d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) ) )
180 df-neg ⊢ - ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( 0 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
181 169 170 negsubdi2d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → - ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
182 180 181 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 0 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
183 177 179 182 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) ) = ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
184 173 174 183 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
185 107 subidd ⊢ ( 𝜑 → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = 0 )
186 185 eqcomd ⊢ ( 𝜑 → 0 = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
187 186 oveq2d ⊢ ( 𝜑 → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + 0 ) = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
188 187 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + 0 ) = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
189 169 addridd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + 0 ) = ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
190 114 122 113 127 118 eliccd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → 𝐴 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) )
191 100 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑇 < 𝑋 ) ∧ 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
192 1 2 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
193 8 192 feqresmpt ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
194 8 192 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
195 ioossicc ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
196 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
197 196 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴 ∈ ℝ* )
198 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
199 198 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐵 ∈ ℝ* )
200 5 6 7 fourierdlem15 ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
201 200 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
202 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
203 197 199 201 202 fourierdlem8 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
204 195 203 sstrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
205 204 resabs1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
206 205 10 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
207 205 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
208 207 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
209 11 208 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
210 207 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
211 12 210 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
212 5 6 7 194 206 209 211 fourierdlem69 ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ 𝐿1 )
213 193 212 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
214 213 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
215 114 122 190 191 149 214 itgspliticc ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
216 215 oveq2d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
217 216 oveq2d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) ) )
218 107 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
219 215 218 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ∈ ℂ )
220 169 218 219 addsub12d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) ) = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) ) )
221 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐹 : ℝ ⟶ ℂ )
222 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ )
223 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
224 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
225 eliccre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
226 222 223 224 225 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
227 221 226 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
228 227 213 itgcl ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
229 228 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
230 169 169 229 subsub4d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
231 230 eqcomd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
232 231 oveq2d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) ) = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
233 169 subidd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = 0 )
234 233 oveq1d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( 0 − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
235 df-neg ⊢ - ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( 0 − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
236 234 235 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = - ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
237 236 oveq2d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + - ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
238 218 229 negsubd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + - ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
239 232 237 238 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) ) = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
240 217 220 239 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
241 188 189 240 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
242 241 oveq2d ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
243 108 107 228 subsubd ⊢ ( 𝜑 → ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
244 93 oveq2d ⊢ ( 𝜑 → ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
245 244 109 eqtrd ⊢ ( 𝜑 → ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = 0 )
246 245 oveq1d ⊢ ( 𝜑 → ( ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( 0 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
247 228 addlidd ⊢ ( 𝜑 → ( 0 + ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
248 243 246 247 3eqtrd ⊢ ( 𝜑 → ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
249 248 adantr ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
250 184 242 249 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑇 < 𝑋 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
251 39 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( 𝐴 − 𝑋 ) ∈ ℝ )
252 29 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( 𝐵 − 𝑋 ) ∈ ℝ )
253 1 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → 𝐴 ∈ ℝ )
254 39 1 50 ltled ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ≤ 𝐴 )
255 254 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( 𝐴 − 𝑋 ) ≤ 𝐴 )
256 22 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → 𝑋 ∈ ℝ )
257 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → 𝐵 ∈ ℝ )
258 id ⊢ ( 𝑋 ≤ 𝑇 → 𝑋 ≤ 𝑇 )
259 258 3 breqtrdi ⊢ ( 𝑋 ≤ 𝑇 → 𝑋 ≤ ( 𝐵 − 𝐴 ) )
260 259 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → 𝑋 ≤ ( 𝐵 − 𝐴 ) )
261 256 257 253 260 lesubd ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → 𝐴 ≤ ( 𝐵 − 𝑋 ) )
262 251 252 253 255 261 eliccd ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → 𝐴 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) )
263 158 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
264 132 102 1 50 78 eliood ⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝐴 − 𝑋 ) (,) +∞ ) )
265 5 3 6 7 8 9 10 11 12 39 264 fourierdlem105 ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
266 265 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
267 1 leidd ⊢ ( 𝜑 → 𝐴 ≤ 𝐴 )
268 4 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝑋 )
269 2 22 subge02d ⊢ ( 𝜑 → ( 0 ≤ 𝑋 ↔ ( 𝐵 − 𝑋 ) ≤ 𝐵 ) )
270 268 269 mpbid ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ≤ 𝐵 )
271 iccss ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≤ 𝐴 ∧ ( 𝐵 − 𝑋 ) ≤ 𝐵 ) ) → ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
272 1 2 267 270 271 syl22anc ⊢ ( 𝜑 → ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
273 iccmbl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 − 𝑋 ) ∈ ℝ ) → ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ∈ dom vol )
274 1 29 273 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ∈ dom vol )
275 272 274 227 213 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
276 275 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( 𝑥 ∈ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
277 251 252 262 263 266 276 itgspliticc ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
278 268 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → 0 ≤ 𝑋 )
279 269 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( 0 ≤ 𝑋 ↔ ( 𝐵 − 𝑋 ) ≤ 𝐵 ) )
280 278 279 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( 𝐵 − 𝑋 ) ≤ 𝐵 )
281 253 257 252 261 280 eliccd ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( 𝐵 − 𝑋 ) ∈ ( 𝐴 [,] 𝐵 ) )
282 227 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
283 2 leidd ⊢ ( 𝜑 → 𝐵 ≤ 𝐵 )
284 283 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → 𝐵 ≤ 𝐵 )
285 iccss ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≤ ( 𝐵 − 𝑋 ) ∧ 𝐵 ≤ 𝐵 ) ) → ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
286 253 257 261 284 285 syl22anc ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
287 iccmbl ⊢ ( ( ( 𝐵 − 𝑋 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ∈ dom vol )
288 29 2 287 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ∈ dom vol )
289 288 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ∈ dom vol )
290 213 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
291 286 289 282 290 iblss ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( 𝑥 ∈ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
292 253 257 281 282 276 291 itgspliticc ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
293 292 oveq1d ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ( ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
294 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ) → 𝐹 : ℝ ⟶ ℂ )
295 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ) → 𝐴 ∈ ℝ )
296 29 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐵 − 𝑋 ) ∈ ℝ )
297 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ) → 𝑥 ∈ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) )
298 eliccre ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 − 𝑋 ) ∈ ℝ ∧ 𝑥 ∈ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ) → 𝑥 ∈ ℝ )
299 295 296 297 298 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ) → 𝑥 ∈ ℝ )
300 294 299 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
301 300 275 itgcl ⊢ ( 𝜑 → ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
302 301 107 107 addsubassd ⊢ ( 𝜑 → ( ( ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
303 302 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( ( ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
304 185 oveq2d ⊢ ( 𝜑 → ( ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + 0 ) )
305 301 addridd ⊢ ( 𝜑 → ( ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + 0 ) = ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
306 304 305 eqtrd ⊢ ( 𝜑 → ( ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
307 306 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
308 293 303 307 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
309 308 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( 𝐴 [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
310 93 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
311 107 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
312 310 311 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
313 282 290 itgcl ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
314 312 313 311 addsub12d ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
315 313 312 311 addsubassd ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) )
316 314 315 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) ) = ( ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
317 277 309 316 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
318 310 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( ( 𝐵 − 𝑋 ) [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ( ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) )
319 313 312 pncand ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ( ( ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 + ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) − ∫ ( ( 𝐴 − 𝑋 ) [,] 𝐴 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
320 317 318 319 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑇 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
321 250 320 55 22 ltlecasei ⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )