Step | Hyp | Ref
| Expression |
1 | | 0red 10977 |
. . 3
⊢ (𝜑 → 0 ∈
ℝ) |
2 | | fourierdlem61.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | fourierdlem61.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
4 | 2, 3 | resubcld 11401 |
. . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
5 | 4 | rexrd 11024 |
. . 3
⊢ (𝜑 → (𝐵 − 𝐴) ∈
ℝ*) |
6 | | fourierdlem61.altb |
. . . 4
⊢ (𝜑 → 𝐴 < 𝐵) |
7 | 3, 2 | posdifd 11560 |
. . . 4
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
8 | 6, 7 | mpbid 231 |
. . 3
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
9 | | fourierdlem61.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
10 | 9 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
11 | 3 | rexrd 11024 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
12 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐴 ∈
ℝ*) |
13 | 2 | rexrd 11024 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐵 ∈
ℝ*) |
15 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐴 ∈ ℝ) |
16 | | elioore 13106 |
. . . . . . . . 9
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) → 𝑠 ∈ ℝ) |
17 | 16 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑠 ∈ ℝ) |
18 | 15, 17 | readdcld 11003 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) ∈ ℝ) |
19 | 3 | recnd 11002 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
20 | 19 | addid1d 11173 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
21 | 20 | eqcomd 2746 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝐴 + 0)) |
22 | 21 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐴 = (𝐴 + 0)) |
23 | | 0red 10977 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 0 ∈
ℝ) |
24 | | 0xr 11021 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 0 ∈
ℝ*) |
26 | 5 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐵 − 𝐴) ∈
ℝ*) |
27 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑠 ∈ (0(,)(𝐵 − 𝐴))) |
28 | 25, 26, 27 | ioogtlbd 43057 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 0 < 𝑠) |
29 | 23, 17, 15, 28 | ltadd2dd 11132 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 0) < (𝐴 + 𝑠)) |
30 | 22, 29 | eqbrtrd 5101 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐴 < (𝐴 + 𝑠)) |
31 | 4 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐵 − 𝐴) ∈ ℝ) |
32 | 25, 26, 27 | iooltubd 43051 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑠 < (𝐵 − 𝐴)) |
33 | 17, 31, 15, 32 | ltadd2dd 11132 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) < (𝐴 + (𝐵 − 𝐴))) |
34 | 2 | recnd 11002 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) |
35 | 19, 34 | pncan3d 11333 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵) |
36 | 35 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + (𝐵 − 𝐴)) = 𝐵) |
37 | 33, 36 | breqtrd 5105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) < 𝐵) |
38 | 12, 14, 18, 30, 37 | eliood 43005 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) ∈ (𝐴(,)𝐵)) |
39 | 10, 38 | ffvelrnd 6957 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐹‘(𝐴 + 𝑠)) ∈ ℝ) |
40 | | ioossre 13137 |
. . . . . . . . 9
⊢ (𝐴(,)𝐵) ⊆ ℝ |
41 | 40 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
42 | | ax-resscn 10927 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
43 | 41, 42 | sstrdi 3938 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
44 | | eqid 2740 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
45 | 44, 13, 3, 6 | lptioo1cn 43156 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴(,)𝐵))) |
46 | | fourierdlem61.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐴)) |
47 | 9, 43, 45, 46 | limcrecl 43139 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ℝ) |
48 | 47 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑌 ∈ ℝ) |
49 | 39, 48 | resubcld 11401 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝐹‘(𝐴 + 𝑠)) − 𝑌) ∈ ℝ) |
50 | | fourierdlem61.n |
. . . 4
⊢ 𝑁 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) |
51 | 49, 50 | fmptd 6983 |
. . 3
⊢ (𝜑 → 𝑁:(0(,)(𝐵 − 𝐴))⟶ℝ) |
52 | | fourierdlem61.d |
. . . 4
⊢ 𝐷 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠) |
53 | 17, 52 | fmptd 6983 |
. . 3
⊢ (𝜑 → 𝐷:(0(,)(𝐵 − 𝐴))⟶ℝ) |
54 | 50 | oveq2i 7280 |
. . . . . 6
⊢ (ℝ
D 𝑁) = (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))) |
55 | 54 | a1i 11 |
. . . . 5
⊢ (𝜑 → (ℝ D 𝑁) = (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)))) |
56 | 55 | dmeqd 5812 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝑁) = dom (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)))) |
57 | | reelprrecn 10962 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
58 | 57 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
59 | 39 | recnd 11002 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐹‘(𝐴 + 𝑠)) ∈ ℂ) |
60 | | dvfre 25111 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
61 | 9, 41, 60 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
62 | | fourierdlem61.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (ℝ D 𝐹) |
63 | 62 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 = (ℝ D 𝐹)) |
64 | 63 | feq1d 6582 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺:dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)) |
65 | 61, 64 | mpbird 256 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:dom (ℝ D 𝐹)⟶ℝ) |
66 | 65 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐺:dom (ℝ D 𝐹)⟶ℝ) |
67 | 63 | eqcomd 2746 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) |
68 | 67 | dmeqd 5812 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (ℝ D 𝐹) = dom 𝐺) |
69 | | fourierdlem61.domg |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐺 = (𝐴(,)𝐵)) |
70 | 68, 69 | eqtr2d 2781 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) = dom (ℝ D 𝐹)) |
71 | 70 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴(,)𝐵) = dom (ℝ D 𝐹)) |
72 | 38, 71 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) ∈ dom (ℝ D 𝐹)) |
73 | 66, 72 | ffvelrnd 6957 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐺‘(𝐴 + 𝑠)) ∈ ℝ) |
74 | | 1red 10975 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 1 ∈
ℝ) |
75 | 9 | ffvelrnda 6956 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
76 | 75 | recnd 11002 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
77 | 70 | feq2d 6583 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺:(𝐴(,)𝐵)⟶ℝ ↔ 𝐺:dom (ℝ D 𝐹)⟶ℝ)) |
78 | 65, 77 | mpbird 256 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
79 | 78 | ffvelrnda 6956 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) ∈ ℝ) |
80 | 19 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝐴 ∈ ℂ) |
81 | 19 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝐴 ∈ ℂ) |
82 | | 0red 10977 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 0 ∈
ℝ) |
83 | 58, 19 | dvmptc 25118 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝐴)) = (𝑠 ∈ ℝ ↦ 0)) |
84 | | ioossre 13137 |
. . . . . . . . . . . . 13
⊢
(0(,)(𝐵 −
𝐴)) ⊆
ℝ |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0(,)(𝐵 − 𝐴)) ⊆ ℝ) |
86 | | tgioo4 43080 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
87 | | iooretop 23925 |
. . . . . . . . . . . . 13
⊢
(0(,)(𝐵 −
𝐴)) ∈
(topGen‘ran (,)) |
88 | 87 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0(,)(𝐵 − 𝐴)) ∈ (topGen‘ran
(,))) |
89 | 58, 81, 82, 83, 85, 86, 44, 88 | dvmptres 25123 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝐴)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 0)) |
90 | 17 | recnd 11002 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑠 ∈ ℂ) |
91 | | recn 10960 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ → 𝑠 ∈
ℂ) |
92 | 91 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℂ) |
93 | | 1red 10975 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 1 ∈
ℝ) |
94 | 58 | dvmptid 25117 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝑠)) = (𝑠 ∈ ℝ ↦ 1)) |
95 | 58, 92, 93, 94, 85, 86, 44, 88 | dvmptres 25123 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)) |
96 | 58, 80, 23, 89, 90, 74, 95 | dvmptadd 25120 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (0 + 1))) |
97 | | 0p1e1 12093 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
98 | 97 | mpteq2i 5184 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (0 + 1)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) |
99 | 96, 98 | eqtrdi 2796 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)) |
100 | 9 | feqmptd 6832 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) |
101 | 100 | eqcomd 2746 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) = 𝐹) |
102 | 101 | oveq2d 7285 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (ℝ D 𝐹)) |
103 | 78 | feqmptd 6832 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥))) |
104 | 102, 67, 103 | 3eqtrd 2784 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥))) |
105 | | fveq2 6769 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴 + 𝑠) → (𝐹‘𝑥) = (𝐹‘(𝐴 + 𝑠))) |
106 | | fveq2 6769 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴 + 𝑠) → (𝐺‘𝑥) = (𝐺‘(𝐴 + 𝑠))) |
107 | 58, 58, 38, 74, 76, 79, 99, 104, 105, 106 | dvmptco 25132 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐹‘(𝐴 + 𝑠)))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) · 1))) |
108 | 73 | recnd 11002 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐺‘(𝐴 + 𝑠)) ∈ ℂ) |
109 | 108 | mulid1d 10991 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝐺‘(𝐴 + 𝑠)) · 1) = (𝐺‘(𝐴 + 𝑠))) |
110 | 109 | mpteq2dva 5179 |
. . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) · 1)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
111 | 107, 110 | eqtrd 2780 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐹‘(𝐴 + 𝑠)))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
112 | | limccl 25035 |
. . . . . . . . 9
⊢ (𝐹 limℂ 𝐴) ⊆
ℂ |
113 | 112, 46 | sselid 3924 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ ℂ) |
114 | 113 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 𝑌 ∈ ℂ) |
115 | 113 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑌 ∈ ℂ) |
116 | 58, 113 | dvmptc 25118 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝑌)) = (𝑠 ∈ ℝ ↦ 0)) |
117 | 58, 115, 82, 116, 85, 86, 44, 88 | dvmptres 25123 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑌)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 0)) |
118 | 58, 59, 73, 111, 114, 23, 117 | dvmptsub 25127 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) − 0))) |
119 | 108 | subid1d 11319 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝐺‘(𝐴 + 𝑠)) − 0) = (𝐺‘(𝐴 + 𝑠))) |
120 | 119 | mpteq2dva 5179 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐺‘(𝐴 + 𝑠)) − 0)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
121 | 118, 120 | eqtrd 2780 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
122 | 121 | dmeqd 5812 |
. . . 4
⊢ (𝜑 → dom (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))) = dom (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
123 | 73 | ralrimiva 3110 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ (0(,)(𝐵 − 𝐴))(𝐺‘(𝐴 + 𝑠)) ∈ ℝ) |
124 | | dmmptg 6143 |
. . . . 5
⊢
(∀𝑠 ∈
(0(,)(𝐵 − 𝐴))(𝐺‘(𝐴 + 𝑠)) ∈ ℝ → dom (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) = (0(,)(𝐵 − 𝐴))) |
125 | 123, 124 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) = (0(,)(𝐵 − 𝐴))) |
126 | 56, 122, 125 | 3eqtrd 2784 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝑁) = (0(,)(𝐵 − 𝐴))) |
127 | 52 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠)) |
128 | 127 | oveq2d 7285 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐷) = (ℝ D (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠))) |
129 | 128, 95 | eqtrd 2780 |
. . . . 5
⊢ (𝜑 → (ℝ D 𝐷) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)) |
130 | 129 | dmeqd 5812 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝐷) = dom (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)) |
131 | 74 | ralrimiva 3110 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ (0(,)(𝐵 − 𝐴))1 ∈ ℝ) |
132 | | dmmptg 6143 |
. . . . 5
⊢
(∀𝑠 ∈
(0(,)(𝐵 − 𝐴))1 ∈ ℝ → dom
(𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) = (0(,)(𝐵 − 𝐴))) |
133 | 131, 132 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) = (0(,)(𝐵 − 𝐴))) |
134 | 130, 133 | eqtrd 2780 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐷) = (0(,)(𝐵 − 𝐴))) |
135 | | eqid 2740 |
. . . . 5
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐹‘(𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐹‘(𝐴 + 𝑠))) |
136 | | eqid 2740 |
. . . . 5
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑌) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑌) |
137 | | eqid 2740 |
. . . . 5
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) |
138 | 38 | adantrr 714 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) ≠ 𝐴)) → (𝐴 + 𝑠) ∈ (𝐴(,)𝐵)) |
139 | | eqid 2740 |
. . . . . . . 8
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝐴) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝐴) |
140 | | eqid 2740 |
. . . . . . . 8
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠) |
141 | | eqid 2740 |
. . . . . . . 8
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠)) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠)) |
142 | 85, 42 | sstrdi 3938 |
. . . . . . . . 9
⊢ (𝜑 → (0(,)(𝐵 − 𝐴)) ⊆ ℂ) |
143 | 1 | recnd 11002 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℂ) |
144 | 139, 142,
19, 143 | constlimc 43134 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝐴) limℂ 0)) |
145 | 142, 140,
143 | idlimc 43136 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠) limℂ 0)) |
146 | 139, 140,
141, 80, 90, 144, 145 | addlimc 43158 |
. . . . . . 7
⊢ (𝜑 → (𝐴 + 0) ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠)) limℂ 0)) |
147 | 21, 146 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐴 + 𝑠)) limℂ 0)) |
148 | 100 | oveq1d 7284 |
. . . . . . 7
⊢ (𝜑 → (𝐹 limℂ 𝐴) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) limℂ 𝐴)) |
149 | 46, 148 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) limℂ 𝐴)) |
150 | | simplrr 775 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐹‘(𝐴 + 𝑠)) = 𝑌) → (𝐴 + 𝑠) = 𝐴) |
151 | 15, 30 | gtned 11108 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐴 + 𝑠) ≠ 𝐴) |
152 | 151 | neneqd 2950 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ¬ (𝐴 + 𝑠) = 𝐴) |
153 | 152 | adantrr 714 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) → ¬ (𝐴 + 𝑠) = 𝐴) |
154 | 153 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐹‘(𝐴 + 𝑠)) = 𝑌) → ¬ (𝐴 + 𝑠) = 𝐴) |
155 | 150, 154 | condan 815 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) → (𝐹‘(𝐴 + 𝑠)) = 𝑌) |
156 | 138, 76, 147, 149, 105, 155 | limcco 25053 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐹‘(𝐴 + 𝑠))) limℂ
0)) |
157 | 136, 142,
113, 143 | constlimc 43134 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑌) limℂ 0)) |
158 | 135, 136,
137, 59, 114, 156, 157 | sublimc 43162 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝑌) ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) limℂ
0)) |
159 | 113 | subidd 11318 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝑌) = 0) |
160 | 50 | eqcomi 2749 |
. . . . . 6
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) = 𝑁 |
161 | 160 | oveq1i 7279 |
. . . . 5
⊢ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) limℂ 0) = (𝑁 limℂ
0) |
162 | 161 | a1i 11 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) limℂ 0) = (𝑁 limℂ
0)) |
163 | 158, 159,
162 | 3eltr3d 2855 |
. . 3
⊢ (𝜑 → 0 ∈ (𝑁 limℂ
0)) |
164 | 142, 52, 143 | idlimc 43136 |
. . 3
⊢ (𝜑 → 0 ∈ (𝐷 limℂ
0)) |
165 | | lbioo 13107 |
. . . . 5
⊢ ¬ 0
∈ (0(,)(𝐵 −
𝐴)) |
166 | 165 | a1i 11 |
. . . 4
⊢ (𝜑 → ¬ 0 ∈ (0(,)(𝐵 − 𝐴))) |
167 | | mptresid 5956 |
. . . . . . 7
⊢ ( I
↾ (0(,)(𝐵 −
𝐴))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠) |
168 | 127, 167 | eqtr4di 2798 |
. . . . . 6
⊢ (𝜑 → 𝐷 = ( I ↾ (0(,)(𝐵 − 𝐴)))) |
169 | 168 | rneqd 5845 |
. . . . 5
⊢ (𝜑 → ran 𝐷 = ran ( I ↾ (0(,)(𝐵 − 𝐴)))) |
170 | | rnresi 5981 |
. . . . 5
⊢ ran ( I
↾ (0(,)(𝐵 −
𝐴))) = (0(,)(𝐵 − 𝐴)) |
171 | 169, 170 | eqtr2di 2797 |
. . . 4
⊢ (𝜑 → (0(,)(𝐵 − 𝐴)) = ran 𝐷) |
172 | 166, 171 | neleqtrd 2862 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ran 𝐷) |
173 | | 0ne1 12042 |
. . . . . 6
⊢ 0 ≠
1 |
174 | 173 | neii 2947 |
. . . . 5
⊢ ¬ 0
= 1 |
175 | | elsng 4581 |
. . . . . 6
⊢ (0 ∈
ℝ → (0 ∈ {1} ↔ 0 = 1)) |
176 | 1, 175 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 ∈ {1} ↔ 0 =
1)) |
177 | 174, 176 | mtbiri 327 |
. . . 4
⊢ (𝜑 → ¬ 0 ∈
{1}) |
178 | 129 | rneqd 5845 |
. . . . 5
⊢ (𝜑 → ran (ℝ D 𝐷) = ran (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)) |
179 | | eqid 2740 |
. . . . . 6
⊢ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) |
180 | 24 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ*) |
181 | | ioon0 13102 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ (𝐵 − 𝐴) ∈ ℝ*) →
((0(,)(𝐵 − 𝐴)) ≠ ∅ ↔ 0 <
(𝐵 − 𝐴))) |
182 | 180, 5, 181 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((0(,)(𝐵 − 𝐴)) ≠ ∅ ↔ 0 < (𝐵 − 𝐴))) |
183 | 8, 182 | mpbird 256 |
. . . . . 6
⊢ (𝜑 → (0(,)(𝐵 − 𝐴)) ≠ ∅) |
184 | 179, 183 | rnmptc 7077 |
. . . . 5
⊢ (𝜑 → ran (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1) = {1}) |
185 | 178, 184 | eqtr2d 2781 |
. . . 4
⊢ (𝜑 → {1} = ran (ℝ D 𝐷)) |
186 | 177, 185 | neleqtrd 2862 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐷)) |
187 | 79 | recnd 11002 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) ∈ ℂ) |
188 | | fourierdlem61.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ (𝐺 limℂ 𝐴)) |
189 | 103 | oveq1d 7284 |
. . . . . 6
⊢ (𝜑 → (𝐺 limℂ 𝐴) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥)) limℂ 𝐴)) |
190 | 188, 189 | eleqtrd 2843 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥)) limℂ 𝐴)) |
191 | | simplrr 775 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐺‘(𝐴 + 𝑠)) = 𝐸) → (𝐴 + 𝑠) = 𝐴) |
192 | 153 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) ∧ ¬ (𝐺‘(𝐴 + 𝑠)) = 𝐸) → ¬ (𝐴 + 𝑠) = 𝐴) |
193 | 191, 192 | condan 815 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐴 + 𝑠) = 𝐴)) → (𝐺‘(𝐴 + 𝑠)) = 𝐸) |
194 | 138, 187,
147, 190, 106, 193 | limcco 25053 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) limℂ
0)) |
195 | 108 | div1d 11741 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝐺‘(𝐴 + 𝑠)) / 1) = (𝐺‘(𝐴 + 𝑠))) |
196 | 54, 121 | eqtrid 2792 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D 𝑁) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
197 | 196 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (ℝ D 𝑁) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))) |
198 | 197 | fveq1d 6771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((ℝ D 𝑁)‘𝑠) = ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))‘𝑠)) |
199 | | fvmpt4 42750 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ (𝐺‘(𝐴 + 𝑠)) ∈ ℝ) → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))‘𝑠) = (𝐺‘(𝐴 + 𝑠))) |
200 | 27, 73, 199 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠)))‘𝑠) = (𝐺‘(𝐴 + 𝑠))) |
201 | 198, 200 | eqtr2d 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐺‘(𝐴 + 𝑠)) = ((ℝ D 𝑁)‘𝑠)) |
202 | 129 | fveq1d 6771 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D 𝐷)‘𝑠) = ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)‘𝑠)) |
203 | 202 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((ℝ D 𝐷)‘𝑠) = ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)‘𝑠)) |
204 | | fvmpt4 42750 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ 1 ∈ ℝ) → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)‘𝑠) = 1) |
205 | 27, 74, 204 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 1)‘𝑠) = 1) |
206 | 203, 205 | eqtr2d 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → 1 = ((ℝ D 𝐷)‘𝑠)) |
207 | 201, 206 | oveq12d 7287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝐺‘(𝐴 + 𝑠)) / 1) = (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) |
208 | 195, 207 | eqtr3d 2782 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐺‘(𝐴 + 𝑠)) = (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) |
209 | 208 | mpteq2dva 5179 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠)))) |
210 | 209 | oveq1d 7284 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (𝐺‘(𝐴 + 𝑠))) limℂ 0) = ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) limℂ
0)) |
211 | 194, 210 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) limℂ
0)) |
212 | 1, 5, 8, 51, 53, 126, 134, 163, 164, 172, 186, 211 | lhop1 25174 |
. 2
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) limℂ
0)) |
213 | 50 | fvmpt2 6881 |
. . . . . . 7
⊢ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ ((𝐹‘(𝐴 + 𝑠)) − 𝑌) ∈ ℝ) → (𝑁‘𝑠) = ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) |
214 | 27, 49, 213 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝑁‘𝑠) = ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) |
215 | 52 | fvmpt2 6881 |
. . . . . . 7
⊢ ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐷‘𝑠) = 𝑠) |
216 | 27, 27, 215 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → (𝐷‘𝑠) = 𝑠) |
217 | 214, 216 | oveq12d 7287 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (0(,)(𝐵 − 𝐴))) → ((𝑁‘𝑠) / (𝐷‘𝑠)) = (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠)) |
218 | 217 | mpteq2dva 5179 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠))) |
219 | | fourierdlem61.h |
. . . 4
⊢ 𝐻 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠)) |
220 | 218, 219 | eqtr4di 2798 |
. . 3
⊢ (𝜑 → (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) = 𝐻) |
221 | 220 | oveq1d 7284 |
. 2
⊢ (𝜑 → ((𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) limℂ 0) = (𝐻 limℂ
0)) |
222 | 212, 221 | eleqtrd 2843 |
1
⊢ (𝜑 → 𝐸 ∈ (𝐻 limℂ 0)) |