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