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 ffvelrnd ( ( 𝜑𝑖 ∈ ( 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 62 tgioo2 ( 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 ffvelrnda ( ( 𝜑𝑖 ∈ ( 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 ffvelrnd ( ( 𝜑𝑖 ∈ ( 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 ffvelrnd ( ( 𝜑𝑠 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 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 ( 𝑄𝑖 ) ) )