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