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

Metamath Proof Explorer

Theorem fourierdlem76

Description: Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem76.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem76.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem76.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem76.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem76.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem76.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem76.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
fourierdlem76.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
fourierdlem76.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem76.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem76.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem76.ab ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
fourierdlem76.n0 ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
fourierdlem76.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem76.o ⊢ 𝑂 = ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
fourierdlem76.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
fourierdlem76.t ⊢ 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
fourierdlem76.n ⊢ 𝑁 = ( ( ♯ ‘ 𝑇 ) − 1 )
fourierdlem76.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
fourierdlem76.d ⊢ 𝐷 = ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) )
fourierdlem76.e ⊢ 𝐸 = ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) )
fourierdlem76.ch ⊢ ( 𝜒 ↔ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
Assertion fourierdlem76 ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝐸 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem76.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem76.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3 fourierdlem76.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
4 fourierdlem76.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5 fourierdlem76.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
6 fourierdlem76.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
7 fourierdlem76.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
8 fourierdlem76.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
9 fourierdlem76.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
10 fourierdlem76.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
11 fourierdlem76.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
12 fourierdlem76.ab ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
13 fourierdlem76.n0 ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
14 fourierdlem76.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
15 fourierdlem76.o ⊢ 𝑂 = ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
16 fourierdlem76.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
17 fourierdlem76.t ⊢ 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
18 fourierdlem76.n ⊢ 𝑁 = ( ( ♯ ‘ 𝑇 ) − 1 )
19 fourierdlem76.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
20 fourierdlem76.d ⊢ 𝐷 = ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) )
21 fourierdlem76.e ⊢ 𝐸 = ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) )
22 fourierdlem76.ch ⊢ ( 𝜒 ↔ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
23 eqid ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) )
24 eqid ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
25 eqid ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
26 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝜑 )
27 22 26 sylbi ⊢ ( 𝜒 → 𝜑 )
28 27 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝜑 )
29 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
30 9 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
31 27 30 syl ⊢ ( 𝜒 → 𝐴 ∈ ℝ* )
32 31 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐴 ∈ ℝ* )
33 10 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
34 27 33 syl ⊢ ( 𝜒 → 𝐵 ∈ ℝ* )
35 34 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐵 ∈ ℝ* )
36 elioore ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑠 ∈ ℝ )
37 36 adantl ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
38 27 9 syl ⊢ ( 𝜒 → 𝐴 ∈ ℝ )
39 38 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐴 ∈ ℝ )
40 prfi ⊢ { 𝐴 , 𝐵 } ∈ Fin
41 40 a1i ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ Fin )
42 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
43 16 rnmptfi ⊢ ( ( 0 ... 𝑀 ) ∈ Fin → ran 𝑄 ∈ Fin )
44 infi ⊢ ( ran 𝑄 ∈ Fin → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ∈ Fin )
45 42 43 44 3syl ⊢ ( 𝜑 → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ∈ Fin )
46 unfi ⊢ ( ( { 𝐴 , 𝐵 } ∈ Fin ∧ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ∈ Fin ) → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ∈ Fin )
47 41 45 46 syl2anc ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ∈ Fin )
48 17 47 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ Fin )
49 prssg ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ↔ { 𝐴 , 𝐵 } ⊆ ℝ ) )
50 9 10 49 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ↔ { 𝐴 , 𝐵 } ⊆ ℝ ) )
51 9 10 50 mpbi2and ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ℝ )
52 inss2 ⊢ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 (,) 𝐵 )
53 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
54 52 53 sstri ⊢ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ℝ
55 54 a1i ⊢ ( 𝜑 → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ℝ )
56 51 55 unssd ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ⊆ ℝ )
57 17 56 eqsstrid ⊢ ( 𝜑 → 𝑇 ⊆ ℝ )
58 48 57 19 18 fourierdlem36 ⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
59 27 58 syl ⊢ ( 𝜒 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
60 isof1o ⊢ ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 )
61 f1of ⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
62 59 60 61 3syl ⊢ ( 𝜒 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
63 27 57 syl ⊢ ( 𝜒 → 𝑇 ⊆ ℝ )
64 62 63 fssd ⊢ ( 𝜒 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
65 64 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
66 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
67 22 66 sylbi ⊢ ( 𝜒 → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
68 elfzofz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
69 67 68 syl ⊢ ( 𝜒 → 𝑗 ∈ ( 0 ... 𝑁 ) )
70 69 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
71 65 70 ffvelcdmd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
72 58 60 61 3syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
73 frn ⊢ ( 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 → ran 𝑆 ⊆ 𝑇 )
74 72 73 syl ⊢ ( 𝜑 → ran 𝑆 ⊆ 𝑇 )
75 9 leidd ⊢ ( 𝜑 → 𝐴 ≤ 𝐴 )
76 9 10 11 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
77 9 10 9 75 76 eliccd ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
78 10 leidd ⊢ ( 𝜑 → 𝐵 ≤ 𝐵 )
79 9 10 10 76 78 eliccd ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
80 prssg ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) ) )
81 9 10 80 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) ) )
82 77 79 81 mpbi2and ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) )
83 52 29 sstri ⊢ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 )
84 83 a1i ⊢ ( 𝜑 → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
85 82 84 unssd ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
86 17 85 eqsstrid ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐴 [,] 𝐵 ) )
87 74 86 sstrd ⊢ ( 𝜑 → ran 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) )
88 27 87 syl ⊢ ( 𝜒 → ran 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) )
89 ffun ⊢ ( 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ → Fun 𝑆 )
90 64 89 syl ⊢ ( 𝜒 → Fun 𝑆 )
91 fdm ⊢ ( 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ → dom 𝑆 = ( 0 ... 𝑁 ) )
92 64 91 syl ⊢ ( 𝜒 → dom 𝑆 = ( 0 ... 𝑁 ) )
93 92 eqcomd ⊢ ( 𝜒 → ( 0 ... 𝑁 ) = dom 𝑆 )
94 69 93 eleqtrd ⊢ ( 𝜒 → 𝑗 ∈ dom 𝑆 )
95 fvelrn ⊢ ( ( Fun 𝑆 ∧ 𝑗 ∈ dom 𝑆 ) → ( 𝑆 ‘ 𝑗 ) ∈ ran 𝑆 )
96 90 94 95 syl2anc ⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ran 𝑆 )
97 88 96 sseldd ⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) )
98 iccgelb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 𝑆 ‘ 𝑗 ) )
99 31 34 97 98 syl3anc ⊢ ( 𝜒 → 𝐴 ≤ ( 𝑆 ‘ 𝑗 ) )
100 99 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐴 ≤ ( 𝑆 ‘ 𝑗 ) )
101 71 rexrd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ* )
102 fzofzp1 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
103 67 102 syl ⊢ ( 𝜒 → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
104 64 103 ffvelcdmd ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
105 104 rexrd ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
106 105 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
107 simpr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
108 ioogtlb ⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑗 ) < 𝑠 )
109 101 106 107 108 syl3anc ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑗 ) < 𝑠 )
110 39 71 37 100 109 lelttrd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐴 < 𝑠 )
111 104 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
112 27 10 syl ⊢ ( 𝜒 → 𝐵 ∈ ℝ )
113 112 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐵 ∈ ℝ )
114 iooltub ⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
115 101 106 107 114 syl3anc ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
116 103 93 eleqtrd ⊢ ( 𝜒 → ( 𝑗 + 1 ) ∈ dom 𝑆 )
117 fvelrn ⊢ ( ( Fun 𝑆 ∧ ( 𝑗 + 1 ) ∈ dom 𝑆 ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ran 𝑆 )
118 90 116 117 syl2anc ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ran 𝑆 )
119 88 118 sseldd ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
120 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐵 )
121 31 34 119 120 syl3anc ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐵 )
122 121 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐵 )
123 37 111 113 115 122 ltletrd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 < 𝐵 )
124 32 35 37 110 123 eliood ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( 𝐴 (,) 𝐵 ) )
125 29 124 sselid ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
126 1 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐹 : ℝ ⟶ ℝ )
127 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑋 ∈ ℝ )
128 9 10 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
129 128 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ∈ ℝ )
130 127 129 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
131 126 130 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
132 28 125 131 syl2anc ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
133 132 recnd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
134 14 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
135 27 134 syl ⊢ ( 𝜒 → 𝐶 ∈ ℂ )
136 135 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐶 ∈ ℂ )
137 133 136 subcld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℂ )
138 ioossre ⊢ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ℝ
139 138 a1i ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ℝ )
140 139 sselda ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
141 140 recnd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ℂ )
142 nne ⊢ ( ¬ 𝑠 ≠ 0 ↔ 𝑠 = 0 )
143 142 biimpi ⊢ ( ¬ 𝑠 ≠ 0 → 𝑠 = 0 )
144 143 eqcomd ⊢ ( ¬ 𝑠 ≠ 0 → 0 = 𝑠 )
145 144 adantl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → 0 = 𝑠 )
146 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
147 146 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
148 145 147 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → 0 ∈ ( 𝐴 [,] 𝐵 ) )
149 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
150 148 149 condan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ≠ 0 )
151 28 125 150 syl2anc ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ≠ 0 )
152 137 141 151 divcld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ∈ ℂ )
153 2cnd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 2 ∈ ℂ )
154 141 halfcld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑠 / 2 ) ∈ ℂ )
155 154 sincld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
156 153 155 mulcld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
157 36 recnd ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑠 ∈ ℂ )
158 157 adantl ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ℂ )
159 158 halfcld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑠 / 2 ) ∈ ℂ )
160 159 sincld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
161 2ne0 ⊢ 2 ≠ 0
162 161 a1i ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 2 ≠ 0 )
163 27 12 syl ⊢ ( 𝜒 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
164 163 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
165 164 125 sseldd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( - π [,] π ) )
166 fourierdlem44 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 ≠ 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
167 165 151 166 syl2anc ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
168 153 160 162 167 mulne0d ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
169 141 156 168 divcld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℂ )
170 eqid ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) )
171 eqid ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 )
172 151 neneqd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ¬ 𝑠 = 0 )
173 velsn ⊢ ( 𝑠 ∈ { 0 } ↔ 𝑠 = 0 )
174 172 173 sylnibr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ¬ 𝑠 ∈ { 0 } )
175 141 174 eldifd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( ℂ ∖ { 0 } ) )
176 eqid ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
177 eqid ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝐶 ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝐶 )
178 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
179 178 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
180 pire ⊢ π ∈ ℝ
181 180 renegcli ⊢ - π ∈ ℝ
182 181 a1i ⊢ ( 𝜑 → - π ∈ ℝ )
183 182 2 readdcld ⊢ ( 𝜑 → ( - π + 𝑋 ) ∈ ℝ )
184 180 a1i ⊢ ( 𝜑 → π ∈ ℝ )
185 184 2 readdcld ⊢ ( 𝜑 → ( π + 𝑋 ) ∈ ℝ )
186 183 185 iccssred ⊢ ( 𝜑 → ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ⊆ ℝ )
187 186 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ⊆ ℝ )
188 3 4 5 fourierdlem15 ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
189 188 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
190 189 179 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
191 187 190 sseldd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
192 2 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ )
193 191 192 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ )
194 16 fvmpt2 ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
195 179 193 194 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
196 195 193 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
197 196 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
198 197 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
199 22 198 sylbi ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
200 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑗 ) )
201 200 oveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
202 201 cbvmptv ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
203 16 202 eqtri ⊢ 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
204 203 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) )
205 fveq2 ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑉 ‘ 𝑗 ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
206 205 oveq1d ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
207 206 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
208 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
209 208 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
210 189 209 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
211 187 210 sseldd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
212 211 192 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ )
213 204 207 209 212 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
214 213 212 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
215 214 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
216 215 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
217 22 216 sylbi ⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
218 3 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
219 4 218 syl ⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
220 5 219 mpbid ⊢ ( 𝜑 → ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
221 220 simprrd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
222 221 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
223 191 211 192 222 ltsub1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) < ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
224 223 195 213 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
225 224 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
226 225 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
227 22 226 sylbi ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
228 22 biimpi ⊢ ( 𝜒 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
229 228 simplrd ⊢ ( 𝜒 → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
230 27 229 191 syl2anc ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
231 230 rexrd ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
232 231 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
233 27 229 211 syl2anc ⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
234 233 rexrd ⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
235 234 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
236 27 2 syl ⊢ ( 𝜒 → 𝑋 ∈ ℝ )
237 236 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
238 elioore ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ )
239 238 adantl ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
240 237 239 readdcld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
241 27 229 195 syl2anc ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
242 241 oveq2d ⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) = ( 𝑋 + ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) )
243 236 recnd ⊢ ( 𝜒 → 𝑋 ∈ ℂ )
244 230 recnd ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) ∈ ℂ )
245 243 244 pncan3d ⊢ ( 𝜒 → ( 𝑋 + ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) = ( 𝑉 ‘ 𝑖 ) )
246 242 245 eqtr2d ⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) = ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) )
247 246 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) )
248 199 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
249 199 rexrd ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
250 249 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
251 217 rexrd ⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
252 251 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
253 simpr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
254 ioogtlb ⊢ ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 )
255 250 252 253 254 syl3anc ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 )
256 248 239 237 255 ltadd2dd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) < ( 𝑋 + 𝑠 ) )
257 247 256 eqbrtrd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑋 + 𝑠 ) )
258 217 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
259 iooltub ⊢ ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
260 250 252 253 259 syl3anc ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
261 239 258 237 260 ltadd2dd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
262 27 229 213 syl2anc ⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
263 262 oveq2d ⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑋 + ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
264 233 recnd ⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
265 243 264 pncan3d ⊢ ( 𝜒 → ( 𝑋 + ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
266 263 265 eqtrd ⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
267 266 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
268 261 267 breqtrd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
269 232 235 240 257 268 eliood ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
270 fvres ⊢ ( ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
271 269 270 syl ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
272 271 eqcomd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) )
273 272 mpteq2dva ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
274 ioosscn ⊢ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
275 274 a1i ⊢ ( 𝜒 → ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
276 27 229 6 syl2anc ⊢ ( 𝜒 → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
277 ioosscn ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
278 277 a1i ⊢ ( 𝜒 → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
279 275 276 278 243 269 fourierdlem23 ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
280 273 279 eqeltrd ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
281 27 1 syl ⊢ ( 𝜒 → 𝐹 : ℝ ⟶ ℝ )
282 ioossre ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
283 282 a1i ⊢ ( 𝜒 → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
284 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
285 ioossre ⊢ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
286 285 a1i ⊢ ( 𝜒 → ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
287 239 260 ltned ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ≠ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
288 27 229 8 syl2anc ⊢ ( 𝜒 → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
289 266 eqcomd ⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) = ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
290 289 oveq2d ⊢ ( 𝜒 → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
291 288 290 eleqtrd ⊢ ( 𝜒 → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
292 217 recnd ⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
293 281 236 283 284 269 286 287 291 292 fourierdlem53 ⊢ ( 𝜒 → 𝐿 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
294 64 69 ffvelcdmd ⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
295 elfzoelz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ℤ )
296 zre ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ℝ )
297 67 295 296 3syl ⊢ ( 𝜒 → 𝑗 ∈ ℝ )
298 297 ltp1d ⊢ ( 𝜒 → 𝑗 < ( 𝑗 + 1 ) )
299 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
300 59 69 103 299 syl12anc ⊢ ( 𝜒 → ( 𝑗 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
301 298 300 mpbid ⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
302 22 simprbi ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
303 eqid ⊢ if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
304 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
305 199 217 227 280 293 294 104 301 302 303 304 fourierdlem33 ⊢ ( 𝜒 → if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
306 eqidd ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) )
307 simpr ⊢ ( ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
308 307 oveq2d ⊢ ( ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑋 + 𝑠 ) = ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
309 308 fveq2d ⊢ ( ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
310 249 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
311 251 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
312 104 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
313 199 217 294 104 301 302 fourierdlem10 ⊢ ( 𝜒 → ( ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
314 313 simpld ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑆 ‘ 𝑗 ) )
315 199 294 104 314 301 lelttrd ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
316 315 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
317 217 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
318 313 simprd ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
319 318 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
320 neqne ⊢ ( ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
321 320 necomd ⊢ ( ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≠ ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
322 321 adantl ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≠ ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
323 312 317 319 322 leneltd ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
324 310 311 312 316 323 eliood ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
325 236 104 readdcld ⊢ ( 𝜒 → ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
326 281 325 ffvelcdmd ⊢ ( 𝜒 → ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ℝ )
327 326 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ℝ )
328 306 309 324 327 fvmptd ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
329 328 ifeq2da ⊢ ( 𝜒 → if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
330 302 resmptd ⊢ ( 𝜒 → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) )
331 330 oveq1d ⊢ ( 𝜒 → ( ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
332 305 329 331 3eltr3d ⊢ ( 𝜒 → if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
333 ax-resscn ⊢ ℝ ⊆ ℂ
334 139 333 sstrdi ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ℂ )
335 104 recnd ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
336 177 334 135 335 constlimc ⊢ ( 𝜒 → 𝐶 ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝐶 ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
337 176 177 170 133 136 332 336 sublimc ⊢ ( 𝜒 → ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
338 334 171 335 idlimc ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
339 27 119 jca ⊢ ( 𝜒 → ( 𝜑 ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
340 eleq1 ⊢ ( 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
341 340 anbi2d ⊢ ( 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑 ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
342 neeq1 ⊢ ( 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( 𝑠 ≠ 0 ↔ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ 0 ) )
343 341 342 imbi12d ⊢ ( 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ 0 ) ) )
344 343 150 vtoclg ⊢ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ → ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ 0 ) )
345 104 339 344 sylc ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ 0 )
346 170 171 23 137 175 337 338 345 151 divlimc ⊢ ( 𝜒 → ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
347 eqid ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
348 153 160 mulcld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
349 168 neneqd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ¬ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 )
350 2re ⊢ 2 ∈ ℝ
351 350 a1i ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 2 ∈ ℝ )
352 36 rehalfcld ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑠 / 2 ) ∈ ℝ )
353 352 resincld ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
354 353 adantl ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
355 351 354 remulcld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ )
356 elsng ⊢ ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } ↔ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 ) )
357 355 356 syl ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } ↔ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 ) )
358 349 357 mtbird ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ¬ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } )
359 348 358 eldifd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ( ℂ ∖ { 0 } ) )
360 eqid ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 )
361 eqid ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) )
362 2cnd ⊢ ( 𝜒 → 2 ∈ ℂ )
363 360 334 362 335 constlimc ⊢ ( 𝜒 → 2 ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
364 352 ad2antrl ⊢ ( ( 𝜒 ∧ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( 𝑠 / 2 ) ≠ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) → ( 𝑠 / 2 ) ∈ ℝ )
365 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
366 365 sincld ⊢ ( 𝑥 ∈ ℝ → ( sin ‘ 𝑥 ) ∈ ℂ )
367 366 adantl ⊢ ( ( 𝜒 ∧ 𝑥 ∈ ℝ ) → ( sin ‘ 𝑥 ) ∈ ℂ )
368 eqid ⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / 2 ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / 2 ) )
369 2cn ⊢ 2 ∈ ℂ
370 eldifsn ⊢ ( 2 ∈ ( ℂ ∖ { 0 } ) ↔ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
371 369 161 370 mpbir2an ⊢ 2 ∈ ( ℂ ∖ { 0 } )
372 371 a1i ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 2 ∈ ( ℂ ∖ { 0 } ) )
373 161 a1i ⊢ ( 𝜒 → 2 ≠ 0 )
374 171 360 368 158 372 338 363 373 162 divlimc ⊢ ( 𝜒 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / 2 ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
375 sinf ⊢ sin : ℂ ⟶ ℂ
376 375 a1i ⊢ ( ⊤ → sin : ℂ ⟶ ℂ )
377 333 a1i ⊢ ( ⊤ → ℝ ⊆ ℂ )
378 376 377 feqresmpt ⊢ ( ⊤ → ( sin ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) ) )
379 378 mptru ⊢ ( sin ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) )
380 resincncf ⊢ ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ )
381 379 380 eqeltrri ⊢ ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) ) ∈ ( ℝ –cn→ ℝ )
382 381 a1i ⊢ ( 𝜒 → ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) ) ∈ ( ℝ –cn→ ℝ ) )
383 104 rehalfcld ⊢ ( 𝜒 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ∈ ℝ )
384 fveq2 ⊢ ( 𝑥 = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) → ( sin ‘ 𝑥 ) = ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) )
385 382 383 384 cnmptlimc ⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ∈ ( ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) ) limℂ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) )
386 fveq2 ⊢ ( 𝑥 = ( 𝑠 / 2 ) → ( sin ‘ 𝑥 ) = ( sin ‘ ( 𝑠 / 2 ) ) )
387 fveq2 ⊢ ( ( 𝑠 / 2 ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) → ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) )
388 387 ad2antll ⊢ ( ( 𝜒 ∧ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( 𝑠 / 2 ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) )
389 364 367 374 385 386 388 limcco ⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
390 360 361 347 153 160 363 389 mullimc ⊢ ( 𝜒 → ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
391 335 halfcld ⊢ ( 𝜒 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ∈ ℂ )
392 391 sincld ⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ∈ ℂ )
393 163 119 sseldd ⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( - π [,] π ) )
394 fourierdlem44 ⊢ ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( - π [,] π ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ 0 ) → ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ≠ 0 )
395 393 345 394 syl2anc ⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ≠ 0 )
396 362 392 373 395 mulne0d ⊢ ( 𝜒 → ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ≠ 0 )
397 171 347 24 158 359 338 390 396 168 divlimc ⊢ ( 𝜒 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
398 23 24 25 152 169 346 397 mullimc ⊢ ( 𝜒 → ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
399 20 a1i ⊢ ( 𝜒 → 𝐷 = ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) )
400 15 reseq1i ⊢ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
401 ioossicc ⊢ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
402 iccss ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐵 ) ) → ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
403 38 112 99 121 402 syl22anc ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
404 401 403 sstrid ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
405 404 resmptd ⊢ ( 𝜒 → ( ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
406 400 405 eqtrid ⊢ ( 𝜒 → ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
407 406 oveq1d ⊢ ( 𝜒 → ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
408 398 399 407 3eltr4d ⊢ ( 𝜒 → 𝐷 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
409 22 408 sylbir ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐷 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
410 248 255 gtned ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ≠ ( 𝑄 ‘ 𝑖 ) )
411 27 229 7 syl2anc ⊢ ( 𝜒 → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
412 246 oveq2d ⊢ ( 𝜒 → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) ) )
413 411 412 eleqtrd ⊢ ( 𝜒 → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) ) )
414 199 recnd ⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
415 281 236 283 284 269 286 410 413 414 fourierdlem53 ⊢ ( 𝜒 → 𝑅 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
416 eqid ⊢ if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ 𝑗 ) ) ) = if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ 𝑗 ) ) )
417 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝑄 ‘ 𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝑄 ‘ 𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
418 199 217 227 280 415 294 104 301 302 416 417 fourierdlem32 ⊢ ( 𝜒 → if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ( ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
419 eqidd ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) )
420 oveq2 ⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( 𝑋 + 𝑠 ) = ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) )
421 420 fveq2d ⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) )
422 421 adantl ⊢ ( ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) ∧ 𝑠 = ( 𝑆 ‘ 𝑗 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) )
423 249 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
424 251 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
425 294 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
426 199 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
427 314 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑆 ‘ 𝑗 ) )
428 neqne ⊢ ( ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) → ( 𝑆 ‘ 𝑗 ) ≠ ( 𝑄 ‘ 𝑖 ) )
429 428 adantl ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) ≠ ( 𝑄 ‘ 𝑖 ) )
430 426 425 427 429 leneltd ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑆 ‘ 𝑗 ) )
431 104 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
432 217 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
433 301 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
434 318 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
435 425 431 432 433 434 ltletrd ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
436 423 424 425 430 435 eliood ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
437 236 294 readdcld ⊢ ( 𝜒 → ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
438 281 437 ffvelcdmd ⊢ ( 𝜒 → ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
439 438 adantr ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
440 419 422 436 439 fvmptd ⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) )
441 440 ifeq2da ⊢ ( 𝜒 → if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ 𝑗 ) ) ) = if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) )
442 330 oveq1d ⊢ ( 𝜒 → ( ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
443 418 441 442 3eltr3d ⊢ ( 𝜒 → if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
444 294 recnd ⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ℂ )
445 177 334 135 444 constlimc ⊢ ( 𝜒 → 𝐶 ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝐶 ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
446 176 177 170 133 136 443 445 sublimc ⊢ ( 𝜒 → ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
447 334 171 444 idlimc ⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
448 27 97 jca ⊢ ( 𝜒 → ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
449 eleq1 ⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
450 449 anbi2d ⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
451 neeq1 ⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( 𝑠 ≠ 0 ↔ ( 𝑆 ‘ 𝑗 ) ≠ 0 ) )
452 450 451 imbi12d ⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ 𝑗 ) ≠ 0 ) ) )
453 452 150 vtoclg ⊢ ( ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ 𝑗 ) ≠ 0 ) )
454 97 448 453 sylc ⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ≠ 0 )
455 170 171 23 137 175 446 447 454 151 divlimc ⊢ ( 𝜒 → ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
456 360 334 362 444 constlimc ⊢ ( 𝜒 → 2 ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
457 352 ad2antrl ⊢ ( ( 𝜒 ∧ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( 𝑠 / 2 ) ≠ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) → ( 𝑠 / 2 ) ∈ ℝ )
458 171 360 368 158 372 447 456 373 162 divlimc ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) / 2 ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / 2 ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
459 294 rehalfcld ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) / 2 ) ∈ ℝ )
460 fveq2 ⊢ ( 𝑥 = ( ( 𝑆 ‘ 𝑗 ) / 2 ) → ( sin ‘ 𝑥 ) = ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) )
461 382 459 460 cnmptlimc ⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ∈ ( ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) ) limℂ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) )
462 fveq2 ⊢ ( ( 𝑠 / 2 ) = ( ( 𝑆 ‘ 𝑗 ) / 2 ) → ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) )
463 462 ad2antll ⊢ ( ( 𝜒 ∧ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( 𝑠 / 2 ) = ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) )
464 457 367 458 461 386 463 limcco ⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
465 360 361 347 153 160 456 464 mullimc ⊢ ( 𝜒 → ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
466 444 halfcld ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) / 2 ) ∈ ℂ )
467 466 sincld ⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ∈ ℂ )
468 163 97 sseldd ⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ( - π [,] π ) )
469 fourierdlem44 ⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ( - π [,] π ) ∧ ( 𝑆 ‘ 𝑗 ) ≠ 0 ) → ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ≠ 0 )
470 468 454 469 syl2anc ⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ≠ 0 )
471 362 467 373 470 mulne0d ⊢ ( 𝜒 → ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ≠ 0 )
472 171 347 24 158 359 447 465 471 168 divlimc ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
473 23 24 25 152 169 455 472 mullimc ⊢ ( 𝜒 → ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
474 21 a1i ⊢ ( 𝜒 → 𝐸 = ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) )
475 406 oveq1d ⊢ ( 𝜒 → ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
476 473 474 475 3eltr4d ⊢ ( 𝜒 → 𝐸 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
477 22 476 sylbir ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐸 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
478 302 sselda ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
479 478 272 syldan ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) )
480 479 mpteq2dva ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
481 231 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
482 234 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
483 236 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
484 483 140 readdcld ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
485 246 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) )
486 199 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
487 249 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
488 251 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
489 487 488 478 254 syl3anc ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 )
490 486 37 483 489 ltadd2dd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) < ( 𝑋 + 𝑠 ) )
491 485 490 eqbrtrd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑋 + 𝑠 ) )
492 217 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
493 487 488 478 259 syl3anc ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
494 37 492 483 493 ltadd2dd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
495 266 adantr ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
496 494 495 breqtrd ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
497 481 482 484 491 496 eliood ⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
498 275 276 334 243 497 fourierdlem23 ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
499 480 498 eqeltrd ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
500 ssid ⊢ ℂ ⊆ ℂ
501 500 a1i ⊢ ( 𝜒 → ℂ ⊆ ℂ )
502 334 135 501 constcncfg ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝐶 ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
503 499 502 subcncf ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
504 175 ralrimiva ⊢ ( 𝜒 → ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) 𝑠 ∈ ( ℂ ∖ { 0 } ) )
505 dfss3 ⊢ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ℂ ∖ { 0 } ) ↔ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) 𝑠 ∈ ( ℂ ∖ { 0 } ) )
506 504 505 sylibr ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ℂ ∖ { 0 } ) )
507 difssd ⊢ ( 𝜒 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
508 506 507 idcncfg ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ( ℂ ∖ { 0 } ) ) )
509 503 508 divcncf ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
510 334 501 idcncfg ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
511 359 347 fmptd ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⟶ ( ℂ ∖ { 0 } ) )
512 334 362 501 constcncfg ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
513 sincn ⊢ sin ∈ ( ℂ –cn→ ℂ )
514 513 a1i ⊢ ( 𝜒 → sin ∈ ( ℂ –cn→ ℂ ) )
515 371 a1i ⊢ ( 𝜒 → 2 ∈ ( ℂ ∖ { 0 } ) )
516 334 515 507 constcncfg ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ( ℂ ∖ { 0 } ) ) )
517 510 516 divcncf ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / 2 ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
518 514 517 cncfmpt1f ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
519 512 518 mulcncf ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
520 cncfcdm ⊢ ( ( ( ℂ ∖ { 0 } ) ⊆ ℂ ∧ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) → ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⟶ ( ℂ ∖ { 0 } ) ) )
521 507 519 520 syl2anc ⊢ ( 𝜒 → ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⟶ ( ℂ ∖ { 0 } ) ) )
522 511 521 mpbird ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ( ℂ ∖ { 0 } ) ) )
523 510 522 divcncf ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
524 509 523 mulcncf ⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
525 406 524 eqeltrd ⊢ ( 𝜒 → ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
526 22 525 sylbir ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
527 409 477 526 jca31 ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝐸 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) )