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
|
ffvelrnd |
⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 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
|
ffvelrnd |
⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 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
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ ) |
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
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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
|
ffvelrnd |
⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ℝ ) |
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
|
ffvelrnd |
⊢ ( 𝜒 → ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 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
|
ffvelrnd |
⊢ ( 𝜒 → ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ ) |
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 |
|
cncffvrn |
⊢ ( ( ( ℂ ∖ { 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→ ℂ ) ) ) |