Metamath Proof Explorer

Theorem fourierdlem92

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by its period T . (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 fourierdlem92.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem92.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem92.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
4 fourierdlem92.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5 fourierdlem92.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
6 fourierdlem92.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
7 fourierdlem92.fper ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
8 fourierdlem92.s ⊢ 𝑆 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) )
9 fourierdlem92.h ⊢ 𝐻 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 + 𝑇 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 + 𝑇 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
10 fourierdlem92.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
11 fourierdlem92.cncf ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
12 fourierdlem92.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
13 fourierdlem92.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
14 1 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑇 ) → 𝐴 ∈ ℝ )
15 2 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑇 ) → 𝐵 ∈ ℝ )
16 4 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑇 ) → 𝑀 ∈ ℕ )
17 5 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑇 ) → 𝑇 ∈ ℝ )
18 simpr ⊢ ( ( 𝜑 ∧ 0 < 𝑇 ) → 0 < 𝑇 )
19 17 18 elrpd ⊢ ( ( 𝜑 ∧ 0 < 𝑇 ) → 𝑇 ∈ ℝ+ )
20 6 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑇 ) → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
21 7 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < 𝑇 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
22 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) )
23 22 oveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑄 ‘ 𝑗 ) + 𝑇 ) = ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) )
24 23 cbvmptv ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑗 ) + 𝑇 ) ) = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) )
25 10 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑇 ) → 𝐹 : ℝ ⟶ ℂ )
26 11 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < 𝑇 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
27 12 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < 𝑇 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
28 13 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < 𝑇 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
29 eqeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ( 𝑄 ‘ 𝑖 ) ↔ 𝑥 = ( 𝑄 ‘ 𝑖 ) ) )
30 eqeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
31 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
32 30 31 ifbieq2d ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑦 ) ) = if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
33 29 32 ifbieq2d ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 = ( 𝑄 ‘ 𝑖 ) , 𝑅 , if ( 𝑦 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑦 ) ) ) = if ( 𝑥 = ( 𝑄 ‘ 𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
34 33 cbvmptv ⊢ ( 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑦 = ( 𝑄 ‘ 𝑖 ) , 𝑅 , if ( 𝑦 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑦 ) ) ) ) = ( 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑄 ‘ 𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
35 eqid ⊢ ( 𝑥 ∈ ( ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑗 ) + 𝑇 ) ) ‘ 𝑖 ) [,] ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑗 ) + 𝑇 ) ) ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑦 = ( 𝑄 ‘ 𝑖 ) , 𝑅 , if ( 𝑦 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑦 ) ) ) ) ‘ ( 𝑥 − 𝑇 ) ) ) = ( 𝑥 ∈ ( ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑗 ) + 𝑇 ) ) ‘ 𝑖 ) [,] ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑗 ) + 𝑇 ) ) ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑦 = ( 𝑄 ‘ 𝑖 ) , 𝑅 , if ( 𝑦 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑦 ) ) ) ) ‘ ( 𝑥 − 𝑇 ) ) )
36 14 15 3 16 19 20 21 24 25 26 27 28 34 35 fourierdlem81 ⊢ ( ( 𝜑 ∧ 0 < 𝑇 ) → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → 𝑇 = 0 )
38 37 oveq2d ⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → ( 𝐴 + 𝑇 ) = ( 𝐴 + 0 ) )
39 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → 𝐴 ∈ ℂ )
41 40 addridd ⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → ( 𝐴 + 0 ) = 𝐴 )
42 38 41 eqtrd ⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → ( 𝐴 + 𝑇 ) = 𝐴 )
43 37 oveq2d ⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → ( 𝐵 + 𝑇 ) = ( 𝐵 + 0 ) )
44 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → 𝐵 ∈ ℂ )
46 45 addridd ⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → ( 𝐵 + 0 ) = 𝐵 )
47 43 46 eqtrd ⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → ( 𝐵 + 𝑇 ) = 𝐵 )
48 42 47 oveq12d ⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) = ( 𝐴 [,] 𝐵 ) )
49 48 itgeq1d ⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
50 49 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ 𝑇 = 0 ) → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
51 simpll ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ ¬ 𝑇 = 0 ) → 𝜑 )
52 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ ¬ 𝑇 = 0 ) → ¬ 𝑇 = 0 )
53 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ ¬ 𝑇 = 0 ) → ¬ 0 < 𝑇 )
54 ioran ⊢ ( ¬ ( 𝑇 = 0 ∨ 0 < 𝑇 ) ↔ ( ¬ 𝑇 = 0 ∧ ¬ 0 < 𝑇 ) )
55 52 53 54 sylanbrc ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ ¬ 𝑇 = 0 ) → ¬ ( 𝑇 = 0 ∨ 0 < 𝑇 ) )
56 51 5 syl ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ ¬ 𝑇 = 0 ) → 𝑇 ∈ ℝ )
57 0red ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ ¬ 𝑇 = 0 ) → 0 ∈ ℝ )
58 56 57 lttrid ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ ¬ 𝑇 = 0 ) → ( 𝑇 < 0 ↔ ¬ ( 𝑇 = 0 ∨ 0 < 𝑇 ) ) )
59 55 58 mpbird ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ ¬ 𝑇 = 0 ) → 𝑇 < 0 )
60 56 lt0neg1d ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ ¬ 𝑇 = 0 ) → ( 𝑇 < 0 ↔ 0 < - 𝑇 ) )
61 59 60 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ ¬ 𝑇 = 0 ) → 0 < - 𝑇 )
62 1 5 readdcld ⊢ ( 𝜑 → ( 𝐴 + 𝑇 ) ∈ ℝ )
63 62 recnd ⊢ ( 𝜑 → ( 𝐴 + 𝑇 ) ∈ ℂ )
64 5 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
65 63 64 negsubd ⊢ ( 𝜑 → ( ( 𝐴 + 𝑇 ) + - 𝑇 ) = ( ( 𝐴 + 𝑇 ) − 𝑇 ) )
66 39 64 pncand ⊢ ( 𝜑 → ( ( 𝐴 + 𝑇 ) − 𝑇 ) = 𝐴 )
67 65 66 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 + 𝑇 ) + - 𝑇 ) = 𝐴 )
68 2 5 readdcld ⊢ ( 𝜑 → ( 𝐵 + 𝑇 ) ∈ ℝ )
69 68 recnd ⊢ ( 𝜑 → ( 𝐵 + 𝑇 ) ∈ ℂ )
70 69 64 negsubd ⊢ ( 𝜑 → ( ( 𝐵 + 𝑇 ) + - 𝑇 ) = ( ( 𝐵 + 𝑇 ) − 𝑇 ) )
71 44 64 pncand ⊢ ( 𝜑 → ( ( 𝐵 + 𝑇 ) − 𝑇 ) = 𝐵 )
72 70 71 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 + 𝑇 ) + - 𝑇 ) = 𝐵 )
73 67 72 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝑇 ) + - 𝑇 ) [,] ( ( 𝐵 + 𝑇 ) + - 𝑇 ) ) = ( 𝐴 [,] 𝐵 ) )
74 73 eqcomd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = ( ( ( 𝐴 + 𝑇 ) + - 𝑇 ) [,] ( ( 𝐵 + 𝑇 ) + - 𝑇 ) ) )
75 74 itgeq1d ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( ( 𝐴 + 𝑇 ) + - 𝑇 ) [,] ( ( 𝐵 + 𝑇 ) + - 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
76 75 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( ( 𝐴 + 𝑇 ) + - 𝑇 ) [,] ( ( 𝐵 + 𝑇 ) + - 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
77 1 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → 𝐴 ∈ ℝ )
78 5 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → 𝑇 ∈ ℝ )
79 77 78 readdcld ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → ( 𝐴 + 𝑇 ) ∈ ℝ )
80 2 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → 𝐵 ∈ ℝ )
81 80 78 readdcld ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → ( 𝐵 + 𝑇 ) ∈ ℝ )
82 eqid ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 + 𝑇 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 + 𝑇 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 + 𝑇 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 + 𝑇 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
83 4 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → 𝑀 ∈ ℕ )
84 78 renegcld ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → - 𝑇 ∈ ℝ )
85 simpr ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → 0 < - 𝑇 )
86 84 85 elrpd ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → - 𝑇 ∈ ℝ+ )
87 3 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
88 4 87 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
89 6 88 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
90 89 simpld ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
91 elmapi ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
92 90 91 syl ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
93 92 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
94 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑇 ∈ ℝ )
95 93 94 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) ∈ ℝ )
96 95 8 fmptd ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑀 ) ⟶ ℝ )
97 reex ⊢ ℝ ∈ V
98 97 a1i ⊢ ( 𝜑 → ℝ ∈ V )
99 ovex ⊢ ( 0 ... 𝑀 ) ∈ V
100 99 a1i ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ V )
101 98 100 elmapd ⊢ ( 𝜑 → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ↔ 𝑆 : ( 0 ... 𝑀 ) ⟶ ℝ ) )
102 96 101 mpbird ⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
103 8 a1i ⊢ ( 𝜑 → 𝑆 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) ) )
104 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 0 ) )
105 104 oveq1d ⊢ ( 𝑖 = 0 → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) = ( ( 𝑄 ‘ 0 ) + 𝑇 ) )
106 105 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) = ( ( 𝑄 ‘ 0 ) + 𝑇 ) )
107 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
108 4 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
109 0le0 ⊢ 0 ≤ 0
110 109 a1i ⊢ ( 𝜑 → 0 ≤ 0 )
111 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
112 111 nn0ge0d ⊢ ( 𝑀 ∈ ℕ → 0 ≤ 𝑀 )
113 4 112 syl ⊢ ( 𝜑 → 0 ≤ 𝑀 )
114 107 108 107 110 113 elfzd ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
115 92 114 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
116 115 5 readdcld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) + 𝑇 ) ∈ ℝ )
117 103 106 114 116 fvmptd ⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) = ( ( 𝑄 ‘ 0 ) + 𝑇 ) )
118 simprll ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 0 ) = 𝐴 )
119 89 118 syl ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
120 119 oveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) + 𝑇 ) = ( 𝐴 + 𝑇 ) )
121 117 120 eqtrd ⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) = ( 𝐴 + 𝑇 ) )
122 fveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑀 ) )
123 122 oveq1d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) = ( ( 𝑄 ‘ 𝑀 ) + 𝑇 ) )
124 123 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 𝑀 ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) = ( ( 𝑄 ‘ 𝑀 ) + 𝑇 ) )
125 4 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
126 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
127 125 126 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
128 eluzfz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
129 127 128 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
130 92 129 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ℝ )
131 130 5 readdcld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑀 ) + 𝑇 ) ∈ ℝ )
132 103 124 129 131 fvmptd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑀 ) = ( ( 𝑄 ‘ 𝑀 ) + 𝑇 ) )
133 simprlr ⊢ ( ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
134 89 133 syl ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
135 134 oveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑀 ) + 𝑇 ) = ( 𝐵 + 𝑇 ) )
136 132 135 eqtrd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑀 ) = ( 𝐵 + 𝑇 ) )
137 121 136 jca ⊢ ( 𝜑 → ( ( 𝑆 ‘ 0 ) = ( 𝐴 + 𝑇 ) ∧ ( 𝑆 ‘ 𝑀 ) = ( 𝐵 + 𝑇 ) ) )
138 92 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
139 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
140 139 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
141 138 140 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
142 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
143 142 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
144 138 143 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
145 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑇 ∈ ℝ )
146 89 simprrd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
147 146 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
148 141 144 145 147 ltadd1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
149 141 145 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) ∈ ℝ )
150 8 fvmpt2 ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) ∈ ℝ ) → ( 𝑆 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) )
151 140 149 150 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) )
152 8 24 eqtr4i ⊢ 𝑆 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑗 ) + 𝑇 ) )
153 152 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑆 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑗 ) + 𝑇 ) ) )
154 fveq2 ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
155 154 oveq1d ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝑄 ‘ 𝑗 ) + 𝑇 ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
156 155 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → ( ( 𝑄 ‘ 𝑗 ) + 𝑇 ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
157 144 145 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ )
158 153 156 143 157 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
159 148 151 158 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
160 159 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
161 102 137 160 jca32 ⊢ ( 𝜑 → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = ( 𝐴 + 𝑇 ) ∧ ( 𝑆 ‘ 𝑀 ) = ( 𝐵 + 𝑇 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
162 9 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑆 ∈ ( 𝐻 ‘ 𝑀 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = ( 𝐴 + 𝑇 ) ∧ ( 𝑆 ‘ 𝑀 ) = ( 𝐵 + 𝑇 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
163 4 162 syl ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝐻 ‘ 𝑀 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = ( 𝐴 + 𝑇 ) ∧ ( 𝑆 ‘ 𝑀 ) = ( 𝐵 + 𝑇 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
164 161 163 mpbird ⊢ ( 𝜑 → 𝑆 ∈ ( 𝐻 ‘ 𝑀 ) )
165 9 fveq1i ⊢ ( 𝐻 ‘ 𝑀 ) = ( ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 + 𝑇 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 + 𝑇 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) ‘ 𝑀 )
166 164 165 eleqtrdi ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 + 𝑇 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 + 𝑇 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) ‘ 𝑀 ) )
167 166 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → 𝑆 ∈ ( ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( 𝐴 + 𝑇 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( 𝐵 + 𝑇 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) ‘ 𝑀 ) )
168 62 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐴 + 𝑇 ) ∈ ℝ )
169 68 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐵 + 𝑇 ) ∈ ℝ )
170 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) )
171 eliccre ⊢ ( ( ( 𝐴 + 𝑇 ) ∈ ℝ ∧ ( 𝐵 + 𝑇 ) ∈ ℝ ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ℝ )
172 168 169 170 171 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ℝ )
173 172 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ℂ )
174 64 negcld ⊢ ( 𝜑 → - 𝑇 ∈ ℂ )
175 174 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → - 𝑇 ∈ ℂ )
176 173 175 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 + - 𝑇 ) ∈ ℂ )
177 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝜑 )
178 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐴 ∈ ℝ )
179 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐵 ∈ ℝ )
180 5 renegcld ⊢ ( 𝜑 → - 𝑇 ∈ ℝ )
181 180 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → - 𝑇 ∈ ℝ )
182 172 181 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 + - 𝑇 ) ∈ ℝ )
183 65 66 eqtr2d ⊢ ( 𝜑 → 𝐴 = ( ( 𝐴 + 𝑇 ) + - 𝑇 ) )
184 183 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐴 = ( ( 𝐴 + 𝑇 ) + - 𝑇 ) )
185 168 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐴 + 𝑇 ) ∈ ℝ* )
186 169 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐵 + 𝑇 ) ∈ ℝ* )
187 iccgelb ⊢ ( ( ( 𝐴 + 𝑇 ) ∈ ℝ* ∧ ( 𝐵 + 𝑇 ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐴 + 𝑇 ) ≤ 𝑥 )
188 185 186 170 187 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐴 + 𝑇 ) ≤ 𝑥 )
189 168 172 181 188 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝐴 + 𝑇 ) + - 𝑇 ) ≤ ( 𝑥 + - 𝑇 ) )
190 184 189 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐴 ≤ ( 𝑥 + - 𝑇 ) )
191 iccleub ⊢ ( ( ( 𝐴 + 𝑇 ) ∈ ℝ* ∧ ( 𝐵 + 𝑇 ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ≤ ( 𝐵 + 𝑇 ) )
192 185 186 170 191 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ≤ ( 𝐵 + 𝑇 ) )
193 172 169 181 192 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 + - 𝑇 ) ≤ ( ( 𝐵 + 𝑇 ) + - 𝑇 ) )
194 169 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐵 + 𝑇 ) ∈ ℂ )
195 64 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑇 ∈ ℂ )
196 194 195 negsubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝐵 + 𝑇 ) + - 𝑇 ) = ( ( 𝐵 + 𝑇 ) − 𝑇 ) )
197 71 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝐵 + 𝑇 ) − 𝑇 ) = 𝐵 )
198 196 197 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝐵 + 𝑇 ) + - 𝑇 ) = 𝐵 )
199 193 198 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 + - 𝑇 ) ≤ 𝐵 )
200 178 179 182 190 199 eliccd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 + - 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) )
201 177 200 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝜑 ∧ ( 𝑥 + - 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
202 eleq1 ⊢ ( 𝑦 = ( 𝑥 + - 𝑇 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 + - 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
203 202 anbi2d ⊢ ( 𝑦 = ( 𝑥 + - 𝑇 ) → ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑 ∧ ( 𝑥 + - 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
204 oveq1 ⊢ ( 𝑦 = ( 𝑥 + - 𝑇 ) → ( 𝑦 + 𝑇 ) = ( ( 𝑥 + - 𝑇 ) + 𝑇 ) )
205 204 fveq2d ⊢ ( 𝑦 = ( 𝑥 + - 𝑇 ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ ( ( 𝑥 + - 𝑇 ) + 𝑇 ) ) )
206 fveq2 ⊢ ( 𝑦 = ( 𝑥 + - 𝑇 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑥 + - 𝑇 ) ) )
207 205 206 eqeq12d ⊢ ( 𝑦 = ( 𝑥 + - 𝑇 ) → ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ ( ( 𝑥 + - 𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥 + - 𝑇 ) ) ) )
208 203 207 imbi12d ⊢ ( 𝑦 = ( 𝑥 + - 𝑇 ) → ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝜑 ∧ ( 𝑥 + - 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( ( 𝑥 + - 𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥 + - 𝑇 ) ) ) ) )
209 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) )
210 209 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) )
211 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 + 𝑇 ) = ( 𝑦 + 𝑇 ) )
212 211 fveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) )
213 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
214 212 213 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) ) )
215 210 214 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) ) ) )
216 215 7 chvarvv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) )
217 208 216 vtoclg ⊢ ( ( 𝑥 + - 𝑇 ) ∈ ℂ → ( ( 𝜑 ∧ ( 𝑥 + - 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( ( 𝑥 + - 𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥 + - 𝑇 ) ) ) )
218 176 201 217 sylc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐹 ‘ ( ( 𝑥 + - 𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥 + - 𝑇 ) ) )
219 173 195 negsubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 + - 𝑇 ) = ( 𝑥 − 𝑇 ) )
220 219 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝑥 + - 𝑇 ) + 𝑇 ) = ( ( 𝑥 − 𝑇 ) + 𝑇 ) )
221 173 195 npcand ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝑥 − 𝑇 ) + 𝑇 ) = 𝑥 )
222 220 221 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝑥 + - 𝑇 ) + 𝑇 ) = 𝑥 )
223 222 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐹 ‘ ( ( 𝑥 + - 𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
224 218 223 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐹 ‘ ( 𝑥 + - 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
225 224 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < - 𝑇 ) ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐹 ‘ ( 𝑥 + - 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
226 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑆 ‘ 𝑗 ) = ( 𝑆 ‘ 𝑖 ) )
227 226 oveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑆 ‘ 𝑗 ) + - 𝑇 ) = ( ( 𝑆 ‘ 𝑖 ) + - 𝑇 ) )
228 227 cbvmptv ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑆 ‘ 𝑗 ) + - 𝑇 ) ) = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑆 ‘ 𝑖 ) + - 𝑇 ) )
229 10 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → 𝐹 : ℝ ⟶ ℂ )
230 10 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : ℝ ⟶ ℂ )
231 ioossre ⊢ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
232 231 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
233 230 232 feqresmpt ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑥 ∈ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
234 151 158 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) )
235 141 144 145 iooshift ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) = { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } )
236 234 235 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) = { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } )
237 236 mpteq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( 𝐹 ‘ 𝑥 ) ) )
238 simpll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → 𝜑 )
239 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
240 235 eleq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ↔ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) )
241 240 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) )
242 141 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
243 242 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
244 144 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
245 244 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
246 elioore ⊢ ( 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) → 𝑥 ∈ ℝ )
247 246 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑥 ∈ ℝ )
248 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑇 ∈ ℝ )
249 247 248 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) ∈ ℝ )
250 249 3adant2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) ∈ ℝ )
251 141 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
252 64 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑇 ∈ ℂ )
253 251 252 pncand ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) − 𝑇 ) = ( 𝑄 ‘ 𝑖 ) )
254 253 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) − 𝑇 ) )
255 254 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) − 𝑇 ) )
256 149 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) ∈ ℝ )
257 247 3adant2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑥 ∈ ℝ )
258 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑇 ∈ ℝ )
259 149 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) ∈ ℝ* )
260 259 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) ∈ ℝ* )
261 157 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ* )
262 261 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ* )
263 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) )
264 ioogtlb ⊢ ( ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) ∈ ℝ* ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ* ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) < 𝑥 )
265 260 262 263 264 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) < 𝑥 )
266 256 257 258 265 ltsub1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) − 𝑇 ) < ( 𝑥 − 𝑇 ) )
267 255 266 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑥 − 𝑇 ) )
268 157 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ )
269 iooltub ⊢ ( ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) ∈ ℝ* ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ* ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑥 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
270 260 262 263 269 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑥 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
271 257 268 258 270 ltsub1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) < ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) − 𝑇 ) )
272 144 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
273 272 252 pncand ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
274 273 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
275 271 274 breqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
276 243 245 250 267 275 eliood ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
277 238 239 241 276 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → ( 𝑥 − 𝑇 ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
278 fvres ⊢ ( ( 𝑥 − 𝑇 ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥 − 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) )
279 277 278 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥 − 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) )
280 238 241 249 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → ( 𝑥 − 𝑇 ) ∈ ℝ )
281 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝐴 ∈ ℝ )
282 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝐵 ∈ ℝ )
283 66 eqcomd ⊢ ( 𝜑 → 𝐴 = ( ( 𝐴 + 𝑇 ) − 𝑇 ) )
284 283 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝐴 = ( ( 𝐴 + 𝑇 ) − 𝑇 ) )
285 62 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝐴 + 𝑇 ) ∈ ℝ )
286 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴 ∈ ℝ )
287 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
288 287 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴 ∈ ℝ* )
289 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
290 289 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐵 ∈ ℝ* )
291 3 4 6 fourierdlem15 ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
292 291 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
293 292 140 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( 𝐴 [,] 𝐵 ) )
294 iccgelb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑄 ‘ 𝑖 ) ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 𝑄 ‘ 𝑖 ) )
295 288 290 293 294 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴 ≤ ( 𝑄 ‘ 𝑖 ) )
296 286 141 145 295 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐴 + 𝑇 ) ≤ ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) )
297 296 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝐴 + 𝑇 ) ≤ ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) )
298 285 256 257 297 265 lelttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝐴 + 𝑇 ) < 𝑥 )
299 285 257 258 298 ltsub1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝐴 + 𝑇 ) − 𝑇 ) < ( 𝑥 − 𝑇 ) )
300 284 299 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝐴 < ( 𝑥 − 𝑇 ) )
301 281 250 300 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝐴 ≤ ( 𝑥 − 𝑇 ) )
302 144 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
303 292 143 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
304 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≤ 𝐵 )
305 288 290 303 304 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≤ 𝐵 )
306 305 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≤ 𝐵 )
307 250 302 282 275 306 ltletrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) < 𝐵 )
308 250 282 307 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) ≤ 𝐵 )
309 281 282 250 301 308 eliccd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) )
310 238 239 241 309 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → ( 𝑥 − 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) )
311 238 310 jca ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → ( 𝜑 ∧ ( 𝑥 − 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
312 eleq1 ⊢ ( 𝑦 = ( 𝑥 − 𝑇 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 − 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
313 312 anbi2d ⊢ ( 𝑦 = ( 𝑥 − 𝑇 ) → ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑 ∧ ( 𝑥 − 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
314 oveq1 ⊢ ( 𝑦 = ( 𝑥 − 𝑇 ) → ( 𝑦 + 𝑇 ) = ( ( 𝑥 − 𝑇 ) + 𝑇 ) )
315 314 fveq2d ⊢ ( 𝑦 = ( 𝑥 − 𝑇 ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ ( ( 𝑥 − 𝑇 ) + 𝑇 ) ) )
316 fveq2 ⊢ ( 𝑦 = ( 𝑥 − 𝑇 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) )
317 315 316 eqeq12d ⊢ ( 𝑦 = ( 𝑥 − 𝑇 ) → ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ ( ( 𝑥 − 𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) ) )
318 313 317 imbi12d ⊢ ( 𝑦 = ( 𝑥 − 𝑇 ) → ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝜑 ∧ ( 𝑥 − 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( ( 𝑥 − 𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) ) ) )
319 318 216 vtoclg ⊢ ( ( 𝑥 − 𝑇 ) ∈ ℝ → ( ( 𝜑 ∧ ( 𝑥 − 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( ( 𝑥 − 𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) ) )
320 280 311 319 sylc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → ( 𝐹 ‘ ( ( 𝑥 − 𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) )
321 241 246 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → 𝑥 ∈ ℝ )
322 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
323 322 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
324 64 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℂ )
325 323 324 npcand ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 − 𝑇 ) + 𝑇 ) = 𝑥 )
326 325 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( ( 𝑥 − 𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
327 238 321 326 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → ( 𝐹 ‘ ( ( 𝑥 − 𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
328 279 320 327 3eqtr2rd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥 − 𝑇 ) ) )
329 328 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥 − 𝑇 ) ) ) )
330 233 237 329 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥 − 𝑇 ) ) ) )
331 ioosscn ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
332 331 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
333 eqeq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 = ( 𝑧 + 𝑇 ) ↔ 𝑥 = ( 𝑧 + 𝑇 ) ) )
334 333 rexbidv ⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ) )
335 oveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 + 𝑇 ) = ( 𝑦 + 𝑇 ) )
336 335 eqeq2d ⊢ ( 𝑧 = 𝑦 → ( 𝑥 = ( 𝑧 + 𝑇 ) ↔ 𝑥 = ( 𝑦 + 𝑇 ) ) )
337 336 cbvrexvw ⊢ ( ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) )
338 334 337 bitrdi ⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) ) )
339 338 cbvrabv ⊢ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } = { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) }
340 eqid ⊢ ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥 − 𝑇 ) ) ) = ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥 − 𝑇 ) ) )
341 332 252 339 11 340 cncfshift ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥 − 𝑇 ) ) ) ∈ ( { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } –cn→ ℂ ) )
342 236 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } = ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
343 342 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } –cn→ ℂ ) = ( ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
344 341 343 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥 − 𝑇 ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
345 330 344 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
346 345 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < - 𝑇 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
347 ffdm ⊢ ( 𝐹 : ℝ ⟶ ℂ → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) )
348 10 347 syl ⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) )
349 348 simpld ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ )
350 349 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
351 ioossre ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
352 fdm ⊢ ( 𝐹 : ℝ ⟶ ℂ → dom 𝐹 = ℝ )
353 230 352 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom 𝐹 = ℝ )
354 351 353 sseqtrrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 )
355 339 eqcomi ⊢ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) } = { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) }
356 232 342 353 3sstr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ⊆ dom 𝐹 )
357 339 356 eqsstrrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) } ⊆ dom 𝐹 )
358 simpll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝜑 )
359 358 287 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐴 ∈ ℝ* )
360 358 289 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐵 ∈ ℝ* )
361 358 291 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
362 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
363 ioossicc ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
364 363 sseli ⊢ ( 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
365 364 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
366 359 360 361 362 365 fourierdlem1 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
367 eleq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) )
368 367 anbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) )
369 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 + 𝑇 ) = ( 𝑧 + 𝑇 ) )
370 369 fveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑧 + 𝑇 ) ) )
371 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
372 370 371 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ ( 𝑧 + 𝑇 ) ) = ( 𝐹 ‘ 𝑧 ) ) )
373 368 372 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑧 + 𝑇 ) ) = ( 𝐹 ‘ 𝑧 ) ) ) )
374 373 7 chvarvv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑧 + 𝑇 ) ) = ( 𝐹 ‘ 𝑧 ) )
375 358 366 374 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑧 + 𝑇 ) ) = ( 𝐹 ‘ 𝑧 ) )
376 350 332 354 252 355 357 375 12 limcperiod ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) } ) limℂ ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) ) )
377 355 342 eqtrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) } = ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
378 377 reseq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) } ) = ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
379 151 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) )
380 378 379 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) } ) limℂ ( ( 𝑄 ‘ 𝑖 ) + 𝑇 ) ) = ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑖 ) ) )
381 376 380 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑖 ) ) )
382 381 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < - 𝑇 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑖 ) ) )
383 350 332 354 252 355 357 375 13 limcperiod ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) } ) limℂ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) )
384 158 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) = ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
385 378 384 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) } ) limℂ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) = ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
386 383 385 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
387 386 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < - 𝑇 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
388 eqeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ( 𝑆 ‘ 𝑖 ) ↔ 𝑥 = ( 𝑆 ‘ 𝑖 ) ) )
389 eqeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ↔ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
390 389 31 ifbieq2d ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑦 ) ) = if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
391 388 390 ifbieq2d ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 = ( 𝑆 ‘ 𝑖 ) , 𝑅 , if ( 𝑦 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑦 ) ) ) = if ( 𝑥 = ( 𝑆 ‘ 𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
392 391 cbvmptv ⊢ ( 𝑦 ∈ ( ( 𝑆 ‘ 𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑦 = ( 𝑆 ‘ 𝑖 ) , 𝑅 , if ( 𝑦 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑦 ) ) ) ) = ( 𝑥 ∈ ( ( 𝑆 ‘ 𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆 ‘ 𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
393 eqid ⊢ ( 𝑥 ∈ ( ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑆 ‘ 𝑗 ) + - 𝑇 ) ) ‘ 𝑖 ) [,] ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑆 ‘ 𝑗 ) + - 𝑇 ) ) ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑦 ∈ ( ( 𝑆 ‘ 𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑦 = ( 𝑆 ‘ 𝑖 ) , 𝑅 , if ( 𝑦 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑦 ) ) ) ) ‘ ( 𝑥 − - 𝑇 ) ) ) = ( 𝑥 ∈ ( ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑆 ‘ 𝑗 ) + - 𝑇 ) ) ‘ 𝑖 ) [,] ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑆 ‘ 𝑗 ) + - 𝑇 ) ) ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑦 ∈ ( ( 𝑆 ‘ 𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑦 = ( 𝑆 ‘ 𝑖 ) , 𝑅 , if ( 𝑦 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ 𝑦 ) ) ) ) ‘ ( 𝑥 − - 𝑇 ) ) )
394 79 81 82 83 86 167 225 228 229 346 382 387 392 393 fourierdlem81 ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → ∫ ( ( ( 𝐴 + 𝑇 ) + - 𝑇 ) [,] ( ( 𝐵 + 𝑇 ) + - 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
395 76 394 eqtr2d ⊢ ( ( 𝜑 ∧ 0 < - 𝑇 ) → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
396 51 61 395 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) ∧ ¬ 𝑇 = 0 ) → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
397 50 396 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ 0 < 𝑇 ) → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
398 36 397 pm2.61dan ⊢ ( 𝜑 → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )