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