Step | Hyp | Ref
| Expression |
1 | | 0red 10490 |
. . 3
⊢ (𝜑 → 0 ∈
ℝ) |
2 | | fourierdlem61.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | fourierdlem61.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
4 | 2, 3 | resubcld 10916 |
. . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
5 | 4 | rexrd 10537 |
. . 3
⊢ (𝜑 → (𝐵 − 𝐴) ∈
ℝ*) |
6 | | fourierdlem61.altb |
. . . 4
⊢ (𝜑 → 𝐴 < 𝐵) |
7 | 3, 2 | posdifd 11075 |
. . . 4
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
8 | 6, 7 | mpbid 233 |
. . 3
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
9 | | fourierdlem61.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
10 | 9 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
11 | 3 | rexrd 10537 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
12 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐴 ∈
ℝ*) |
13 | 2 | rexrd 10537 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐵 ∈
ℝ*) |
15 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐴 ∈ ℝ) |
16 | | elioore 12618 |
. . . . . . . . 9
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) → 𝑠 ∈ ℝ) |
17 | 16 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑠 ∈ ℝ) |
18 | 15, 17 | readdcld 10516 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) ∈ ℝ) |
19 | 3 | recnd 10515 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
20 | 19 | addid1d 10687 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
21 | 20 | eqcomd 2801 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝐴 + 0)) |
22 | 21 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐴 = (𝐴 + 0)) |
23 | | 0red 10490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 0 ∈
ℝ) |
24 | | 0xr 10534 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 0 ∈
ℝ*) |
26 | 5 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐵 − 𝐴) ∈
ℝ*) |
27 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑠 ∈ (0(,)(𝐵 − 𝐴))) |
28 | | ioogtlb 41312 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ (𝐵 − 𝐴) ∈ ℝ* ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 0 < 𝑠) |
29 | 25, 26, 27, 28 | syl3anc 1364 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 0 < 𝑠) |
30 | 23, 17, 15, 29 | ltadd2dd 10646 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 0) < (𝐴 + 𝑠)) |
31 | 22, 30 | eqbrtrd 4984 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐴 < (𝐴 + 𝑠)) |
32 | 4 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐵 − 𝐴) ∈ ℝ) |
33 | | iooltub 41328 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ (𝐵 − 𝐴) ∈ ℝ* ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑠 < (𝐵 − 𝐴)) |
34 | 25, 26, 27, 33 | syl3anc 1364 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑠 < (𝐵 − 𝐴)) |
35 | 17, 32, 15, 34 | ltadd2dd 10646 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) < (𝐴 + (𝐵 − 𝐴))) |
36 | 2 | recnd 10515 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) |
37 | 19, 36 | pncan3d 10848 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵) |
38 | 37 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + (𝐵 − 𝐴)) = 𝐵) |
39 | 35, 38 | breqtrd 4988 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) < 𝐵) |
40 | 12, 14, 18, 31, 39 | eliood 41315 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) ∈ (𝐴(,)𝐵)) |
41 | 10, 40 | ffvelrnd 6717 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐹‘(𝐴 + 𝑠)) ∈ ℝ) |
42 | | ioossre 12648 |
. . . . . . . . 9
⊢ (𝐴(,)𝐵) ⊆ ℝ |
43 | 42 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
44 | | ax-resscn 10440 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
45 | 43, 44 | syl6ss 3901 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
46 | | eqid 2795 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
47 | 46, 13, 3, 6 | lptioo1cn 41469 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴(,)𝐵))) |
48 | | fourierdlem61.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐴)) |
49 | 9, 45, 47, 48 | limcrecl 41452 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ℝ) |
50 | 49 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑌 ∈ ℝ) |
51 | 41, 50 | resubcld 10916 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝐹‘(𝐴 + 𝑠)) − 𝑌) ∈ ℝ) |
52 | | fourierdlem61.n |
. . . 4
⊢ 𝑁 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) |
53 | 51, 52 | fmptd 6741 |
. . 3
⊢ (𝜑 → 𝑁:(0(,)(𝐵 − 𝐴))⟶ℝ) |
54 | | fourierdlem61.d |
. . . 4
⊢ 𝐷 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠) |
55 | 17, 54 | fmptd 6741 |
. . 3
⊢ (𝜑 → 𝐷:(0(,)(𝐵 − 𝐴))⟶ℝ) |
56 | 52 | oveq2i 7027 |
. . . . . 6
⊢ (ℝ
D 𝑁) = (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))) |
57 | 56 | a1i 11 |
. . . . 5
⊢ (𝜑 → (ℝ D 𝑁) = (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)))) |
58 | 57 | dmeqd 5660 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝑁) = dom (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)))) |
59 | | reelprrecn 10475 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
60 | 59 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
61 | 41 | recnd 10515 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐹‘(𝐴 + 𝑠)) ∈ ℂ) |
62 | | dvfre 24231 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
63 | 9, 43, 62 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
64 | | fourierdlem61.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (ℝ D 𝐹) |
65 | 64 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 = (ℝ D 𝐹)) |
66 | 65 | feq1d 6367 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺:dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)) |
67 | 63, 66 | mpbird 258 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:dom (ℝ D 𝐹)⟶ℝ) |
68 | 67 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐺:dom (ℝ D 𝐹)⟶ℝ) |
69 | 65 | eqcomd 2801 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) |
70 | 69 | dmeqd 5660 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (ℝ D 𝐹) = dom 𝐺) |
71 | | fourierdlem61.domg |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐺 = (𝐴(,)𝐵)) |
72 | 70, 71 | eqtr2d 2832 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) = dom (ℝ D 𝐹)) |
73 | 72 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴(,)𝐵) = dom (ℝ D 𝐹)) |
74 | 40, 73 | eleqtrd 2885 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) ∈ dom (ℝ D 𝐹)) |
75 | 68, 74 | ffvelrnd 6717 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐺‘(𝐴 + 𝑠)) ∈ ℝ) |
76 | | 1red 10488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 1 ∈
ℝ) |
77 | 9 | ffvelrnda 6716 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
78 | 77 | recnd 10515 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
79 | 72 | feq2d 6368 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺:(𝐴(,)𝐵)⟶ℝ ↔ 𝐺:dom (ℝ D 𝐹)⟶ℝ)) |
80 | 67, 79 | mpbird 258 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
81 | 80 | ffvelrnda 6716 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) ∈ ℝ) |
82 | 19 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐴 ∈ ℂ) |
83 | 19 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝐴 ∈ ℂ) |
84 | | 0red 10490 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 0 ∈
ℝ) |
85 | 60, 19 | dvmptc 24238 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝐴)) = (𝑠 ∈ ℝ ↦ 0)) |
86 | | ioossre 12648 |
. . . . . . . . . . . . 13
⊢
(0(,)(𝐵 −
𝐴)) ⊆
ℝ |
87 | 86 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0(,)(𝐵 − 𝐴)) ⊆ ℝ) |
88 | 46 | tgioo2 23094 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
89 | | iooretop 23057 |
. . . . . . . . . . . . 13
⊢
(0(,)(𝐵 −
𝐴)) ∈
(topGen‘ran (,)) |
90 | 89 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0(,)(𝐵 − 𝐴)) ∈ (topGen‘ran
(,))) |
91 | 60, 83, 84, 85, 87, 88, 46, 90 | dvmptres 24243 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝐴)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 0)) |
92 | 17 | recnd 10515 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑠 ∈ ℂ) |
93 | | recn 10473 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ → 𝑠 ∈
ℂ) |
94 | 93 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℂ) |
95 | | 1red 10488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 1 ∈
ℝ) |
96 | 60 | dvmptid 24237 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝑠)) = (𝑠 ∈ ℝ ↦ 1)) |
97 | 60, 94, 95, 96, 87, 88, 46, 90 | dvmptres 24243 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)) |
98 | 60, 82, 23, 91, 92, 76, 97 | dvmptadd 24240 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (0 + 1))) |
99 | | 0p1e1 11607 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
100 | 99 | mpteq2i 5052 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (0 + 1)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) |
101 | 98, 100 | syl6eq 2847 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)) |
102 | 9 | feqmptd 6601 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) |
103 | 102 | eqcomd 2801 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) = 𝐹) |
104 | 103 | oveq2d 7032 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (ℝ D 𝐹)) |
105 | 80 | feqmptd 6601 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥))) |
106 | 104, 69, 105 | 3eqtrd 2835 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥))) |
107 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴 + 𝑠) → (𝐹‘𝑥) = (𝐹‘(𝐴 + 𝑠))) |
108 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴 + 𝑠) → (𝐺‘𝑥) = (𝐺‘(𝐴 + 𝑠))) |
109 | 60, 60, 40, 76, 78, 81, 101, 106, 107, 108 | dvmptco 24252 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐹‘(𝐴 + 𝑠)))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) · 1))) |
110 | 75 | recnd 10515 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐺‘(𝐴 + 𝑠)) ∈ ℂ) |
111 | 110 | mulid1d 10504 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝐺‘(𝐴 + 𝑠)) · 1) = (𝐺‘(𝐴 + 𝑠))) |
112 | 111 | mpteq2dva 5055 |
. . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) · 1)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
113 | 109, 112 | eqtrd 2831 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐹‘(𝐴 + 𝑠)))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
114 | | limccl 24156 |
. . . . . . . . 9
⊢ (𝐹 limℂ 𝐴) ⊆
ℂ |
115 | 114, 48 | sseldi 3887 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ ℂ) |
116 | 115 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑌 ∈ ℂ) |
117 | 115 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑌 ∈ ℂ) |
118 | 60, 115 | dvmptc 24238 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝑌)) = (𝑠 ∈ ℝ ↦ 0)) |
119 | 60, 117, 84, 118, 87, 88, 46, 90 | dvmptres 24243 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑌)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 0)) |
120 | 60, 61, 75, 113, 116, 25, 119 | dvmptsub 24247 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) − 0))) |
121 | 110 | subid1d 10834 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝐺‘(𝐴 + 𝑠)) − 0) = (𝐺‘(𝐴 + 𝑠))) |
122 | 121 | mpteq2dva 5055 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) − 0)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
123 | 120, 122 | eqtrd 2831 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
124 | 123 | dmeqd 5660 |
. . . 4
⊢ (𝜑 → dom (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))) = dom (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
125 | 75 | ralrimiva 3149 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ (0(,)(𝐵 − 𝐴))(𝐺‘(𝐴 + 𝑠)) ∈ ℝ) |
126 | | dmmptg 5971 |
. . . . 5
⊢
(∀𝑠 ∈
(0(,)(𝐵 − 𝐴))(𝐺‘(𝐴 + 𝑠)) ∈ ℝ → dom (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) = (0(,)(𝐵 − 𝐴))) |
127 | 125, 126 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) = (0(,)(𝐵 − 𝐴))) |
128 | 58, 124, 127 | 3eqtrd 2835 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝑁) = (0(,)(𝐵 − 𝐴))) |
129 | 54 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠)) |
130 | 129 | oveq2d 7032 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐷) = (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠))) |
131 | 130, 97 | eqtrd 2831 |
. . . . 5
⊢ (𝜑 → (ℝ D 𝐷) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)) |
132 | 131 | dmeqd 5660 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝐷) = dom (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)) |
133 | 76 | ralrimiva 3149 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ (0(,)(𝐵 − 𝐴))1 ∈ ℝ) |
134 | | dmmptg 5971 |
. . . . 5
⊢
(∀𝑠 ∈
(0(,)(𝐵 − 𝐴))1 ∈ ℝ → dom
(𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) = (0(,)(𝐵 − 𝐴))) |
135 | 133, 134 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) = (0(,)(𝐵 − 𝐴))) |
136 | 132, 135 | eqtrd 2831 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐷) = (0(,)(𝐵 − 𝐴))) |
137 | | eqid 2795 |
. . . . 5
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐹‘(𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐹‘(𝐴 + 𝑠))) |
138 | | eqid 2795 |
. . . . 5
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑌) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑌) |
139 | | eqid 2795 |
. . . . 5
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) |
140 | 40 | adantrr 713 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) ≠ 𝐴)) → (𝐴 + 𝑠) ∈ (𝐴(,)𝐵)) |
141 | | eqid 2795 |
. . . . . . . 8
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝐴) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝐴) |
142 | | eqid 2795 |
. . . . . . . 8
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠) |
143 | | eqid 2795 |
. . . . . . . 8
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠)) |
144 | 87, 44 | syl6ss 3901 |
. . . . . . . . 9
⊢ (𝜑 → (0(,)(𝐵 − 𝐴)) ⊆ ℂ) |
145 | 1 | recnd 10515 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℂ) |
146 | 141, 144,
19, 145 | constlimc 41447 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝐴) limℂ 0)) |
147 | 144, 142,
145 | idlimc 41449 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠) limℂ 0)) |
148 | 141, 142,
143, 82, 92, 146, 147 | addlimc 41471 |
. . . . . . 7
⊢ (𝜑 → (𝐴 + 0) ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠)) limℂ 0)) |
149 | 21, 148 | eqeltrd 2883 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠)) limℂ 0)) |
150 | 102 | oveq1d 7031 |
. . . . . . 7
⊢ (𝜑 → (𝐹 limℂ 𝐴) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) limℂ 𝐴)) |
151 | 48, 150 | eleqtrd 2885 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) limℂ 𝐴)) |
152 | | simplrr 774 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐹‘(𝐴 + 𝑠)) = 𝑌) → (𝐴 + 𝑠) = 𝐴) |
153 | 15, 31 | gtned 10622 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) ≠ 𝐴) |
154 | 153 | neneqd 2989 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ¬ (𝐴 + 𝑠) = 𝐴) |
155 | 154 | adantrr 713 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) → ¬ (𝐴 + 𝑠) = 𝐴) |
156 | 155 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐹‘(𝐴 + 𝑠)) = 𝑌) → ¬ (𝐴 + 𝑠) = 𝐴) |
157 | 152, 156 | condan 814 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) → (𝐹‘(𝐴 + 𝑠)) = 𝑌) |
158 | 140, 78, 149, 151, 107, 157 | limcco 24174 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐹‘(𝐴 + 𝑠))) limℂ
0)) |
159 | 138, 144,
115, 145 | constlimc 41447 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑌) limℂ 0)) |
160 | 137, 138,
139, 61, 116, 158, 159 | sublimc 41475 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝑌) ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) limℂ
0)) |
161 | 115 | subidd 10833 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝑌) = 0) |
162 | 52 | eqcomi 2804 |
. . . . . 6
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) = 𝑁 |
163 | 162 | oveq1i 7026 |
. . . . 5
⊢ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) limℂ 0) = (𝑁 limℂ
0) |
164 | 163 | a1i 11 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) limℂ 0) = (𝑁 limℂ
0)) |
165 | 160, 161,
164 | 3eltr3d 2897 |
. . 3
⊢ (𝜑 → 0 ∈ (𝑁 limℂ
0)) |
166 | 144, 54, 145 | idlimc 41449 |
. . 3
⊢ (𝜑 → 0 ∈ (𝐷 limℂ
0)) |
167 | | lbioo 12619 |
. . . . 5
⊢ ¬ 0
∈ (0(,)(𝐵 −
𝐴)) |
168 | 167 | a1i 11 |
. . . 4
⊢ (𝜑 → ¬ 0 ∈ (0(,)(𝐵 − 𝐴))) |
169 | | mptresid 5798 |
. . . . . . 7
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠) = ( I ↾ (0(,)(𝐵 − 𝐴))) |
170 | 129, 169 | syl6eq 2847 |
. . . . . 6
⊢ (𝜑 → 𝐷 = ( I ↾ (0(,)(𝐵 − 𝐴)))) |
171 | 170 | rneqd 5690 |
. . . . 5
⊢ (𝜑 → ran 𝐷 = ran ( I ↾ (0(,)(𝐵 − 𝐴)))) |
172 | | rnresi 5819 |
. . . . 5
⊢ ran ( I
↾ (0(,)(𝐵 −
𝐴))) = (0(,)(𝐵 − 𝐴)) |
173 | 171, 172 | syl6req 2848 |
. . . 4
⊢ (𝜑 → (0(,)(𝐵 − 𝐴)) = ran 𝐷) |
174 | 168, 173 | neleqtrd 2904 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ran 𝐷) |
175 | | 0ne1 11556 |
. . . . . 6
⊢ 0 ≠
1 |
176 | 175 | neii 2986 |
. . . . 5
⊢ ¬ 0
= 1 |
177 | | elsng 4486 |
. . . . . 6
⊢ (0 ∈
ℝ → (0 ∈ {1} ↔ 0 = 1)) |
178 | 1, 177 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 ∈ {1} ↔ 0 =
1)) |
179 | 176, 178 | mtbiri 328 |
. . . 4
⊢ (𝜑 → ¬ 0 ∈
{1}) |
180 | 131 | rneqd 5690 |
. . . . 5
⊢ (𝜑 → ran (ℝ D 𝐷) = ran (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)) |
181 | | eqid 2795 |
. . . . . 6
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) |
182 | 24 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ*) |
183 | | ioon0 12614 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ (𝐵 − 𝐴) ∈ ℝ*) →
((0(,)(𝐵 − 𝐴)) ≠ ∅ ↔ 0 <
(𝐵 − 𝐴))) |
184 | 182, 5, 183 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((0(,)(𝐵 − 𝐴)) ≠ ∅ ↔ 0 < (𝐵 − 𝐴))) |
185 | 8, 184 | mpbird 258 |
. . . . . 6
⊢ (𝜑 → (0(,)(𝐵 − 𝐴)) ≠ ∅) |
186 | 181, 76, 185 | rnmptc 6836 |
. . . . 5
⊢ (𝜑 → ran (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) = {1}) |
187 | 180, 186 | eqtr2d 2832 |
. . . 4
⊢ (𝜑 → {1} = ran (ℝ D 𝐷)) |
188 | 179, 187 | neleqtrd 2904 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐷)) |
189 | 81 | recnd 10515 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) ∈ ℂ) |
190 | | fourierdlem61.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ (𝐺 limℂ 𝐴)) |
191 | 105 | oveq1d 7031 |
. . . . . 6
⊢ (𝜑 → (𝐺 limℂ 𝐴) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥)) limℂ 𝐴)) |
192 | 190, 191 | eleqtrd 2885 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥)) limℂ 𝐴)) |
193 | | simplrr 774 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐺‘(𝐴 + 𝑠)) = 𝐸) → (𝐴 + 𝑠) = 𝐴) |
194 | 155 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐺‘(𝐴 + 𝑠)) = 𝐸) → ¬ (𝐴 + 𝑠) = 𝐴) |
195 | 193, 194 | condan 814 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) → (𝐺‘(𝐴 + 𝑠)) = 𝐸) |
196 | 140, 189,
149, 192, 108, 195 | limcco 24174 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) limℂ
0)) |
197 | 110 | div1d 11256 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝐺‘(𝐴 + 𝑠)) / 1) = (𝐺‘(𝐴 + 𝑠))) |
198 | 56, 123 | syl5eq 2843 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D 𝑁) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
199 | 198 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (ℝ D 𝑁) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
200 | 199 | fveq1d 6540 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((ℝ D 𝑁)‘𝑠) = ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))‘𝑠)) |
201 | | eqid 2795 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) |
202 | 201 | fvmpt2 6645 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐺‘(𝐴 + 𝑠)) ∈ ℝ) → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))‘𝑠) = (𝐺‘(𝐴 + 𝑠))) |
203 | 27, 75, 202 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))‘𝑠) = (𝐺‘(𝐴 + 𝑠))) |
204 | 200, 203 | eqtr2d 2832 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐺‘(𝐴 + 𝑠)) = ((ℝ D 𝑁)‘𝑠)) |
205 | 131 | fveq1d 6540 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D 𝐷)‘𝑠) = ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)‘𝑠)) |
206 | 205 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((ℝ D 𝐷)‘𝑠) = ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)‘𝑠)) |
207 | 181 | fvmpt2 6645 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ 1 ∈ ℝ) → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)‘𝑠) = 1) |
208 | 27, 76, 207 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)‘𝑠) = 1) |
209 | 206, 208 | eqtr2d 2832 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 1 = ((ℝ D 𝐷)‘𝑠)) |
210 | 204, 209 | oveq12d 7034 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝐺‘(𝐴 + 𝑠)) / 1) = (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) |
211 | 197, 210 | eqtr3d 2833 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐺‘(𝐴 + 𝑠)) = (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) |
212 | 211 | mpteq2dva 5055 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠)))) |
213 | 212 | oveq1d 7031 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) limℂ 0) = ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) limℂ
0)) |
214 | 196, 213 | eleqtrd 2885 |
. . 3
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) limℂ
0)) |
215 | 1, 5, 8, 53, 55, 128, 136, 165, 166, 174, 188, 214 | lhop1 24294 |
. 2
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) limℂ
0)) |
216 | 52 | fvmpt2 6645 |
. . . . . . 7
⊢ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ ((𝐹‘(𝐴 + 𝑠)) − 𝑌) ∈ ℝ) → (𝑁‘𝑠) = ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) |
217 | 27, 51, 216 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝑁‘𝑠) = ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) |
218 | 54 | fvmpt2 6645 |
. . . . . . 7
⊢ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐷‘𝑠) = 𝑠) |
219 | 27, 27, 218 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐷‘𝑠) = 𝑠) |
220 | 217, 219 | oveq12d 7034 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝑁‘𝑠) / (𝐷‘𝑠)) = (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠)) |
221 | 220 | mpteq2dva 5055 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠))) |
222 | | fourierdlem61.h |
. . . 4
⊢ 𝐻 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠)) |
223 | 221, 222 | syl6eqr 2849 |
. . 3
⊢ (𝜑 → (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) = 𝐻) |
224 | 223 | oveq1d 7031 |
. 2
⊢ (𝜑 → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) limℂ 0) = (𝐻 limℂ
0)) |
225 | 215, 224 | eleqtrd 2885 |
1
⊢ (𝜑 → 𝐸 ∈ (𝐻 limℂ 0)) |