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 addid2d ( 𝜑 → ( 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 ffvelrnd ( ( 𝜑𝑥 ∈ ( ( 𝐵𝑋 ) [,] 𝐵 ) ) → ( 𝐹𝑥 ) ∈ ℂ )
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 ffvelrnd ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑋 ) [,] 𝐴 ) ) → ( 𝐹𝑥 ) ∈ ℂ )
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 ffvelrnd ( ( 𝜑𝑥 ∈ ( ( 𝐴𝑋 ) [,] ( 𝐵𝑋 ) ) ) → ( 𝐹𝑥 ) ∈ ℂ )
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 ffvelrnd ( ( 𝜑𝑥 ∈ ( ( 𝐵𝑋 ) [,] 𝐴 ) ) → ( 𝐹𝑥 ) ∈ ℂ )
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 addid1d ( ( 𝜑𝑇 < 𝑋 ) → ( ∫ ( ( 𝐵𝑋 ) [,] 𝐴 ) ( 𝐹𝑥 ) 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 ffvelrnd ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹𝑥 ) ∈ ℂ )
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 addid2d ( 𝜑 → ( 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 ffvelrnd ( ( 𝜑𝑥 ∈ ( 𝐴 [,] ( 𝐵𝑋 ) ) ) → ( 𝐹𝑥 ) ∈ ℂ )
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 addid1d ( 𝜑 → ( ∫ ( 𝐴 [,] ( 𝐵𝑋 ) ) ( 𝐹𝑥 ) 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 𝑥 )