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

Metamath Proof Explorer

Theorem fourierdlem86

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

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

Proof

Step Hyp Ref Expression
1 fourierdlem86.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem86.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3 fourierdlem86.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
4 fourierdlem86.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5 fourierdlem86.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
6 fourierdlem86.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
7 fourierdlem86.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
8 fourierdlem86.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
9 fourierdlem86.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
10 fourierdlem86.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
11 fourierdlem86.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
12 fourierdlem86.ab ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
13 fourierdlem86.n0 ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
14 fourierdlem86.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
15 fourierdlem86.o ⊢ 𝑂 = ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
16 fourierdlem86.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
17 fourierdlem86.t ⊢ 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
18 fourierdlem86.n ⊢ 𝑁 = ( ( ♯ ‘ 𝑇 ) − 1 )
19 fourierdlem86.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
20 fourierdlem86.d ⊢ 𝐷 = ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) )
21 fourierdlem86.e ⊢ 𝐸 = ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) )
22 fourierdlem86.u ⊢ 𝑈 = ( ℩ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
23 2 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑋 ∈ ℝ )
24 4 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑀 ∈ ℕ )
25 5 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
26 9 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ℝ )
27 10 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ∈ ℝ )
28 11 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 < 𝐵 )
29 12 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
31 biid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑦 ) (,) ( 𝑄 ‘ ( 𝑦 + 1 ) ) ) ) ↔ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑦 ) (,) ( 𝑄 ‘ ( 𝑦 + 1 ) ) ) ) )
32 23 3 24 25 26 27 28 29 16 17 18 19 30 22 31 fourierdlem50 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑈 ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ) )
33 32 simpld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑈 ∈ ( 0 ..^ 𝑀 ) )
34 id ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) )
35 32 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) )
36 34 33 35 jca31 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ) )
37 nfv ⊢ Ⅎ 𝑖 ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) )
38 nfv ⊢ Ⅎ 𝑖 ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) )
39 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑈 / 𝑖 ⦌ 𝐿
40 nfcv ⊢ Ⅎ 𝑖 ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
41 38 39 40 nfif ⊢ Ⅎ 𝑖 if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
42 nfcv ⊢ Ⅎ 𝑖 −
43 nfcv ⊢ Ⅎ 𝑖 𝐶
44 41 42 43 nfov ⊢ Ⅎ 𝑖 ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 )
45 nfcv ⊢ Ⅎ 𝑖 /
46 nfcv ⊢ Ⅎ 𝑖 ( 𝑆 ‘ ( 𝑗 + 1 ) )
47 44 45 46 nfov ⊢ Ⅎ 𝑖 ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
48 nfcv ⊢ Ⅎ 𝑖 ·
49 nfcv ⊢ Ⅎ 𝑖 ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) )
50 47 48 49 nfov ⊢ Ⅎ 𝑖 ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) )
51 50 nfel1 ⊢ Ⅎ 𝑖 ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
52 nfv ⊢ Ⅎ 𝑖 ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 )
53 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑈 / 𝑖 ⦌ 𝑅
54 nfcv ⊢ Ⅎ 𝑖 ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) )
55 52 53 54 nfif ⊢ Ⅎ 𝑖 if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) )
56 55 42 43 nfov ⊢ Ⅎ 𝑖 ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 )
57 nfcv ⊢ Ⅎ 𝑖 ( 𝑆 ‘ 𝑗 )
58 56 45 57 nfov ⊢ Ⅎ 𝑖 ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) )
59 nfcv ⊢ Ⅎ 𝑖 ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) )
60 58 48 59 nfov ⊢ Ⅎ 𝑖 ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) )
61 60 nfel1 ⊢ Ⅎ 𝑖 ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) )
62 51 61 nfan ⊢ Ⅎ 𝑖 ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
63 nfv ⊢ Ⅎ 𝑖 ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ )
64 62 63 nfan ⊢ Ⅎ 𝑖 ( ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
65 37 64 nfim ⊢ Ⅎ 𝑖 ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ) → ( ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) )
66 eleq1 ⊢ ( 𝑖 = 𝑈 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) )
67 66 anbi2d ⊢ ( 𝑖 = 𝑈 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) ) )
68 fveq2 ⊢ ( 𝑖 = 𝑈 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑈 ) )
69 oveq1 ⊢ ( 𝑖 = 𝑈 → ( 𝑖 + 1 ) = ( 𝑈 + 1 ) )
70 69 fveq2d ⊢ ( 𝑖 = 𝑈 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) )
71 68 70 oveq12d ⊢ ( 𝑖 = 𝑈 → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) )
72 71 sseq2d ⊢ ( 𝑖 = 𝑈 → ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ) )
73 67 72 anbi12d ⊢ ( 𝑖 = 𝑈 → ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ) ) )
74 70 eqeq2d ⊢ ( 𝑖 = 𝑈 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) )
75 csbeq1a ⊢ ( 𝑖 = 𝑈 → 𝐿 = ⦋ 𝑈 / 𝑖 ⦌ 𝐿 )
76 74 75 ifbieq1d ⊢ ( 𝑖 = 𝑈 → if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
77 76 oveq1d ⊢ ( 𝑖 = 𝑈 → ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) = ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) )
78 77 oveq1d ⊢ ( 𝑖 = 𝑈 → ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
79 78 oveq1d ⊢ ( 𝑖 = 𝑈 → ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) = ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) )
80 79 eleq1d ⊢ ( 𝑖 = 𝑈 → ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↔ ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
81 68 eqeq2d ⊢ ( 𝑖 = 𝑈 → ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ↔ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) ) )
82 csbeq1a ⊢ ( 𝑖 = 𝑈 → 𝑅 = ⦋ 𝑈 / 𝑖 ⦌ 𝑅 )
83 81 82 ifbieq1d ⊢ ( 𝑖 = 𝑈 → if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) = if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) )
84 83 oveq1d ⊢ ( 𝑖 = 𝑈 → ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) = ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) )
85 84 oveq1d ⊢ ( 𝑖 = 𝑈 → ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) = ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) )
86 85 oveq1d ⊢ ( 𝑖 = 𝑈 → ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) = ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) )
87 86 eleq1d ⊢ ( 𝑖 = 𝑈 → ( ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ↔ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) )
88 80 87 anbi12d ⊢ ( 𝑖 = 𝑈 → ( ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ) )
89 88 anbi1d ⊢ ( 𝑖 = 𝑈 → ( ( ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) ↔ ( ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) ) )
90 73 89 imbi12d ⊢ ( 𝑖 = 𝑈 → ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ) → ( ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) ) ) )
91 eqid ⊢ ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) = ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) )
92 eqid ⊢ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) = ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) )
93 biid ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
94 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 91 92 93 fourierdlem76 ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) )
95 65 90 94 vtoclg1f ⊢ ( 𝑈 ∈ ( 0 ..^ 𝑀 ) → ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ) → ( ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) ) )
96 33 36 95 sylc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) )
97 96 simpld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) )
98 97 simpld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑈 + 1 ) ) , ⦋ 𝑈 / 𝑖 ⦌ 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
99 20 98 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐷 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
100 97 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑈 ) , ⦋ 𝑈 / 𝑖 ⦌ 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
101 21 100 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐸 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
102 96 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
103 99 101 102 jca31 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐷 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝐸 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) )