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→ ℂ ) ) )