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