Metamath Proof Explorer

Theorem fourierdlem91

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

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

Proof

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