This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem90

Description: Given a piecewise continuous function, it is still continuous with respect to an open interval of the moved partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 fourierdlem90.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem90.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
3 fourierdlem90.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 fourierdlem90.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5 fourierdlem90.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
6 fourierdlem90.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
7 fourierdlem90.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
8 fourierdlem90.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
9 fourierdlem90.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
10 fourierdlem90.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
11 fourierdlem90.h ⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
12 fourierdlem90.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
13 fourierdlem90.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
14 fourierdlem90.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
15 fourierdlem90.J ⊢ 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
16 fourierdlem90.17 ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
17 fourierdlem90.u ⊢ 𝑈 = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
18 fourierdlem90.g ⊢ 𝐺 = ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
19 fourierdlem90.r ⊢ 𝑅 = ( 𝑦 ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) )
20 fourierdlem90.i ⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
21 1 3 4 fourierdlem11 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
22 21 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
23 21 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
24 22 23 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
25 21 simp3d ⊢ ( 𝜑 → 𝐴 < 𝐵 )
26 22 23 25 15 fourierdlem17 ⊢ ( 𝜑 → 𝐿 : ( 𝐴 (,] 𝐵 ) ⟶ ( 𝐴 [,] 𝐵 ) )
27 22 23 25 2 14 fourierdlem4 ⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
28 elioore ⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) → 𝐷 ∈ ℝ )
29 9 28 syl ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
30 elioo4g ⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) ↔ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) ) )
31 9 30 sylib ⊢ ( 𝜑 → ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) ) )
32 31 simprd ⊢ ( 𝜑 → ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) )
33 32 simpld ⊢ ( 𝜑 → 𝐶 < 𝐷 )
34 2 1 3 4 8 29 33 10 11 12 13 fourierdlem54 ⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) )
35 34 simpld ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) )
36 35 simprd ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
37 35 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
38 10 fourierdlem2 ⊢ ( 𝑁 ∈ ℕ → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
39 37 38 syl ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
40 36 39 mpbid ⊢ ( 𝜑 → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
41 40 simpld ⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) )
42 elmapi ⊢ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
43 41 42 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
44 elfzofz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
45 16 44 syl ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑁 ) )
46 43 45 ffvelcdmd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
47 27 46 ffvelcdmd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
48 26 47 ffvelcdmd ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( 𝐴 [,] 𝐵 ) )
49 24 48 sseldd ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
50 22 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
51 iocssre ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
52 50 23 51 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
53 fzofzp1 ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
54 16 53 syl ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
55 43 54 ffvelcdmd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
56 27 55 ffvelcdmd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ( 𝐴 (,] 𝐵 ) )
57 52 56 sseldd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
58 eqid ⊢ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
59 55 57 resubcld ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ℝ )
60 17 59 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
61 eqid ⊢ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) = ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) )
62 eleq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↔ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) )
63 62 anbi2d ⊢ ( 𝑗 = 𝐽 → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ) )
64 fveq2 ⊢ ( 𝑗 = 𝐽 → ( 𝑆 ‘ 𝑗 ) = ( 𝑆 ‘ 𝐽 ) )
65 64 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) )
66 65 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
67 oveq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 + 1 ) = ( 𝐽 + 1 ) )
68 67 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
69 68 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
70 66 69 oveq12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
71 64 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) )
72 71 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
73 71 oveq1d ⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) = ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) )
74 73 fveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
75 72 74 oveq12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) = ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
76 70 75 sseq12d ⊢ ( 𝑗 = 𝐽 → ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) ↔ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
77 63 76 imbi12d ⊢ ( 𝑗 = 𝐽 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) ) ↔ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ) )
78 2 oveq2i ⊢ ( 𝑘 · 𝑇 ) = ( 𝑘 · ( 𝐵 − 𝐴 ) )
79 78 oveq2i ⊢ ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) )
80 79 eleq1i ⊢ ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
81 80 rexbii ⊢ ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
82 81 a1i ⊢ ( 𝑦 ∈ ( 𝐶 [,] 𝐷 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
83 82 rabbiia ⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 }
84 83 uneq2i ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
85 11 84 eqtri ⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
86 id ⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
87 2 eqcomi ⊢ ( 𝐵 − 𝐴 ) = 𝑇
88 87 oveq2i ⊢ ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( 𝑘 · 𝑇 )
89 88 a1i ⊢ ( 𝑦 = 𝑥 → ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( 𝑘 · 𝑇 ) )
90 86 89 oveq12d ⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
91 90 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
92 91 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
93 92 cbvrabv ⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } = { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
94 93 uneq2i ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
95 85 94 eqtri ⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
96 eqid ⊢ ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) = ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) )
97 2 1 3 4 8 29 33 10 95 12 13 14 15 96 20 fourierdlem79 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) )
98 77 97 vtoclg ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
99 98 anabsi7 ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
100 16 99 mpdan ⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
101 100 resabs1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
102 101 eqcomd ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
103 1 3 4 2 14 15 20 fourierdlem37 ⊢ ( 𝜑 → ( 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 ∈ ℝ → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ) ) )
104 103 simpld ⊢ ( 𝜑 → 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) )
105 104 46 ffvelcdmd ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) )
106 105 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) )
107 eleq1 ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) )
108 107 anbi2d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) )
109 fveq2 ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
110 oveq1 ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑖 + 1 ) = ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) )
111 110 fveq2d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
112 109 111 oveq12d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
113 112 reseq2d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
114 112 oveq1d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) = ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) )
115 113 114 eleq12d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) ↔ ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) )
116 108 115 imbi12d ⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) ) ↔ ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) ) )
117 116 7 vtoclg ⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) → ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) )
118 105 106 117 sylc ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) )
119 rescncf ⊢ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) –cn→ ℂ ) ) )
120 100 118 119 sylc ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) –cn→ ℂ ) )
121 102 120 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) –cn→ ℂ ) )
122 18 121 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) –cn→ ℂ ) )
123 49 57 58 60 61 122 19 cncfshiftioo ⊢ ( 𝜑 → 𝑅 ∈ ( ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) –cn→ ℂ ) )
124 19 a1i ⊢ ( 𝜑 → 𝑅 = ( 𝑦 ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) ) )
125 17 oveq2i ⊢ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
126 125 a1i ⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
127 69 66 oveq12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
128 68 64 oveq12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
129 127 128 eqeq12d ⊢ ( 𝑗 = 𝐽 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
130 63 129 imbi12d ⊢ ( 𝑗 = 𝐽 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) ) )
131 85 fveq2i ⊢ ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
132 131 oveq1i ⊢ ( ( ♯ ‘ 𝐻 ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
133 12 132 eqtri ⊢ 𝑁 = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
134 isoeq5 ⊢ ( 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) → ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ) )
135 85 134 ax-mp ⊢ ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
136 135 iotabii ⊢ ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
137 13 136 eqtri ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
138 eqid ⊢ ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
139 1 2 3 4 8 9 10 133 137 14 15 138 fourierdlem65 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
140 130 139 vtoclg ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
141 140 anabsi7 ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
142 16 141 mpdan ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
143 57 recnd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
144 55 recnd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℂ )
145 8 29 iccssred ⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℝ )
146 ax-resscn ⊢ ℝ ⊆ ℂ
147 145 146 sstrdi ⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℂ )
148 10 37 36 fourierdlem15 ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐶 [,] 𝐷 ) )
149 148 45 ffvelcdmd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ( 𝐶 [,] 𝐷 ) )
150 147 149 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℂ )
151 144 150 subcld ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ∈ ℂ )
152 49 recnd ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℂ )
153 143 151 152 subsub23d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
154 142 153 mpbird ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
155 154 eqcomd ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
156 155 oveq1d ⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
157 143 151 subcld ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℂ )
158 157 144 143 addsub12d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
159 143 151 143 sub32d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
160 143 subidd ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = 0 )
161 160 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
162 df-neg ⊢ - ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) = ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
163 144 150 negsubdi2d ⊢ ( 𝜑 → - ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
164 162 163 eqtr3id ⊢ ( 𝜑 → ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
165 159 161 164 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
166 165 oveq2d ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
167 144 150 pncan3d ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑆 ‘ 𝐽 ) )
168 158 166 167 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝑆 ‘ 𝐽 ) )
169 126 156 168 3eqtrd ⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( 𝑆 ‘ 𝐽 ) )
170 17 oveq2i ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
171 143 144 pncan3d ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
172 170 171 eqtrid ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
173 169 172 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) = ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
174 173 mpteq1d ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) ) = ( 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) ) )
175 5 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) )
176 175 reseq1d ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
177 ioossre ⊢ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ℝ
178 177 a1i ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ℝ )
179 178 resmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) )
180 18 fveq1i ⊢ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) = ( ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑦 − 𝑈 ) )
181 180 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) = ( ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑦 − 𝑈 ) ) )
182 49 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
183 182 rexrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ* )
184 57 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
185 184 rexrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ* )
186 178 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 ∈ ℝ )
187 60 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑈 ∈ ℝ )
188 186 187 resubcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − 𝑈 ) ∈ ℝ )
189 46 rexrd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ* )
190 189 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ 𝐽 ) ∈ ℝ* )
191 55 rexrd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
192 191 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
193 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
194 ioogtlb ⊢ ( ( ( 𝑆 ‘ 𝐽 ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ 𝐽 ) < 𝑦 )
195 190 192 193 194 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ 𝐽 ) < 𝑦 )
196 169 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( 𝑆 ‘ 𝐽 ) )
197 186 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 ∈ ℂ )
198 187 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑈 ∈ ℂ )
199 197 198 npcand ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑦 − 𝑈 ) + 𝑈 ) = 𝑦 )
200 195 196 199 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) < ( ( 𝑦 − 𝑈 ) + 𝑈 ) )
201 182 188 187 ltadd1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑦 − 𝑈 ) ↔ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) < ( ( 𝑦 − 𝑈 ) + 𝑈 ) ) )
202 200 201 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑦 − 𝑈 ) )
203 iooltub ⊢ ( ( ( 𝑆 ‘ 𝐽 ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
204 190 192 193 203 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
205 172 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
206 204 199 205 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑦 − 𝑈 ) + 𝑈 ) < ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) )
207 188 184 187 ltadd1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑦 − 𝑈 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↔ ( ( 𝑦 − 𝑈 ) + 𝑈 ) < ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) )
208 206 207 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − 𝑈 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
209 183 185 188 202 208 eliood ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − 𝑈 ) ∈ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
210 fvres ⊢ ( ( 𝑦 − 𝑈 ) ∈ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑦 − 𝑈 ) ) = ( 𝐹 ‘ ( 𝑦 − 𝑈 ) ) )
211 209 210 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑦 − 𝑈 ) ) = ( 𝐹 ‘ ( 𝑦 − 𝑈 ) ) )
212 17 oveq2i ⊢ ( 𝑦 − 𝑈 ) = ( 𝑦 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
213 212 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − 𝑈 ) = ( 𝑦 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
214 144 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℂ )
215 143 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
216 197 214 215 subsub2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝑦 + ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
217 215 214 subcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
218 23 22 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
219 2 218 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
220 219 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
221 220 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑇 ∈ ℂ )
222 22 23 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
223 25 222 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
224 223 2 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑇 )
225 224 gt0ne0d ⊢ ( 𝜑 → 𝑇 ≠ 0 )
226 225 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑇 ≠ 0 )
227 217 221 226 divcan1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
228 227 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) )
229 228 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 + ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑦 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) ) )
230 213 216 229 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − 𝑈 ) = ( 𝑦 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) ) )
231 230 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑦 − 𝑈 ) ) = ( 𝐹 ‘ ( 𝑦 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) ) ) )
232 5 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝐹 : ℝ ⟶ ℂ )
233 219 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑇 ∈ ℝ )
234 14 a1i ⊢ ( 𝜑 → 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
235 id ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
236 oveq2 ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( 𝐵 − 𝑥 ) = ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
237 236 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) )
238 237 fveq2d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
239 238 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
240 235 239 oveq12d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
241 240 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
242 23 55 resubcld ⊢ ( 𝜑 → ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
243 242 219 225 redivcld ⊢ ( 𝜑 → ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℝ )
244 243 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℤ )
245 244 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ )
246 245 219 remulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
247 55 246 readdcld ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
248 234 241 55 247 fvmptd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
249 248 oveq1d ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
250 245 recnd ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℂ )
251 250 220 mulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
252 144 251 pncan2d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
253 249 252 eqtrd ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
254 253 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) )
255 250 220 225 divcan4d ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
256 254 255 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
257 256 244 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℤ )
258 257 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℤ )
259 6 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
260 232 233 258 186 259 fperiodmul ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑦 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
261 231 260 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑦 − 𝑈 ) ) = ( 𝐹 ‘ 𝑦 ) )
262 181 211 261 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) )
263 262 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) = ( 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) ) )
264 176 179 263 3eqtrrd ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) ) = ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
265 124 174 264 3eqtrd ⊢ ( 𝜑 → 𝑅 = ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
266 173 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) –cn→ ℂ ) = ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) –cn→ ℂ ) )
267 123 265 266 3eltr3d ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) –cn→ ℂ ) )