Metamath Proof Explorer

Theorem fourierdlem109

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 fourierdlem109.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem109.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem109.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem109.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem109.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem109.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem109.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem109.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
fourierdlem109.fper ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
fourierdlem109.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem109.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
fourierdlem109.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
fourierdlem109.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 − 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem109.h ⊢ 𝐻 = ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
fourierdlem109.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
fourierdlem109.16 ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
fourierdlem109.17 ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem109.18 ⊢ 𝐽 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
fourierdlem109.19 ⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
Assertion fourierdlem109 ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 fourierdlem109.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem109.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem109.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
4 fourierdlem109.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
5 fourierdlem109.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
6 fourierdlem109.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7 fourierdlem109.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
8 fourierdlem109.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
9 fourierdlem109.fper ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
10 fourierdlem109.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
11 fourierdlem109.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
12 fourierdlem109.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
13 fourierdlem109.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 − 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
14 fourierdlem109.h ⊢ 𝐻 = ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
15 fourierdlem109.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
16 fourierdlem109.16 ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
17 fourierdlem109.17 ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
18 fourierdlem109.18 ⊢ 𝐽 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
19 fourierdlem109.19 ⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
20 1 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑋 ) → 𝐴 ∈ ℝ )
21 2 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑋 ) → 𝐵 ∈ ℝ )
22 4 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑋 ) → 𝑋 ∈ ℝ )
23 simpr ⊢ ( ( 𝜑 ∧ 0 < 𝑋 ) → 0 < 𝑋 )
24 22 23 elrpd ⊢ ( ( 𝜑 ∧ 0 < 𝑋 ) → 𝑋 ∈ ℝ+ )
25 6 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑋 ) → 𝑀 ∈ ℕ )
26 7 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑋 ) → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
27 8 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑋 ) → 𝐹 : ℝ ⟶ ℂ )
28 9 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < 𝑋 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
29 10 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < 𝑋 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
30 11 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < 𝑋 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
31 12 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < 𝑋 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
32 20 21 3 24 5 25 26 27 28 29 30 31 fourierdlem108 ⊢ ( ( 𝜑 ∧ 0 < 𝑋 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
33 oveq2 ⊢ ( 𝑋 = 0 → ( 𝐴 − 𝑋 ) = ( 𝐴 − 0 ) )
34 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
35 34 subid1d ⊢ ( 𝜑 → ( 𝐴 − 0 ) = 𝐴 )
36 33 35 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( 𝐴 − 𝑋 ) = 𝐴 )
37 oveq2 ⊢ ( 𝑋 = 0 → ( 𝐵 − 𝑋 ) = ( 𝐵 − 0 ) )
38 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
39 38 subid1d ⊢ ( 𝜑 → ( 𝐵 − 0 ) = 𝐵 )
40 37 39 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( 𝐵 − 𝑋 ) = 𝐵 )
41 36 40 oveq12d ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) = ( 𝐴 [,] 𝐵 ) )
42 41 itgeq1d ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
43 42 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑋 ) ∧ 𝑋 = 0 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
44 simpll ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑋 ) ∧ ¬ 𝑋 = 0 ) → 𝜑 )
45 44 4 syl ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑋 ) ∧ ¬ 𝑋 = 0 ) → 𝑋 ∈ ℝ )
46 0red ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑋 ) ∧ ¬ 𝑋 = 0 ) → 0 ∈ ℝ )
47 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑋 ) ∧ ¬ 𝑋 = 0 ) → ¬ 𝑋 = 0 )
48 47 neqned ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑋 ) ∧ ¬ 𝑋 = 0 ) → 𝑋 ≠ 0 )
49 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑋 ) ∧ ¬ 𝑋 = 0 ) → ¬ 0 < 𝑋 )
50 45 46 48 49 lttri5d ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑋 ) ∧ ¬ 𝑋 = 0 ) → 𝑋 < 0 )
51 4 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
52 34 51 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ∈ ℂ )
53 52 51 subnegd ⊢ ( 𝜑 → ( ( 𝐴 − 𝑋 ) − - 𝑋 ) = ( ( 𝐴 − 𝑋 ) + 𝑋 ) )
54 34 51 npcand ⊢ ( 𝜑 → ( ( 𝐴 − 𝑋 ) + 𝑋 ) = 𝐴 )
55 53 54 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 − 𝑋 ) − - 𝑋 ) = 𝐴 )
56 38 51 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℂ )
57 56 51 subnegd ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) − - 𝑋 ) = ( ( 𝐵 − 𝑋 ) + 𝑋 ) )
58 38 51 npcand ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) + 𝑋 ) = 𝐵 )
59 57 58 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) − - 𝑋 ) = 𝐵 )
60 55 59 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑋 ) − - 𝑋 ) [,] ( ( 𝐵 − 𝑋 ) − - 𝑋 ) ) = ( 𝐴 [,] 𝐵 ) )
61 60 eqcomd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = ( ( ( 𝐴 − 𝑋 ) − - 𝑋 ) [,] ( ( 𝐵 − 𝑋 ) − - 𝑋 ) ) )
62 61 itgeq1d ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( ( 𝐴 − 𝑋 ) − - 𝑋 ) [,] ( ( 𝐵 − 𝑋 ) − - 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 0 ) → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( ( 𝐴 − 𝑋 ) − - 𝑋 ) [,] ( ( 𝐵 − 𝑋 ) − - 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
64 1 4 resubcld ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ∈ ℝ )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 0 ) → ( 𝐴 − 𝑋 ) ∈ ℝ )
66 2 4 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 0 ) → ( 𝐵 − 𝑋 ) ∈ ℝ )
68 eqid ⊢ ( ( 𝐵 − 𝑋 ) − ( 𝐴 − 𝑋 ) ) = ( ( 𝐵 − 𝑋 ) − ( 𝐴 − 𝑋 ) )
69 4 renegcld ⊢ ( 𝜑 → - 𝑋 ∈ ℝ )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 0 ) → - 𝑋 ∈ ℝ )
71 4 lt0neg1d ⊢ ( 𝜑 → ( 𝑋 < 0 ↔ 0 < - 𝑋 ) )
72 71 biimpa ⊢ ( ( 𝜑 ∧ 𝑋 < 0 ) → 0 < - 𝑋 )
73 70 72 elrpd ⊢ ( ( 𝜑 ∧ 𝑋 < 0 ) → - 𝑋 ∈ ℝ+ )
74 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑝 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑗 ) )
75 oveq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 + 1 ) = ( 𝑗 + 1 ) )
76 75 fveq2d ⊢ ( 𝑖 = 𝑗 → ( 𝑝 ‘ ( 𝑖 + 1 ) ) = ( 𝑝 ‘ ( 𝑗 + 1 ) ) )
77 74 76 breq12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) )
78 77 cbvralvw ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) )
79 78 anbi2i ⊢ ( ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 − 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 − 𝑋 ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) )
80 79 a1i ⊢ ( 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) → ( ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 − 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 − 𝑋 ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) ) )
81 80 rabbiia ⊢ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 − 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } = { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 − 𝑋 ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) }
82 81 mpteq2i ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 − 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 − 𝑋 ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) } )
83 13 82 eqtri ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 − 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 − 𝑋 ) ) ∧ ∀ 𝑗 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑗 ) < ( 𝑝 ‘ ( 𝑗 + 1 ) ) ) } )
84 5 6 7 fourierdlem11 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
85 84 simp3d ⊢ ( 𝜑 → 𝐴 < 𝐵 )
86 1 2 4 85 ltsub1dd ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) < ( 𝐵 − 𝑋 ) )
87 3 5 6 7 64 66 86 13 14 15 16 fourierdlem54 ⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) )
88 87 simpld ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) )
89 88 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
90 89 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 0 ) → 𝑁 ∈ ℕ )
91 88 simprd ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
92 91 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 0 ) → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
93 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 0 ) → 𝐹 : ℝ ⟶ ℂ )
94 38 34 51 nnncan2d ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) − ( 𝐴 − 𝑋 ) ) = ( 𝐵 − 𝐴 ) )
95 94 3 eqtr4di ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) − ( 𝐴 − 𝑋 ) ) = 𝑇 )
96 95 oveq2d ⊢ ( 𝜑 → ( 𝑥 + ( ( 𝐵 − 𝑋 ) − ( 𝐴 − 𝑋 ) ) ) = ( 𝑥 + 𝑇 ) )
97 96 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( 𝐵 − 𝑋 ) − ( 𝐴 − 𝑋 ) ) ) = ( 𝑥 + 𝑇 ) )
98 97 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + ( ( 𝐵 − 𝑋 ) − ( 𝐴 − 𝑋 ) ) ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) )
99 98 9 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + ( ( 𝐵 − 𝑋 ) − ( 𝐴 − 𝑋 ) ) ) ) = ( 𝐹 ‘ 𝑥 ) )
100 99 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 < 0 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + ( ( 𝐵 − 𝑋 ) − ( 𝐴 − 𝑋 ) ) ) ) = ( 𝐹 ‘ 𝑥 ) )
101 6 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑀 ∈ ℕ )
102 7 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
103 8 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 : ℝ ⟶ ℂ )
104 9 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
105 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
106 64 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 − 𝑋 ) ∈ ℝ )
107 64 rexrd ⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) ∈ ℝ* )
108 pnfxr ⊢ +∞ ∈ ℝ*
109 108 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
110 66 ltpnfd ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) < +∞ )
111 107 109 66 86 110 eliood ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ( ( 𝐴 − 𝑋 ) (,) +∞ ) )
112 111 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − 𝑋 ) ∈ ( ( 𝐴 − 𝑋 ) (,) +∞ ) )
113 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = ( 𝑦 + ( 𝑘 · 𝑇 ) ) )
114 113 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
115 114 rexbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
116 115 cbvrabv ⊢ { 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
117 116 uneq2i ⊢ ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑥 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
118 14 117 eqtri ⊢ 𝐻 = ( { ( 𝐴 − 𝑋 ) , ( 𝐵 − 𝑋 ) } ∪ { 𝑦 ∈ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
119 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
120 eqid ⊢ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
121 eqid ⊢ ( 𝐹 ↾ ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( 𝐹 ↾ ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
122 eqid ⊢ ( 𝑦 ∈ ( ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ ( 𝑦 − ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ) = ( 𝑦 ∈ ( ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ ( 𝑦 − ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) )
123 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) )
124 123 breq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑄 ‘ 𝑗 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) ↔ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) ) )
125 124 cbvrabv ⊢ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) }
126 125 supeq1i ⊢ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < )
127 126 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ) = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
128 19 127 eqtri ⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐽 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
129 5 3 101 102 103 104 105 106 112 13 118 15 16 17 18 119 120 121 122 128 fourierdlem90 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
130 129 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 < 0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
131 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
132 eqid ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 ) = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 )
133 5 3 101 102 103 104 105 131 106 112 13 118 15 16 17 18 119 120 128 132 fourierdlem89 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 ) ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( 𝐹 ‘ ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
134 133 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 < 0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 ) ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( 𝐹 ‘ ( 𝐽 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
135 12 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
136 eqid ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 ) = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 )
137 5 3 101 102 103 104 105 135 106 112 13 118 15 16 17 18 119 120 128 136 fourierdlem91 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 ) ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( 𝐹 ‘ ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
138 137 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 < 0 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) , ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝐿 ) ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) , ( 𝐹 ‘ ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
139 65 67 68 73 83 90 92 93 100 130 134 138 fourierdlem108 ⊢ ( ( 𝜑 ∧ 𝑋 < 0 ) → ∫ ( ( ( 𝐴 − 𝑋 ) − - 𝑋 ) [,] ( ( 𝐵 − 𝑋 ) − - 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
140 63 139 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑋 < 0 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
141 44 50 140 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑋 ) ∧ ¬ 𝑋 = 0 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
142 43 141 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ 0 < 𝑋 ) → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
143 32 142 pm2.61dan ⊢ ( 𝜑 → ∫ ( ( 𝐴 − 𝑋 ) [,] ( 𝐵 − 𝑋 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )