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

Metamath Proof Explorer

Theorem fourierdlem74

Description: Given a piecewise smooth function F , the derived function H has a limit at the upper bound of each interval of the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem74.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem74.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem74.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem74.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝑉 )
fourierdlem74.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
fourierdlem74.w ⊢ ( 𝜑 → 𝑊 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
fourierdlem74.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
fourierdlem74.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem74.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem74.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
fourierdlem74.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
fourierdlem74.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem74.g ⊢ 𝐺 = ( ℝ D 𝐹 )
fourierdlem74.gcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
fourierdlem74.e ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
fourierdlem74.a ⊢ 𝐴 = if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
Assertion fourierdlem74 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴 ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem74.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2 fourierdlem74.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
3 fourierdlem74.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
4 fourierdlem74.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝑉 )
5 fourierdlem74.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
6 fourierdlem74.w ⊢ ( 𝜑 → 𝑊 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
7 fourierdlem74.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
8 fourierdlem74.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
9 fourierdlem74.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
10 fourierdlem74.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
11 fourierdlem74.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
12 fourierdlem74.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
13 fourierdlem74.g ⊢ 𝐺 = ( ℝ D 𝐹 )
14 fourierdlem74.gcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
15 fourierdlem74.e ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
16 fourierdlem74.a ⊢ 𝐴 = if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
17 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
18 pire ⊢ π ∈ ℝ
19 18 renegcli ⊢ - π ∈ ℝ
20 19 a1i ⊢ ( 𝜑 → - π ∈ ℝ )
21 20 1 readdcld ⊢ ( 𝜑 → ( - π + 𝑋 ) ∈ ℝ )
22 18 a1i ⊢ ( 𝜑 → π ∈ ℝ )
23 22 1 readdcld ⊢ ( 𝜑 → ( π + 𝑋 ) ∈ ℝ )
24 21 23 iccssred ⊢ ( 𝜑 → ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ⊆ ℝ )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ⊆ ℝ )
26 2 8 9 fourierdlem15 ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
27 26 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
28 25 27 sseldd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
29 17 28 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
30 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
31 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝑋 ∈ ℝ )
32 2 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
33 8 32 syl ⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
34 9 33 mpbid ⊢ ( 𝜑 → ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
35 34 simprrd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
36 35 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
37 36 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
38 eqcom ⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ↔ 𝑋 = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
39 38 biimpi ⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → 𝑋 = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
40 39 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝑋 = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
41 37 40 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑉 ‘ 𝑖 ) < 𝑋 )
42 ioossre ⊢ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⊆ ℝ
43 42 a1i ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⊆ ℝ )
44 3 43 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ )
45 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ )
46 limcresi ⊢ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ⊆ ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 )
47 46 6 sselid ⊢ ( 𝜑 → 𝑊 ∈ ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑊 ∈ ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) )
49 mnfxr ⊢ -∞ ∈ ℝ*
50 49 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → -∞ ∈ ℝ* )
51 29 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
52 29 mnfltd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → -∞ < ( 𝑉 ‘ 𝑖 ) )
53 50 51 52 xrltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → -∞ ≤ ( 𝑉 ‘ 𝑖 ) )
54 iooss1 ⊢ ( ( -∞ ∈ ℝ* ∧ -∞ ≤ ( 𝑉 ‘ 𝑖 ) ) → ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⊆ ( -∞ (,) 𝑋 ) )
55 50 53 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⊆ ( -∞ (,) 𝑋 ) )
56 55 resabs1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) )
57 56 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) )
58 48 57 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑊 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) )
59 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝑊 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) )
60 eqid ⊢ ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) )
61 ax-resscn ⊢ ℝ ⊆ ℂ
62 61 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
63 3 62 fssd ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
64 ssid ⊢ ℝ ⊆ ℝ
65 64 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ )
66 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
67 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
68 66 67 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) )
69 62 63 65 43 68 syl22anc ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) )
70 13 eqcomi ⊢ ( ℝ D 𝐹 ) = 𝐺
71 ioontr ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 )
72 70 71 reseq12i ⊢ ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) )
73 72 a1i ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) )
74 69 73 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) )
75 74 dmeqd ⊢ ( 𝜑 → dom ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = dom ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) )
76 75 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = dom ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) )
77 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
78 oveq2 ⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) )
79 78 reseq2d ⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) )
80 79 78 feq12d ⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ ↔ ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ ) )
81 80 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ ↔ ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ ) )
82 77 81 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ )
83 fdm ⊢ ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ → dom ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) )
84 82 83 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → dom ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) )
85 76 84 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) )
86 limcresi ⊢ ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ⊆ ( ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 )
87 55 resabs1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) )
88 87 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) = ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) )
89 86 88 sseqtrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ⊆ ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) )
90 15 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐸 ∈ ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
91 89 90 sseldd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐸 ∈ ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) )
92 69 73 eqtr2d ⊢ ( 𝜑 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) )
93 92 oveq1d ⊢ ( 𝜑 → ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) = ( ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) limℂ 𝑋 ) )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) = ( ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) limℂ 𝑋 ) )
95 91 94 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐸 ∈ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) limℂ 𝑋 ) )
96 95 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐸 ∈ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) limℂ 𝑋 ) )
97 eqid ⊢ ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) = ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) )
98 oveq2 ⊢ ( 𝑥 = 𝑠 → ( 𝑋 + 𝑥 ) = ( 𝑋 + 𝑠 ) )
99 98 fveq2d ⊢ ( 𝑥 = 𝑠 → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑥 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) )
100 99 oveq1d ⊢ ( 𝑥 = 𝑠 → ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑥 ) ) − 𝑊 ) = ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) )
101 100 cbvmptv ⊢ ( 𝑥 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑥 ) ) − 𝑊 ) ) = ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) )
102 id ⊢ ( 𝑥 = 𝑠 → 𝑥 = 𝑠 )
103 102 cbvmptv ⊢ ( 𝑥 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ 𝑥 ) = ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ 𝑠 )
104 30 31 41 45 59 60 85 96 97 101 103 fourierdlem60 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐸 ∈ ( ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) limℂ 0 ) )
105 iftrue ⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = 𝐸 )
106 16 105 eqtrid ⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → 𝐴 = 𝐸 )
107 106 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐴 = 𝐸 )
108 7 reseq1i ⊢ ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
109 108 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
110 ioossicc ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
111 19 rexri ⊢ - π ∈ ℝ*
112 111 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → - π ∈ ℝ* )
113 18 rexri ⊢ π ∈ ℝ*
114 113 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → π ∈ ℝ* )
115 19 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → - π ∈ ℝ )
116 18 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → π ∈ ℝ )
117 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ℝ )
118 28 117 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ )
119 20 recnd ⊢ ( 𝜑 → - π ∈ ℂ )
120 1 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
121 119 120 pncand ⊢ ( 𝜑 → ( ( - π + 𝑋 ) − 𝑋 ) = - π )
122 121 eqcomd ⊢ ( 𝜑 → - π = ( ( - π + 𝑋 ) − 𝑋 ) )
123 122 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → - π = ( ( - π + 𝑋 ) − 𝑋 ) )
124 21 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( - π + 𝑋 ) ∈ ℝ )
125 23 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( π + 𝑋 ) ∈ ℝ )
126 elicc2 ⊢ ( ( ( - π + 𝑋 ) ∈ ℝ ∧ ( π + 𝑋 ) ∈ ℝ ) → ( ( 𝑉 ‘ 𝑖 ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ↔ ( ( 𝑉 ‘ 𝑖 ) ∈ ℝ ∧ ( - π + 𝑋 ) ≤ ( 𝑉 ‘ 𝑖 ) ∧ ( 𝑉 ‘ 𝑖 ) ≤ ( π + 𝑋 ) ) ) )
127 124 125 126 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ↔ ( ( 𝑉 ‘ 𝑖 ) ∈ ℝ ∧ ( - π + 𝑋 ) ≤ ( 𝑉 ‘ 𝑖 ) ∧ ( 𝑉 ‘ 𝑖 ) ≤ ( π + 𝑋 ) ) ) )
128 27 127 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) ∈ ℝ ∧ ( - π + 𝑋 ) ≤ ( 𝑉 ‘ 𝑖 ) ∧ ( 𝑉 ‘ 𝑖 ) ≤ ( π + 𝑋 ) ) )
129 128 simp2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( - π + 𝑋 ) ≤ ( 𝑉 ‘ 𝑖 ) )
130 124 28 117 129 lesub1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( - π + 𝑋 ) − 𝑋 ) ≤ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
131 123 130 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → - π ≤ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
132 128 simp3d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ≤ ( π + 𝑋 ) )
133 28 125 117 132 lesub1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ≤ ( ( π + 𝑋 ) − 𝑋 ) )
134 116 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → π ∈ ℂ )
135 120 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ℂ )
136 134 135 pncand ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( π + 𝑋 ) − 𝑋 ) = π )
137 133 136 breqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ≤ π )
138 115 116 118 131 137 eliccd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ( - π [,] π ) )
139 138 11 fmptd ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
140 139 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
141 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
142 112 114 140 141 fourierdlem8 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
143 110 142 sstrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
144 143 resmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) )
145 144 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) )
146 17 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
147 17 118 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ )
148 11 fvmpt2 ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
149 146 147 148 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
150 149 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
151 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑗 ) )
152 151 oveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
153 152 cbvmptv ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
154 11 153 eqtri ⊢ 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
155 154 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) )
156 fveq2 ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑉 ‘ 𝑗 ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
157 156 oveq1d ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
158 157 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
159 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
160 159 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
161 34 simpld ⊢ ( 𝜑 → 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
162 elmapi ⊢ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
163 161 162 syl ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
164 163 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
165 164 160 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
166 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ )
167 165 166 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ )
168 155 158 160 167 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
169 168 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
170 oveq1 ⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) = ( 𝑋 − 𝑋 ) )
171 170 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) = ( 𝑋 − 𝑋 ) )
172 120 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝑋 ∈ ℂ )
173 172 subidd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑋 − 𝑋 ) = 0 )
174 17 173 sylanl2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑋 − 𝑋 ) = 0 )
175 169 171 174 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = 0 )
176 150 175 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) )
177 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 0 ) → 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
178 8 adantr ⊢ ( ( 𝜑 ∧ 𝑠 = 0 ) → 𝑀 ∈ ℕ )
179 20 22 1 2 12 8 9 11 fourierdlem14 ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) )
180 179 adantr ⊢ ( ( 𝜑 ∧ 𝑠 = 0 ) → 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) )
181 simpr ⊢ ( ( 𝜑 ∧ 𝑠 = 0 ) → 𝑠 = 0 )
182 ffn ⊢ ( 𝑉 : ( 0 ... 𝑀 ) ⟶ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) → 𝑉 Fn ( 0 ... 𝑀 ) )
183 fvelrnb ⊢ ( 𝑉 Fn ( 0 ... 𝑀 ) → ( 𝑋 ∈ ran 𝑉 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑉 ‘ 𝑖 ) = 𝑋 ) )
184 26 182 183 3syl ⊢ ( 𝜑 → ( 𝑋 ∈ ran 𝑉 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑉 ‘ 𝑖 ) = 𝑋 ) )
185 4 184 mpbid ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑉 ‘ 𝑖 ) = 𝑋 )
186 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
187 11 fvmpt2 ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ( - π [,] π ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
188 186 138 187 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
189 188 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) = 𝑋 ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
190 oveq1 ⊢ ( ( 𝑉 ‘ 𝑖 ) = 𝑋 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( 𝑋 − 𝑋 ) )
191 190 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) = 𝑋 ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( 𝑋 − 𝑋 ) )
192 120 subidd ⊢ ( 𝜑 → ( 𝑋 − 𝑋 ) = 0 )
193 192 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) = 𝑋 ) → ( 𝑋 − 𝑋 ) = 0 )
194 189 191 193 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) = 𝑋 ) → ( 𝑄 ‘ 𝑖 ) = 0 )
195 194 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) = 𝑋 → ( 𝑄 ‘ 𝑖 ) = 0 ) )
196 195 reximdva ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑉 ‘ 𝑖 ) = 𝑋 → ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = 0 ) )
197 185 196 mpd ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = 0 )
198 118 11 fmptd ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
199 ffn ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ → 𝑄 Fn ( 0 ... 𝑀 ) )
200 fvelrnb ⊢ ( 𝑄 Fn ( 0 ... 𝑀 ) → ( 0 ∈ ran 𝑄 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = 0 ) )
201 198 199 200 3syl ⊢ ( 𝜑 → ( 0 ∈ ran 𝑄 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = 0 ) )
202 197 201 mpbird ⊢ ( 𝜑 → 0 ∈ ran 𝑄 )
203 202 adantr ⊢ ( ( 𝜑 ∧ 𝑠 = 0 ) → 0 ∈ ran 𝑄 )
204 181 203 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑠 = 0 ) → 𝑠 ∈ ran 𝑄 )
205 12 178 180 204 fourierdlem12 ⊢ ( ( ( 𝜑 ∧ 𝑠 = 0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
206 205 an32s ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 = 0 ) → ¬ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
207 206 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 0 ) → ¬ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
208 177 207 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑠 = 0 )
209 208 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑠 = 0 )
210 209 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) )
211 elioore ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ )
212 211 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
213 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 ∈ ℝ )
214 elioo3g ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ℝ* ) ∧ ( ( 𝑄 ‘ 𝑖 ) < 𝑠 ∧ 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
215 214 biimpi ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ℝ* ) ∧ ( ( 𝑄 ‘ 𝑖 ) < 𝑠 ∧ 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
216 215 simprrd ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
217 216 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
218 175 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = 0 )
219 217 218 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < 0 )
220 212 213 219 ltnsymd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 0 < 𝑠 )
221 220 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑊 )
222 221 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) )
223 222 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) )
224 51 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
225 1 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
226 225 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ* )
227 166 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
228 227 212 readdcld ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
229 120 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℂ )
230 iccssre ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
231 19 18 230 mp2an ⊢ ( - π [,] π ) ⊆ ℝ
232 231 61 sstri ⊢ ( - π [,] π ) ⊆ ℂ
233 188 138 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( - π [,] π ) )
234 17 233 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( - π [,] π ) )
235 232 234 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
236 229 235 addcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) )
237 149 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) = ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) + 𝑋 ) )
238 29 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℂ )
239 238 229 npcand ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) + 𝑋 ) = ( 𝑉 ‘ 𝑖 ) )
240 236 237 239 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) )
241 240 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) )
242 149 147 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
243 242 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
244 211 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
245 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
246 215 simprld ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 )
247 246 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 )
248 243 244 245 247 ltadd2dd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) < ( 𝑋 + 𝑠 ) )
249 241 248 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑋 + 𝑠 ) )
250 249 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑋 + 𝑠 ) )
251 ltaddneg ⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 𝑠 < 0 ↔ ( 𝑋 + 𝑠 ) < 𝑋 ) )
252 212 227 251 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 < 0 ↔ ( 𝑋 + 𝑠 ) < 𝑋 ) )
253 219 252 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < 𝑋 )
254 224 226 228 250 253 eliood ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) )
255 fvres ⊢ ( ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
256 255 eqcomd ⊢ ( ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) )
257 254 256 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) )
258 257 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) = ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) )
259 258 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) = ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) )
260 210 223 259 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) )
261 176 260 mpteq12dva ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) = ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) )
262 109 145 261 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) )
263 262 175 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) limℂ 0 ) )
264 104 107 263 3eltr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐴 ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
265 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) )
266 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑠 ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑠 )
267 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) )
268 3 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐹 : ℝ ⟶ ℝ )
269 1 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
270 211 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
271 269 270 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
272 268 271 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
273 272 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
274 273 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
275 274 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
276 5 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
277 limccl ⊢ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ⊆ ℂ
278 277 6 sselid ⊢ ( 𝜑 → 𝑊 ∈ ℂ )
279 276 278 ifcld ⊢ ( 𝜑 → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ )
280 279 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ )
281 280 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ )
282 275 281 subcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℂ )
283 211 recnd ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℂ )
284 283 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℂ )
285 velsn ⊢ ( 𝑠 ∈ { 0 } ↔ 𝑠 = 0 )
286 208 285 sylnibr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑠 ∈ { 0 } )
287 286 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑠 ∈ { 0 } )
288 284 287 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ( ℂ ∖ { 0 } ) )
289 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
290 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑊 ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑊 )
291 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) )
292 278 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑊 ∈ ℂ )
293 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : ℝ ⟶ ℝ )
294 ioossre ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
295 294 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
296 51 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
297 165 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
298 297 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
299 271 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
300 198 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
301 300 160 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
302 301 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
303 216 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
304 244 302 245 303 ltadd2dd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
305 168 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑋 + ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
306 165 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
307 229 306 pncan3d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
308 305 307 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
309 308 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
310 304 309 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
311 296 298 299 249 310 eliood ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
312 ioossre ⊢ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
313 312 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
314 244 303 ltned ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ≠ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
315 308 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) = ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
316 315 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
317 10 316 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
318 301 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
319 293 166 295 289 311 313 314 317 318 fourierdlem53 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
320 ioosscn ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
321 320 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
322 278 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑊 ∈ ℂ )
323 290 321 322 318 constlimc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑊 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑊 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
324 289 290 291 274 292 319 323 sublimc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 − 𝑊 ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
325 324 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑅 − 𝑊 ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
326 iftrue ⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) = 𝑊 )
327 326 oveq2d ⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) = ( 𝑅 − 𝑊 ) )
328 327 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) = ( 𝑅 − 𝑊 ) )
329 211 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
330 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 ∈ ℝ )
331 301 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
332 216 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
333 168 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
334 165 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
335 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 ∈ ℝ )
336 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 )
337 334 335 336 ltled ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ≤ 𝑋 )
338 334 335 suble0d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ≤ 0 ↔ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ≤ 𝑋 ) )
339 337 338 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ≤ 0 )
340 333 339 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≤ 0 )
341 340 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≤ 0 )
342 329 331 330 332 341 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < 0 )
343 329 330 342 ltnsymd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 0 < 𝑠 )
344 343 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑊 )
345 344 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) )
346 345 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) )
347 346 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
348 325 328 347 3eltr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
349 348 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
350 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝜑 )
351 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
352 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 ∈ ℝ )
353 352 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 ∈ ℝ )
354 165 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
355 354 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
356 neqne ⊢ ( ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ≠ 𝑋 )
357 356 necomd ⊢ ( ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → 𝑋 ≠ ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
358 357 adantr ⊢ ( ( ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 ≠ ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
359 358 3ad2antl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 ≠ ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
360 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 )
361 353 355 359 360 lttri5d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
362 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 0 < 𝑠 , 𝑌 , 𝑊 ) )
363 274 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
364 279 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ )
365 319 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 𝑅 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
366 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 )
367 276 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑌 ∈ ℂ )
368 366 321 367 318 constlimc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑌 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
369 368 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 𝑌 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
370 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 𝑋 ∈ ℝ )
371 165 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
372 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
373 370 371 372 ltnsymd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 )
374 373 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) = 𝑌 )
375 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 ∈ ℝ )
376 242 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
377 211 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
378 192 eqcomd ⊢ ( 𝜑 → 0 = ( 𝑋 − 𝑋 ) )
379 378 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 0 = ( 𝑋 − 𝑋 ) )
380 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
381 51 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
382 297 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
383 166 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → 𝑋 ∈ ℝ )
384 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) )
385 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
386 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → 𝑋 ∈ ℝ )
387 385 386 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( ( 𝑉 ‘ 𝑖 ) < 𝑋 ↔ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) )
388 384 387 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( 𝑉 ‘ 𝑖 ) < 𝑋 )
389 388 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( 𝑉 ‘ 𝑖 ) < 𝑋 )
390 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
391 381 382 383 389 390 eliood ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → 𝑋 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
392 2 8 9 4 fourierdlem12 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
393 392 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ¬ 𝑋 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
394 391 393 condan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) )
395 370 380 370 394 lesub1dd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑋 − 𝑋 ) ≤ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
396 379 395 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 0 ≤ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
397 149 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( 𝑄 ‘ 𝑖 ) )
398 397 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( 𝑄 ‘ 𝑖 ) )
399 396 398 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 0 ≤ ( 𝑄 ‘ 𝑖 ) )
400 399 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 ≤ ( 𝑄 ‘ 𝑖 ) )
401 246 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 )
402 375 376 377 400 401 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 < 𝑠 )
403 402 iftrued ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑌 )
404 403 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 ) )
405 404 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
406 369 374 405 3eltr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
407 289 362 265 363 364 365 406 sublimc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
408 350 351 361 407 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
409 349 408 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
410 321 266 318 idlimc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑠 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
411 410 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑠 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
412 168 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
413 306 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
414 229 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝑋 ∈ ℂ )
415 356 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ≠ 𝑋 )
416 413 414 415 subne0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ≠ 0 )
417 412 416 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≠ 0 )
418 208 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑠 = 0 )
419 418 neqned ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ≠ 0 )
420 265 266 267 282 288 409 411 417 419 divlimc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
421 iffalse ⊢ ( ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
422 16 421 eqtrid ⊢ ( ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → 𝐴 = ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
423 422 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐴 = ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
424 ioossre ⊢ ( -∞ (,) 𝑋 ) ⊆ ℝ
425 424 a1i ⊢ ( 𝜑 → ( -∞ (,) 𝑋 ) ⊆ ℝ )
426 3 425 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) : ( -∞ (,) 𝑋 ) ⟶ ℝ )
427 424 62 sstrid ⊢ ( 𝜑 → ( -∞ (,) 𝑋 ) ⊆ ℂ )
428 49 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
429 1 mnfltd ⊢ ( 𝜑 → -∞ < 𝑋 )
430 66 428 1 429 lptioo2cn ⊢ ( 𝜑 → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( -∞ (,) 𝑋 ) ) )
431 426 427 430 6 limcrecl ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
432 3 1 5 431 7 fourierdlem9 ⊢ ( 𝜑 → 𝐻 : ( - π [,] π ) ⟶ ℝ )
433 432 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐻 : ( - π [,] π ) ⟶ ℝ )
434 433 143 feqresmpt ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
435 143 sselda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ( - π [,] π ) )
436 0cnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 ∈ ℂ )
437 279 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ )
438 274 437 subcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℂ )
439 283 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℂ )
440 208 neqned ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ≠ 0 )
441 438 439 440 divcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ∈ ℂ )
442 436 441 ifcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ∈ ℂ )
443 7 fvmpt2 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ∈ ℂ ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
444 435 442 443 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
445 208 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) )
446 444 445 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) )
447 446 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
448 434 447 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
449 448 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
450 449 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
451 420 423 450 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐴 ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
452 451 3expa ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐴 ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
453 264 452 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴 ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )