Metamath Proof Explorer

Theorem fourierdlem89

Description: Given a piecewise continuous function and changing the interval and the partition, the limit at the lower bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem89.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem89.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem89.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem89.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem89.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
fourierdlem89.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
fourierdlem89.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem89.limc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
fourierdlem89.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem89.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
fourierdlem89.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem89.12 ⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
fourierdlem89.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
fourierdlem89.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
fourierdlem89.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem89.z ⊢ 𝑍 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
fourierdlem89.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
fourierdlem89.u ⊢ 𝑈 = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
fourierdlem89.20 ⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
fourierdlem89.21 ⊢ 𝑉 = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 )
Assertion fourierdlem89 ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem89.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem89.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
3 fourierdlem89.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 fourierdlem89.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5 fourierdlem89.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
6 fourierdlem89.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
7 fourierdlem89.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
8 fourierdlem89.limc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
9 fourierdlem89.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
10 fourierdlem89.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
11 fourierdlem89.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
12 fourierdlem89.12 ⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
13 fourierdlem89.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
14 fourierdlem89.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
15 fourierdlem89.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
16 fourierdlem89.z ⊢ 𝑍 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
17 fourierdlem89.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
18 fourierdlem89.u ⊢ 𝑈 = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
19 fourierdlem89.20 ⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
20 fourierdlem89.21 ⊢ 𝑉 = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 )
21 1 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
22 3 21 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
23 4 22 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
24 23 simpld ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
25 elmapi ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
26 24 25 syl ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
27 fzossfz ⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
28 1 3 4 2 15 16 19 fourierdlem37 ⊢ ( 𝜑 → ( 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 ∈ ℝ → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ 𝑥 ) ) } ) ) )
29 28 simpld ⊢ ( 𝜑 → 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) )
30 elioore ⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) → 𝐷 ∈ ℝ )
31 10 30 syl ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
32 elioo4g ⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) ↔ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) ) )
33 10 32 sylib ⊢ ( 𝜑 → ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) ) )
34 33 simprd ⊢ ( 𝜑 → ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) )
35 34 simpld ⊢ ( 𝜑 → 𝐶 < 𝐷 )
36 oveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
37 36 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
38 37 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
39 38 cbvrabv ⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
40 39 uneq2i ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
41 12 fveq2i ⊢ ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
42 41 oveq1i ⊢ ( ( ♯ ‘ 𝐻 ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
43 13 42 eqtri ⊢ 𝑁 = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
44 isoeq5 ⊢ ( 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) → ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
45 12 44 ax-mp ⊢ ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
46 45 iotabii ⊢ ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
47 14 46 eqtri ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
48 2 1 3 4 9 31 35 11 40 43 47 fourierdlem54 ⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
49 48 simpld ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) )
50 49 simprd ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
51 49 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
52 11 fourierdlem2 ⊢ ( 𝑁 ∈ ℕ → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
53 51 52 syl ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
54 50 53 mpbid ⊢ ( 𝜑 → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
55 54 simpld ⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) )
56 elmapi ⊢ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
57 55 56 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
58 elfzofz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
59 17 58 syl ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑁 ) )
60 57 59 ffvelrnd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
61 29 60 ffvelrnd ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) )
62 27 61 sselid ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ... 𝑀 ) )
63 26 62 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
64 63 rexrd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ* )
65 64 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ* )
66 fzofzp1 ⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ∈ ( 0 ... 𝑀 ) )
67 61 66 syl ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ∈ ( 0 ... 𝑀 ) )
68 26 67 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ∈ ℝ )
69 68 rexrd ⊢ ( 𝜑 → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ∈ ℝ* )
70 69 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ∈ ℝ* )
71 1 3 4 fourierdlem11 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
72 71 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
73 71 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
74 72 73 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
75 71 simp3d ⊢ ( 𝜑 → 𝐴 < 𝐵 )
76 72 73 75 16 fourierdlem17 ⊢ ( 𝜑 → 𝑍 : ( 𝐴 (,] 𝐵 ) ⟶ ( 𝐴 [,] 𝐵 ) )
77 72 73 75 2 15 fourierdlem4 ⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
78 77 60 ffvelrnd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
79 76 78 ffvelrnd ⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( 𝐴 [,] 𝐵 ) )
80 74 79 sseldd ⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
81 80 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
82 63 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
83 72 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
84 iocssre ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
85 83 73 84 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
86 fzofzp1 ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
87 17 86 syl ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
88 57 87 ffvelrnd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
89 77 88 ffvelrnd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ( 𝐴 (,] 𝐵 ) )
90 85 89 sseldd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
91 54 simprrd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
92 fveq2 ⊢ ( 𝑖 = 𝐽 → ( 𝑆 ‘ 𝑖 ) = ( 𝑆 ‘ 𝐽 ) )
93 oveq1 ⊢ ( 𝑖 = 𝐽 → ( 𝑖 + 1 ) = ( 𝐽 + 1 ) )
94 93 fveq2d ⊢ ( 𝑖 = 𝐽 → ( 𝑆 ‘ ( 𝑖 + 1 ) ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
95 92 94 breq12d ⊢ ( 𝑖 = 𝐽 → ( ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
96 95 rspccva ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
97 91 17 96 syl2anc ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
98 60 88 posdifd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ↔ 0 < ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
99 97 98 mpbid ⊢ ( 𝜑 → 0 < ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
100 17 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) )
101 eleq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↔ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) )
102 101 anbi2d ⊢ ( 𝑗 = 𝐽 → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ) )
103 oveq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 + 1 ) = ( 𝐽 + 1 ) )
104 103 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
105 104 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
106 fveq2 ⊢ ( 𝑗 = 𝐽 → ( 𝑆 ‘ 𝑗 ) = ( 𝑆 ‘ 𝐽 ) )
107 106 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) )
108 107 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
109 105 108 oveq12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
110 104 106 oveq12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
111 109 110 eqeq12d ⊢ ( 𝑗 = 𝐽 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
112 102 111 imbi12d ⊢ ( 𝑗 = 𝐽 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) ) )
113 2 oveq2i ⊢ ( 𝑘 · 𝑇 ) = ( 𝑘 · ( 𝐵 − 𝐴 ) )
114 113 oveq2i ⊢ ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) )
115 114 eleq1i ⊢ ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
116 115 rexbii ⊢ ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
117 116 rgenw ⊢ ∀ 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
118 rabbi ⊢ ( ∀ 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) ↔ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
119 117 118 mpbi ⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 }
120 119 uneq2i ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
121 120 fveq2i ⊢ ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
122 121 oveq1i ⊢ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
123 43 122 eqtri ⊢ 𝑁 = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
124 isoeq5 ⊢ ( ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) → ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ) )
125 120 124 ax-mp ⊢ ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
126 125 iotabii ⊢ ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
127 47 126 eqtri ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
128 eqid ⊢ ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
129 1 2 3 4 9 10 11 123 127 15 16 128 fourierdlem65 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
130 112 129 vtoclg ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
131 17 100 130 sylc ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
132 99 131 breqtrrd ⊢ ( 𝜑 → 0 < ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
133 80 90 posdifd ⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↔ 0 < ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) )
134 132 133 mpbird ⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
135 id ⊢ ( 𝜑 → 𝜑 )
136 108 105 oveq12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
137 106 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) )
138 137 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
139 137 oveq1d ⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) = ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) )
140 139 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
141 138 140 oveq12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) = ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
142 136 141 sseq12d ⊢ ( 𝑗 = 𝐽 → ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) ↔ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
143 102 142 imbi12d ⊢ ( 𝑗 = 𝐽 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) ) ↔ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ) )
144 eqid ⊢ ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) = ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) )
145 2 1 3 4 9 31 35 11 40 43 47 15 16 144 19 fourierdlem79 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) )
146 143 145 vtoclg ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
147 146 anabsi7 ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
148 135 17 147 syl2anc ⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
149 63 68 80 90 134 148 fourierdlem10 ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ≤ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
150 149 simpld ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
151 150 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
152 neqne ⊢ ( ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ≠ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
153 152 adantl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ≠ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
154 82 81 151 153 leneltd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
155 149 simprd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ≤ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
156 80 90 68 134 155 ltletrd ⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
157 156 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
158 65 70 81 154 157 eliood ⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
159 fvres ⊢ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
160 158 159 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
161 160 eqcomd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
162 161 ifeq2da ⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) = if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) )
163 fdm ⊢ ( 𝐹 : ℝ ⟶ ℂ → dom 𝐹 = ℝ )
164 5 163 syl ⊢ ( 𝜑 → dom 𝐹 = ℝ )
165 164 feq2d ⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ↔ 𝐹 : ℝ ⟶ ℂ ) )
166 5 165 mpbird ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ )
167 ioosscn ⊢ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ℂ
168 167 a1i ⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ℂ )
169 ioossre ⊢ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ℝ
170 169 164 sseqtrrid ⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ dom 𝐹 )
171 88 90 resubcld ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ℝ )
172 18 171 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
173 172 recnd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
174 eqid ⊢ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } = { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) }
175 80 90 172 iooshift ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) = { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } )
176 ioossre ⊢ ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) ⊆ ℝ
177 176 164 sseqtrrid ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) ⊆ dom 𝐹 )
178 175 177 eqsstrrd ⊢ ( 𝜑 → { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ⊆ dom 𝐹 )
179 elioore ⊢ ( 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 ∈ ℝ )
180 73 72 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
181 2 180 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
182 181 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
183 72 73 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
184 75 183 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
185 184 2 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑇 )
186 185 gt0ne0d ⊢ ( 𝜑 → 𝑇 ≠ 0 )
187 173 182 186 divcan1d ⊢ ( 𝜑 → ( ( 𝑈 / 𝑇 ) · 𝑇 ) = 𝑈 )
188 187 eqcomd ⊢ ( 𝜑 → 𝑈 = ( ( 𝑈 / 𝑇 ) · 𝑇 ) )
189 188 oveq2d ⊢ ( 𝜑 → ( 𝑦 + 𝑈 ) = ( 𝑦 + ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) )
190 189 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 + 𝑈 ) = ( 𝑦 + ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) )
191 190 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + 𝑈 ) ) = ( 𝐹 ‘ ( 𝑦 + ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) ) )
192 5 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℂ )
193 181 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑇 ∈ ℝ )
194 90 recnd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
195 88 recnd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℂ )
196 194 195 negsubdi2d ⊢ ( 𝜑 → - ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
197 196 eqcomd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = - ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
198 197 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) / 𝑇 ) = ( - ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) )
199 18 oveq1i ⊢ ( 𝑈 / 𝑇 ) = ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) / 𝑇 )
200 199 a1i ⊢ ( 𝜑 → ( 𝑈 / 𝑇 ) = ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) / 𝑇 ) )
201 15 a1i ⊢ ( 𝜑 → 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
202 id ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
203 oveq2 ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( 𝐵 − 𝑥 ) = ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
204 203 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) )
205 204 fveq2d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
206 205 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
207 202 206 oveq12d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
208 207 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
209 73 88 resubcld ⊢ ( 𝜑 → ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
210 209 181 186 redivcld ⊢ ( 𝜑 → ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℝ )
211 210 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℤ )
212 211 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ )
213 212 181 remulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
214 88 213 readdcld ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
215 201 208 88 214 fvmptd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
216 215 oveq1d ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
217 212 recnd ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℂ )
218 217 182 mulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
219 195 218 pncan2d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
220 216 219 eqtrd ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
221 220 218 eqeltrd ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
222 221 182 186 divnegd ⊢ ( 𝜑 → - ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) = ( - ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) )
223 198 200 222 3eqtr4d ⊢ ( 𝜑 → ( 𝑈 / 𝑇 ) = - ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) )
224 220 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) )
225 217 182 186 divcan4d ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
226 224 225 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
227 226 211 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℤ )
228 227 znegcld ⊢ ( 𝜑 → - ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℤ )
229 223 228 eqeltrd ⊢ ( 𝜑 → ( 𝑈 / 𝑇 ) ∈ ℤ )
230 229 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑈 / 𝑇 ) ∈ ℤ )
231 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
232 6 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
233 192 193 230 231 232 fperiodmul ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
234 191 233 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + 𝑈 ) ) = ( 𝐹 ‘ 𝑦 ) )
235 179 234 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑈 ) ) = ( 𝐹 ‘ 𝑦 ) )
236 23 simprrd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
237 fveq2 ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
238 oveq1 ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑖 + 1 ) = ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) )
239 238 fveq2d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
240 237 239 breq12d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
241 240 rspccva ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
242 236 61 241 syl2anc ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
243 61 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) )
244 eleq1 ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) )
245 244 anbi2d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) )
246 237 239 oveq12d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
247 246 reseq2d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
248 246 oveq1d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) = ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) )
249 247 248 eleq12d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) ↔ ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) )
250 245 249 imbi12d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) ) ↔ ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) ) )
251 250 7 vtoclg ⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) → ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) )
252 61 243 251 sylc ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) )
253 nfv ⊢ Ⅎ 𝑖 ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) )
254 nfmpt1 ⊢ Ⅎ 𝑖 ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 )
255 20 254 nfcxfr ⊢ Ⅎ 𝑖 𝑉
256 nfcv ⊢ Ⅎ 𝑖 ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) )
257 255 256 nffv ⊢ Ⅎ 𝑖 ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) )
258 257 nfel1 ⊢ Ⅎ 𝑖 ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
259 253 258 nfim ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
260 245 biimpar ⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) )
261 260 3adant2 ⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) )
262 261 8 syl ⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
263 fveq2 ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
264 263 eqcomd ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑉 ‘ 𝑖 ) )
265 264 adantr ⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑉 ‘ 𝑖 ) )
266 260 simprd ⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
267 elex ⊢ ( 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) → 𝑅 ∈ V )
268 260 8 267 3syl ⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → 𝑅 ∈ V )
269 20 fvmpt2 ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑅 ∈ V ) → ( 𝑉 ‘ 𝑖 ) = 𝑅 )
270 266 268 269 syl2anc ⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑉 ‘ 𝑖 ) = 𝑅 )
271 265 270 eqtrd ⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = 𝑅 )
272 271 3adant2 ⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = 𝑅 )
273 247 237 oveq12d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
274 273 eqcomd ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
275 274 3ad2ant1 ⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
276 262 272 275 3eltr4d ⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
277 276 3exp ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) → ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ) )
278 8 2a1i ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ) )
279 277 278 impbid ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ) )
280 259 279 8 vtoclg1f ⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) → ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) )
281 61 243 280 sylc ⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
282 eqid ⊢ if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) = if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
283 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) [,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) [,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
284 63 68 242 252 281 80 90 134 148 282 283 fourierdlem32 ⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) limℂ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
285 148 resabs1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝐹 ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
286 285 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) limℂ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) limℂ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
287 284 286 eleqtrd ⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) limℂ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
288 166 168 170 173 174 178 235 287 limcperiod ⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) limℂ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) ) )
289 18 oveq2i ⊢ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
290 289 a1i ⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
291 9 31 iccssred ⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℝ )
292 ax-resscn ⊢ ℝ ⊆ ℂ
293 291 292 sstrdi ⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℂ )
294 11 51 50 fourierdlem15 ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐶 [,] 𝐷 ) )
295 294 59 ffvelrnd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ( 𝐶 [,] 𝐷 ) )
296 293 295 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℂ )
297 195 296 subcld ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ∈ ℂ )
298 80 recnd ⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℂ )
299 194 297 298 subsub23d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
300 131 299 mpbird ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
301 300 eqcomd ⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
302 301 oveq1d ⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
303 194 297 subcld ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℂ )
304 303 195 194 addsub12d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
305 194 297 194 sub32d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
306 194 subidd ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = 0 )
307 306 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
308 df-neg ⊢ - ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) = ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
309 195 296 negsubdi2d ⊢ ( 𝜑 → - ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
310 308 309 eqtr3id ⊢ ( 𝜑 → ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
311 305 307 310 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
312 311 oveq2d ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
313 195 296 pncan3d ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑆 ‘ 𝐽 ) )
314 304 312 313 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝑆 ‘ 𝐽 ) )
315 290 302 314 3eqtrd ⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( 𝑆 ‘ 𝐽 ) )
316 315 oveq2d ⊢ ( 𝜑 → ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) limℂ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) ) = ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) limℂ ( 𝑆 ‘ 𝐽 ) ) )
317 288 316 eleqtrd ⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) limℂ ( 𝑆 ‘ 𝐽 ) ) )
318 18 oveq2i ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
319 194 195 pncan3d ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
320 318 319 syl5eq ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
321 315 320 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) = ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
322 175 321 eqtr3d ⊢ ( 𝜑 → { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } = ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
323 322 reseq2d ⊢ ( 𝜑 → ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) = ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
324 323 oveq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) limℂ ( 𝑆 ‘ 𝐽 ) ) = ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝐽 ) ) )
325 317 324 eleqtrd ⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝐽 ) ) )
326 162 325 eqeltrd ⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝐽 ) ) )