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

Metamath Proof Explorer

Theorem fourierdlem75

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

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

Proof

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