Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem74.xre |
⊢ ( 𝜑 → 𝑋 ∈ ℝ ) |
2 |
|
fourierdlem74.p |
⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) |
3 |
|
fourierdlem74.f |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ ) |
4 |
|
fourierdlem74.x |
⊢ ( 𝜑 → 𝑋 ∈ ran 𝑉 ) |
5 |
|
fourierdlem74.y |
⊢ ( 𝜑 → 𝑌 ∈ ℝ ) |
6 |
|
fourierdlem74.w |
⊢ ( 𝜑 → 𝑊 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) |
7 |
|
fourierdlem74.h |
⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) |
8 |
|
fourierdlem74.m |
⊢ ( 𝜑 → 𝑀 ∈ ℕ ) |
9 |
|
fourierdlem74.v |
⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ) |
10 |
|
fourierdlem74.r |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) |
11 |
|
fourierdlem74.q |
⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) |
12 |
|
fourierdlem74.o |
⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) |
13 |
|
fourierdlem74.g |
⊢ 𝐺 = ( ℝ D 𝐹 ) |
14 |
|
fourierdlem74.gcn |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ ) |
15 |
|
fourierdlem74.e |
⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) |
16 |
|
fourierdlem74.a |
⊢ 𝐴 = if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
17 |
|
elfzofz |
⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) ) |
18 |
|
pire |
⊢ π ∈ ℝ |
19 |
18
|
renegcli |
⊢ - π ∈ ℝ |
20 |
19
|
a1i |
⊢ ( 𝜑 → - π ∈ ℝ ) |
21 |
20 1
|
readdcld |
⊢ ( 𝜑 → ( - π + 𝑋 ) ∈ ℝ ) |
22 |
18
|
a1i |
⊢ ( 𝜑 → π ∈ ℝ ) |
23 |
22 1
|
readdcld |
⊢ ( 𝜑 → ( π + 𝑋 ) ∈ ℝ ) |
24 |
21 23
|
iccssred |
⊢ ( 𝜑 → ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ⊆ ℝ ) |
25 |
24
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ⊆ ℝ ) |
26 |
2 8 9
|
fourierdlem15 |
⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ) |
27 |
26
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ) |
28 |
25 27
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ ) |
29 |
17 28
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ ) |
30 |
29
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ ) |
31 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝑋 ∈ ℝ ) |
32 |
2
|
fourierdlem2 |
⊢ ( 𝑀 ∈ ℕ → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) ) |
33 |
8 32
|
syl |
⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) ) |
34 |
9 33
|
mpbid |
⊢ ( 𝜑 → ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) |
35 |
34
|
simprrd |
⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
36 |
35
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
37 |
36
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
38 |
|
eqcom |
⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ↔ 𝑋 = ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
39 |
38
|
biimpi |
⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → 𝑋 = ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
40 |
39
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝑋 = ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
41 |
37 40
|
breqtrrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑉 ‘ 𝑖 ) < 𝑋 ) |
42 |
|
ioossre |
⊢ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⊆ ℝ |
43 |
42
|
a1i |
⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⊆ ℝ ) |
44 |
3 43
|
fssresd |
⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ ) |
45 |
44
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ ) |
46 |
|
limcresi |
⊢ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ⊆ ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) |
47 |
46 6
|
sselid |
⊢ ( 𝜑 → 𝑊 ∈ ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) ) |
48 |
47
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑊 ∈ ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) ) |
49 |
|
mnfxr |
⊢ -∞ ∈ ℝ* |
50 |
49
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → -∞ ∈ ℝ* ) |
51 |
29
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* ) |
52 |
29
|
mnfltd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → -∞ < ( 𝑉 ‘ 𝑖 ) ) |
53 |
50 51 52
|
xrltled |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → -∞ ≤ ( 𝑉 ‘ 𝑖 ) ) |
54 |
|
iooss1 |
⊢ ( ( -∞ ∈ ℝ* ∧ -∞ ≤ ( 𝑉 ‘ 𝑖 ) ) → ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⊆ ( -∞ (,) 𝑋 ) ) |
55 |
50 53 54
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⊆ ( -∞ (,) 𝑋 ) ) |
56 |
55
|
resabs1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) |
57 |
56
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) ) |
58 |
48 57
|
eleqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑊 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) ) |
59 |
58
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝑊 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) ) |
60 |
|
eqid |
⊢ ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) |
61 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
62 |
61
|
a1i |
⊢ ( 𝜑 → ℝ ⊆ ℂ ) |
63 |
3 62
|
fssd |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ ) |
64 |
|
ssid |
⊢ ℝ ⊆ ℝ |
65 |
64
|
a1i |
⊢ ( 𝜑 → ℝ ⊆ ℝ ) |
66 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
67 |
66
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
68 |
66 67
|
dvres |
⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) ) |
69 |
62 63 65 43 68
|
syl22anc |
⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) ) |
70 |
13
|
eqcomi |
⊢ ( ℝ D 𝐹 ) = 𝐺 |
71 |
|
ioontr |
⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) |
72 |
70 71
|
reseq12i |
⊢ ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) |
73 |
72
|
a1i |
⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) |
74 |
69 73
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) |
75 |
74
|
dmeqd |
⊢ ( 𝜑 → dom ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = dom ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) |
76 |
75
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = dom ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) |
77 |
14
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ ) |
78 |
|
oveq2 |
⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) |
79 |
78
|
reseq2d |
⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) |
80 |
79 78
|
feq12d |
⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ ↔ ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ ) ) |
81 |
80
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ ↔ ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ ) ) |
82 |
77 81
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ ) |
83 |
|
fdm |
⊢ ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ⟶ ℝ → dom ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) |
84 |
82 83
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → dom ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) |
85 |
76 84
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) = ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) |
86 |
|
limcresi |
⊢ ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ⊆ ( ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) |
87 |
55
|
resabs1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) |
88 |
87
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) = ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) ) |
89 |
86 88
|
sseqtrid |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ⊆ ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) ) |
90 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐸 ∈ ( ( 𝐺 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) |
91 |
89 90
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐸 ∈ ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) ) |
92 |
69 73
|
eqtr2d |
⊢ ( 𝜑 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) ) |
93 |
92
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) = ( ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) limℂ 𝑋 ) ) |
94 |
93
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐺 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) limℂ 𝑋 ) = ( ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) limℂ 𝑋 ) ) |
95 |
91 94
|
eleqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐸 ∈ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) limℂ 𝑋 ) ) |
96 |
95
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐸 ∈ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ) limℂ 𝑋 ) ) |
97 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) = ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) |
98 |
|
oveq2 |
⊢ ( 𝑥 = 𝑠 → ( 𝑋 + 𝑥 ) = ( 𝑋 + 𝑠 ) ) |
99 |
98
|
fveq2d |
⊢ ( 𝑥 = 𝑠 → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑥 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) ) |
100 |
99
|
oveq1d |
⊢ ( 𝑥 = 𝑠 → ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑥 ) ) − 𝑊 ) = ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) |
101 |
100
|
cbvmptv |
⊢ ( 𝑥 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑥 ) ) − 𝑊 ) ) = ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) |
102 |
|
id |
⊢ ( 𝑥 = 𝑠 → 𝑥 = 𝑠 ) |
103 |
102
|
cbvmptv |
⊢ ( 𝑥 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ 𝑥 ) = ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ 𝑠 ) |
104 |
30 31 41 45 59 60 85 96 97 101 103
|
fourierdlem60 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐸 ∈ ( ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) limℂ 0 ) ) |
105 |
|
iftrue |
⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = 𝐸 ) |
106 |
16 105
|
eqtrid |
⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → 𝐴 = 𝐸 ) |
107 |
106
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐴 = 𝐸 ) |
108 |
7
|
reseq1i |
⊢ ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
109 |
108
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) |
110 |
|
ioossicc |
⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) |
111 |
19
|
rexri |
⊢ - π ∈ ℝ* |
112 |
111
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → - π ∈ ℝ* ) |
113 |
18
|
rexri |
⊢ π ∈ ℝ* |
114 |
113
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → π ∈ ℝ* ) |
115 |
19
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → - π ∈ ℝ ) |
116 |
18
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → π ∈ ℝ ) |
117 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ℝ ) |
118 |
28 117
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ ) |
119 |
20
|
recnd |
⊢ ( 𝜑 → - π ∈ ℂ ) |
120 |
1
|
recnd |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
121 |
119 120
|
pncand |
⊢ ( 𝜑 → ( ( - π + 𝑋 ) − 𝑋 ) = - π ) |
122 |
121
|
eqcomd |
⊢ ( 𝜑 → - π = ( ( - π + 𝑋 ) − 𝑋 ) ) |
123 |
122
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → - π = ( ( - π + 𝑋 ) − 𝑋 ) ) |
124 |
21
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( - π + 𝑋 ) ∈ ℝ ) |
125 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( π + 𝑋 ) ∈ ℝ ) |
126 |
|
elicc2 |
⊢ ( ( ( - π + 𝑋 ) ∈ ℝ ∧ ( π + 𝑋 ) ∈ ℝ ) → ( ( 𝑉 ‘ 𝑖 ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ↔ ( ( 𝑉 ‘ 𝑖 ) ∈ ℝ ∧ ( - π + 𝑋 ) ≤ ( 𝑉 ‘ 𝑖 ) ∧ ( 𝑉 ‘ 𝑖 ) ≤ ( π + 𝑋 ) ) ) ) |
127 |
124 125 126
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ↔ ( ( 𝑉 ‘ 𝑖 ) ∈ ℝ ∧ ( - π + 𝑋 ) ≤ ( 𝑉 ‘ 𝑖 ) ∧ ( 𝑉 ‘ 𝑖 ) ≤ ( π + 𝑋 ) ) ) ) |
128 |
27 127
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) ∈ ℝ ∧ ( - π + 𝑋 ) ≤ ( 𝑉 ‘ 𝑖 ) ∧ ( 𝑉 ‘ 𝑖 ) ≤ ( π + 𝑋 ) ) ) |
129 |
128
|
simp2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( - π + 𝑋 ) ≤ ( 𝑉 ‘ 𝑖 ) ) |
130 |
124 28 117 129
|
lesub1dd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( - π + 𝑋 ) − 𝑋 ) ≤ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) |
131 |
123 130
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → - π ≤ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) |
132 |
128
|
simp3d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ≤ ( π + 𝑋 ) ) |
133 |
28 125 117 132
|
lesub1dd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ≤ ( ( π + 𝑋 ) − 𝑋 ) ) |
134 |
116
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → π ∈ ℂ ) |
135 |
120
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ℂ ) |
136 |
134 135
|
pncand |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( π + 𝑋 ) − 𝑋 ) = π ) |
137 |
133 136
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ≤ π ) |
138 |
115 116 118 131 137
|
eliccd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ( - π [,] π ) ) |
139 |
138 11
|
fmptd |
⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) ) |
140 |
139
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) ) |
141 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) ) |
142 |
112 114 140 141
|
fourierdlem8 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) ) |
143 |
110 142
|
sstrid |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) ) |
144 |
143
|
resmptd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ) |
145 |
144
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) ) |
146 |
17
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) ) |
147 |
17 118
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ ) |
148 |
11
|
fvmpt2 |
⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) |
149 |
146 147 148
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) |
150 |
149
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) |
151 |
|
fveq2 |
⊢ ( 𝑖 = 𝑗 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑗 ) ) |
152 |
151
|
oveq1d |
⊢ ( 𝑖 = 𝑗 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) |
153 |
152
|
cbvmptv |
⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) |
154 |
11 153
|
eqtri |
⊢ 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) |
155 |
154
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) ) |
156 |
|
fveq2 |
⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑉 ‘ 𝑗 ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
157 |
156
|
oveq1d |
⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) |
158 |
157
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) |
159 |
|
fzofzp1 |
⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) ) |
160 |
159
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) ) |
161 |
34
|
simpld |
⊢ ( 𝜑 → 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ) |
162 |
|
elmapi |
⊢ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ ) |
163 |
161 162
|
syl |
⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ ) |
164 |
163
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ ) |
165 |
164 160
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) |
166 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ ) |
167 |
165 166
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ ) |
168 |
155 158 160 167
|
fvmptd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) |
169 |
168
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) |
170 |
|
oveq1 |
⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) = ( 𝑋 − 𝑋 ) ) |
171 |
170
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) = ( 𝑋 − 𝑋 ) ) |
172 |
120
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝑋 ∈ ℂ ) |
173 |
172
|
subidd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑋 − 𝑋 ) = 0 ) |
174 |
17 173
|
sylanl2 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑋 − 𝑋 ) = 0 ) |
175 |
169 171 174
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = 0 ) |
176 |
150 175
|
oveq12d |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ) |
177 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 0 ) → 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
178 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 = 0 ) → 𝑀 ∈ ℕ ) |
179 |
20 22 1 2 12 8 9 11
|
fourierdlem14 |
⊢ ( 𝜑 → 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) ) |
180 |
179
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 = 0 ) → 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) ) |
181 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑠 = 0 ) → 𝑠 = 0 ) |
182 |
|
ffn |
⊢ ( 𝑉 : ( 0 ... 𝑀 ) ⟶ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) → 𝑉 Fn ( 0 ... 𝑀 ) ) |
183 |
|
fvelrnb |
⊢ ( 𝑉 Fn ( 0 ... 𝑀 ) → ( 𝑋 ∈ ran 𝑉 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑉 ‘ 𝑖 ) = 𝑋 ) ) |
184 |
26 182 183
|
3syl |
⊢ ( 𝜑 → ( 𝑋 ∈ ran 𝑉 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑉 ‘ 𝑖 ) = 𝑋 ) ) |
185 |
4 184
|
mpbid |
⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑉 ‘ 𝑖 ) = 𝑋 ) |
186 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) ) |
187 |
11
|
fvmpt2 |
⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ( - π [,] π ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) |
188 |
186 138 187
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) |
189 |
188
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) = 𝑋 ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) |
190 |
|
oveq1 |
⊢ ( ( 𝑉 ‘ 𝑖 ) = 𝑋 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( 𝑋 − 𝑋 ) ) |
191 |
190
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) = 𝑋 ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( 𝑋 − 𝑋 ) ) |
192 |
120
|
subidd |
⊢ ( 𝜑 → ( 𝑋 − 𝑋 ) = 0 ) |
193 |
192
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) = 𝑋 ) → ( 𝑋 − 𝑋 ) = 0 ) |
194 |
189 191 193
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑉 ‘ 𝑖 ) = 𝑋 ) → ( 𝑄 ‘ 𝑖 ) = 0 ) |
195 |
194
|
ex |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) = 𝑋 → ( 𝑄 ‘ 𝑖 ) = 0 ) ) |
196 |
195
|
reximdva |
⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑉 ‘ 𝑖 ) = 𝑋 → ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = 0 ) ) |
197 |
185 196
|
mpd |
⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = 0 ) |
198 |
118 11
|
fmptd |
⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ) |
199 |
|
ffn |
⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ → 𝑄 Fn ( 0 ... 𝑀 ) ) |
200 |
|
fvelrnb |
⊢ ( 𝑄 Fn ( 0 ... 𝑀 ) → ( 0 ∈ ran 𝑄 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = 0 ) ) |
201 |
198 199 200
|
3syl |
⊢ ( 𝜑 → ( 0 ∈ ran 𝑄 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) = 0 ) ) |
202 |
197 201
|
mpbird |
⊢ ( 𝜑 → 0 ∈ ran 𝑄 ) |
203 |
202
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 = 0 ) → 0 ∈ ran 𝑄 ) |
204 |
181 203
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑠 = 0 ) → 𝑠 ∈ ran 𝑄 ) |
205 |
12 178 180 204
|
fourierdlem12 |
⊢ ( ( ( 𝜑 ∧ 𝑠 = 0 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
206 |
205
|
an32s |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 = 0 ) → ¬ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
207 |
206
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 0 ) → ¬ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
208 |
177 207
|
pm2.65da |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑠 = 0 ) |
209 |
208
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑠 = 0 ) |
210 |
209
|
iffalsed |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) |
211 |
|
elioore |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ ) |
212 |
211
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ ) |
213 |
|
0red |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 ∈ ℝ ) |
214 |
|
elioo3g |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ℝ* ) ∧ ( ( 𝑄 ‘ 𝑖 ) < 𝑠 ∧ 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) |
215 |
214
|
biimpi |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ℝ* ) ∧ ( ( 𝑄 ‘ 𝑖 ) < 𝑠 ∧ 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) |
216 |
215
|
simprrd |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) |
217 |
216
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) |
218 |
175
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = 0 ) |
219 |
217 218
|
breqtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < 0 ) |
220 |
212 213 219
|
ltnsymd |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 0 < 𝑠 ) |
221 |
220
|
iffalsed |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑊 ) |
222 |
221
|
oveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) |
223 |
222
|
oveq1d |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) |
224 |
51
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* ) |
225 |
1
|
rexrd |
⊢ ( 𝜑 → 𝑋 ∈ ℝ* ) |
226 |
225
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ* ) |
227 |
166
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ ) |
228 |
227 212
|
readdcld |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ ) |
229 |
120
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℂ ) |
230 |
|
iccssre |
⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ ) |
231 |
19 18 230
|
mp2an |
⊢ ( - π [,] π ) ⊆ ℝ |
232 |
231 61
|
sstri |
⊢ ( - π [,] π ) ⊆ ℂ |
233 |
188 138
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( - π [,] π ) ) |
234 |
17 233
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( - π [,] π ) ) |
235 |
232 234
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ ) |
236 |
229 235
|
addcomd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) ) |
237 |
149
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) + 𝑋 ) = ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) + 𝑋 ) ) |
238 |
29
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℂ ) |
239 |
238 229
|
npcand |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) + 𝑋 ) = ( 𝑉 ‘ 𝑖 ) ) |
240 |
236 237 239
|
3eqtrrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) ) |
241 |
240
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) ) |
242 |
149 147
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ ) |
243 |
242
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ ) |
244 |
211
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ ) |
245 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ ) |
246 |
215
|
simprld |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 ) |
247 |
246
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 ) |
248 |
243 244 245 247
|
ltadd2dd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) < ( 𝑋 + 𝑠 ) ) |
249 |
241 248
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑋 + 𝑠 ) ) |
250 |
249
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑋 + 𝑠 ) ) |
251 |
|
ltaddneg |
⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 𝑠 < 0 ↔ ( 𝑋 + 𝑠 ) < 𝑋 ) ) |
252 |
212 227 251
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 < 0 ↔ ( 𝑋 + 𝑠 ) < 𝑋 ) ) |
253 |
219 252
|
mpbid |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < 𝑋 ) |
254 |
224 226 228 250 253
|
eliood |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) |
255 |
|
fvres |
⊢ ( ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) |
256 |
255
|
eqcomd |
⊢ ( ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) ) |
257 |
254 256
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) ) |
258 |
257
|
oveq1d |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) = ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) |
259 |
258
|
oveq1d |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) = ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) |
260 |
210 223 259
|
3eqtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) |
261 |
176 260
|
mpteq12dva |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) = ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) ) |
262 |
109 145 261
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) ) |
263 |
262 175
|
oveq12d |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) (,) 0 ) ↦ ( ( ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) 𝑋 ) ) ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) / 𝑠 ) ) limℂ 0 ) ) |
264 |
104 107 263
|
3eltr4d |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐴 ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
265 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) |
266 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑠 ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑠 ) |
267 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) |
268 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐹 : ℝ ⟶ ℝ ) |
269 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ ) |
270 |
211
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ ) |
271 |
269 270
|
readdcld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ ) |
272 |
268 271
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ ) |
273 |
272
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ ) |
274 |
273
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ ) |
275 |
274
|
3adantl3 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ ) |
276 |
5
|
recnd |
⊢ ( 𝜑 → 𝑌 ∈ ℂ ) |
277 |
|
limccl |
⊢ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ⊆ ℂ |
278 |
277 6
|
sselid |
⊢ ( 𝜑 → 𝑊 ∈ ℂ ) |
279 |
276 278
|
ifcld |
⊢ ( 𝜑 → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ ) |
280 |
279
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ ) |
281 |
280
|
3ad2antl1 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ ) |
282 |
275 281
|
subcld |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℂ ) |
283 |
211
|
recnd |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℂ ) |
284 |
283
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℂ ) |
285 |
|
velsn |
⊢ ( 𝑠 ∈ { 0 } ↔ 𝑠 = 0 ) |
286 |
208 285
|
sylnibr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑠 ∈ { 0 } ) |
287 |
286
|
3adantl3 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑠 ∈ { 0 } ) |
288 |
284 287
|
eldifd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ( ℂ ∖ { 0 } ) ) |
289 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) |
290 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑊 ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑊 ) |
291 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) |
292 |
278
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑊 ∈ ℂ ) |
293 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : ℝ ⟶ ℝ ) |
294 |
|
ioossre |
⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ |
295 |
294
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ ) |
296 |
51
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* ) |
297 |
165
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ) |
298 |
297
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ) |
299 |
271
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ ) |
300 |
198
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ) |
301 |
300 160
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) |
302 |
301
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) |
303 |
216
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) |
304 |
244 302 245 303
|
ltadd2dd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
305 |
168
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑋 + ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) |
306 |
165
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℂ ) |
307 |
229 306
|
pncan3d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
308 |
305 307
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
309 |
308
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
310 |
304 309
|
breqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
311 |
296 298 299 249 310
|
eliood |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) |
312 |
|
ioossre |
⊢ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ |
313 |
312
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ ) |
314 |
244 303
|
ltned |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ≠ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) |
315 |
308
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) = ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
316 |
315
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) |
317 |
10 316
|
eleqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) |
318 |
301
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℂ ) |
319 |
293 166 295 289 311 313 314 317 318
|
fourierdlem53 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
320 |
|
ioosscn |
⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ |
321 |
320
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ ) |
322 |
278
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑊 ∈ ℂ ) |
323 |
290 321 322 318
|
constlimc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑊 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑊 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
324 |
289 290 291 274 292 319 323
|
sublimc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 − 𝑊 ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
325 |
324
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑅 − 𝑊 ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
326 |
|
iftrue |
⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) = 𝑊 ) |
327 |
326
|
oveq2d |
⊢ ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) = ( 𝑅 − 𝑊 ) ) |
328 |
327
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) = ( 𝑅 − 𝑊 ) ) |
329 |
211
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ ) |
330 |
|
0red |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 ∈ ℝ ) |
331 |
301
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) |
332 |
216
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) |
333 |
168
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) |
334 |
165
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) |
335 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 ∈ ℝ ) |
336 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) |
337 |
334 335 336
|
ltled |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ≤ 𝑋 ) |
338 |
334 335
|
suble0d |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ≤ 0 ↔ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ≤ 𝑋 ) ) |
339 |
337 338
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ≤ 0 ) |
340 |
333 339
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≤ 0 ) |
341 |
340
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≤ 0 ) |
342 |
329 331 330 332 341
|
ltletrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < 0 ) |
343 |
329 330 342
|
ltnsymd |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 0 < 𝑠 ) |
344 |
343
|
iffalsed |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑊 ) |
345 |
344
|
oveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) |
346 |
345
|
mpteq2dva |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) ) |
347 |
346
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝑊 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
348 |
325 328 347
|
3eltr4d |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
349 |
348
|
3adantl3 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
350 |
|
simpl1 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝜑 ) |
351 |
|
simpl2 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) ) |
352 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 ∈ ℝ ) |
353 |
352
|
3adantl3 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 ∈ ℝ ) |
354 |
165
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) |
355 |
354
|
3adantl3 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) |
356 |
|
neqne |
⊢ ( ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ≠ 𝑋 ) |
357 |
356
|
necomd |
⊢ ( ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → 𝑋 ≠ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
358 |
357
|
adantr |
⊢ ( ( ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 ≠ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
359 |
358
|
3ad2antl3 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 ≠ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
360 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) |
361 |
353 355 359 360
|
lttri5d |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
362 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) |
363 |
274
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ ) |
364 |
279
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ ) |
365 |
319
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 𝑅 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
366 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 ) |
367 |
276
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑌 ∈ ℂ ) |
368 |
366 321 367 318
|
constlimc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑌 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
369 |
368
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 𝑌 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
370 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 𝑋 ∈ ℝ ) |
371 |
165
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) |
372 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
373 |
370 371 372
|
ltnsymd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) |
374 |
373
|
iffalsed |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) = 𝑌 ) |
375 |
|
0red |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 ∈ ℝ ) |
376 |
242
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ ) |
377 |
211
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ ) |
378 |
192
|
eqcomd |
⊢ ( 𝜑 → 0 = ( 𝑋 − 𝑋 ) ) |
379 |
378
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 0 = ( 𝑋 − 𝑋 ) ) |
380 |
29
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ ) |
381 |
51
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* ) |
382 |
297
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ) |
383 |
166
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → 𝑋 ∈ ℝ ) |
384 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) |
385 |
29
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ ) |
386 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → 𝑋 ∈ ℝ ) |
387 |
385 386
|
ltnled |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( ( 𝑉 ‘ 𝑖 ) < 𝑋 ↔ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) ) |
388 |
384 387
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( 𝑉 ‘ 𝑖 ) < 𝑋 ) |
389 |
388
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ( 𝑉 ‘ 𝑖 ) < 𝑋 ) |
390 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) |
391 |
381 382 383 389 390
|
eliood |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → 𝑋 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) |
392 |
2 8 9 4
|
fourierdlem12 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑋 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) |
393 |
392
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ ¬ 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) → ¬ 𝑋 ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) |
394 |
391 393
|
condan |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 𝑋 ≤ ( 𝑉 ‘ 𝑖 ) ) |
395 |
370 380 370 394
|
lesub1dd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑋 − 𝑋 ) ≤ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) |
396 |
379 395
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 0 ≤ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) |
397 |
149
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( 𝑄 ‘ 𝑖 ) ) |
398 |
397
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( 𝑄 ‘ 𝑖 ) ) |
399 |
396 398
|
breqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → 0 ≤ ( 𝑄 ‘ 𝑖 ) ) |
400 |
399
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 ≤ ( 𝑄 ‘ 𝑖 ) ) |
401 |
246
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 ) |
402 |
375 376 377 400 401
|
lelttrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 < 𝑠 ) |
403 |
402
|
iftrued |
⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) = 𝑌 ) |
404 |
403
|
mpteq2dva |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 ) ) |
405 |
404
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑌 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
406 |
369 374 405
|
3eltr4d |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
407 |
289 362 265 363 364 365 406
|
sublimc |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑋 < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
408 |
350 351 361 407
|
syl21anc |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
409 |
349 408
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
410 |
321 266 318
|
idlimc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑠 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
411 |
410
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝑠 ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
412 |
168
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) |
413 |
306
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℂ ) |
414 |
229
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝑋 ∈ ℂ ) |
415 |
356
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ≠ 𝑋 ) |
416 |
413 414 415
|
subne0d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ≠ 0 ) |
417 |
412 416
|
eqnetrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≠ 0 ) |
418 |
208
|
3adantl3 |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑠 = 0 ) |
419 |
418
|
neqned |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ≠ 0 ) |
420 |
265 266 267 282 288 409 411 417 419
|
divlimc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
421 |
|
iffalse |
⊢ ( ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
422 |
16 421
|
eqtrid |
⊢ ( ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 → 𝐴 = ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
423 |
422
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐴 = ( ( 𝑅 − if ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
424 |
|
ioossre |
⊢ ( -∞ (,) 𝑋 ) ⊆ ℝ |
425 |
424
|
a1i |
⊢ ( 𝜑 → ( -∞ (,) 𝑋 ) ⊆ ℝ ) |
426 |
3 425
|
fssresd |
⊢ ( 𝜑 → ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) : ( -∞ (,) 𝑋 ) ⟶ ℝ ) |
427 |
424 62
|
sstrid |
⊢ ( 𝜑 → ( -∞ (,) 𝑋 ) ⊆ ℂ ) |
428 |
49
|
a1i |
⊢ ( 𝜑 → -∞ ∈ ℝ* ) |
429 |
1
|
mnfltd |
⊢ ( 𝜑 → -∞ < 𝑋 ) |
430 |
66 428 1 429
|
lptioo2cn |
⊢ ( 𝜑 → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( -∞ (,) 𝑋 ) ) ) |
431 |
426 427 430 6
|
limcrecl |
⊢ ( 𝜑 → 𝑊 ∈ ℝ ) |
432 |
3 1 5 431 7
|
fourierdlem9 |
⊢ ( 𝜑 → 𝐻 : ( - π [,] π ) ⟶ ℝ ) |
433 |
432
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐻 : ( - π [,] π ) ⟶ ℝ ) |
434 |
433 143
|
feqresmpt |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) ) |
435 |
143
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ( - π [,] π ) ) |
436 |
|
0cnd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 0 ∈ ℂ ) |
437 |
279
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℂ ) |
438 |
274 437
|
subcld |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℂ ) |
439 |
283
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℂ ) |
440 |
208
|
neqned |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ≠ 0 ) |
441 |
438 439 440
|
divcld |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ∈ ℂ ) |
442 |
436 441
|
ifcld |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ∈ ℂ ) |
443 |
7
|
fvmpt2 |
⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ∈ ℂ ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) |
444 |
435 442 443
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) |
445 |
208
|
iffalsed |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) |
446 |
444 445
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) |
447 |
446
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) |
448 |
434 447
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) |
449 |
448
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ) |
450 |
449
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
451 |
420 423 450
|
3eltr4d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐴 ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
452 |
451
|
3expa |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ( 𝑉 ‘ ( 𝑖 + 1 ) ) = 𝑋 ) → 𝐴 ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |
453 |
264 452
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴 ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) |