Step | Hyp | Ref
| Expression |
1 | | fourierdlem60.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | fourierdlem60.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | 1, 2 | resubcld 11260 |
. . . 4
⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ) |
4 | 3 | rexrd 10883 |
. . 3
⊢ (𝜑 → (𝐴 − 𝐵) ∈
ℝ*) |
5 | | 0red 10836 |
. . 3
⊢ (𝜑 → 0 ∈
ℝ) |
6 | | fourierdlem60.altb |
. . . 4
⊢ (𝜑 → 𝐴 < 𝐵) |
7 | 1, 2 | sublt0d 11458 |
. . . 4
⊢ (𝜑 → ((𝐴 − 𝐵) < 0 ↔ 𝐴 < 𝐵)) |
8 | 6, 7 | mpbird 260 |
. . 3
⊢ (𝜑 → (𝐴 − 𝐵) < 0) |
9 | | fourierdlem60.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
10 | 9 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
11 | 1 | rexrd 10883 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
12 | 11 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐴 ∈
ℝ*) |
13 | 2 | rexrd 10883 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
14 | 13 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐵 ∈
ℝ*) |
15 | 2 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐵 ∈ ℝ) |
16 | | elioore 12965 |
. . . . . . . . 9
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) → 𝑠 ∈ ℝ) |
17 | 16 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑠 ∈ ℝ) |
18 | 15, 17 | readdcld 10862 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) ∈ ℝ) |
19 | 2 | recnd 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
20 | 1 | recnd 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
21 | 19, 20 | pncan3d 11192 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 + (𝐴 − 𝐵)) = 𝐴) |
22 | 21 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝐵 + (𝐴 − 𝐵))) |
23 | 22 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐴 = (𝐵 + (𝐴 − 𝐵))) |
24 | 3 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐴 − 𝐵) ∈ ℝ) |
25 | 4 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐴 − 𝐵) ∈
ℝ*) |
26 | | 0xr 10880 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 0 ∈
ℝ*) |
28 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) |
29 | 25, 27, 28 | ioogtlbd 42763 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐴 − 𝐵) < 𝑠) |
30 | 24, 17, 15, 29 | ltadd2dd 10991 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + (𝐴 − 𝐵)) < (𝐵 + 𝑠)) |
31 | 23, 30 | eqbrtrd 5075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐴 < (𝐵 + 𝑠)) |
32 | | 0red 10836 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 0 ∈
ℝ) |
33 | 25, 27, 28 | iooltubd 42757 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑠 < 0) |
34 | 17, 32, 15, 33 | ltadd2dd 10991 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) < (𝐵 + 0)) |
35 | 19 | addid1d 11032 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 + 0) = 𝐵) |
36 | 35 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 0) = 𝐵) |
37 | 34, 36 | breqtrd 5079 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) < 𝐵) |
38 | 12, 14, 18, 31, 37 | eliood 42711 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) ∈ (𝐴(,)𝐵)) |
39 | 10, 38 | ffvelrnd 6905 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐹‘(𝐵 + 𝑠)) ∈ ℝ) |
40 | | ioossre 12996 |
. . . . . . . . 9
⊢ (𝐴(,)𝐵) ⊆ ℝ |
41 | 40 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
42 | | ax-resscn 10786 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
43 | 41, 42 | sstrdi 3913 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
44 | | eqid 2737 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
45 | 44, 11, 2, 6 | lptioo2cn 42861 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴(,)𝐵))) |
46 | | fourierdlem60.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐵)) |
47 | 9, 43, 45, 46 | limcrecl 42845 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ℝ) |
48 | 47 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑌 ∈ ℝ) |
49 | 39, 48 | resubcld 11260 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝐹‘(𝐵 + 𝑠)) − 𝑌) ∈ ℝ) |
50 | | fourierdlem60.n |
. . . 4
⊢ 𝑁 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) |
51 | 49, 50 | fmptd 6931 |
. . 3
⊢ (𝜑 → 𝑁:((𝐴 − 𝐵)(,)0)⟶ℝ) |
52 | | fourierdlem60.d |
. . . 4
⊢ 𝐷 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠) |
53 | 17, 52 | fmptd 6931 |
. . 3
⊢ (𝜑 → 𝐷:((𝐴 − 𝐵)(,)0)⟶ℝ) |
54 | 50 | oveq2i 7224 |
. . . . . 6
⊢ (ℝ
D 𝑁) = (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌))) |
55 | 54 | a1i 11 |
. . . . 5
⊢ (𝜑 → (ℝ D 𝑁) = (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)))) |
56 | 55 | dmeqd 5774 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝑁) = dom (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)))) |
57 | | reelprrecn 10821 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
58 | 57 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
59 | 39 | recnd 10861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐹‘(𝐵 + 𝑠)) ∈ ℂ) |
60 | | dvfre 24848 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
61 | 9, 41, 60 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
62 | | fourierdlem60.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (ℝ D 𝐹) |
63 | 62 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 = (ℝ D 𝐹)) |
64 | 63 | feq1d 6530 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺:dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)) |
65 | 61, 64 | mpbird 260 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:dom (ℝ D 𝐹)⟶ℝ) |
66 | 65 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐺:dom (ℝ D 𝐹)⟶ℝ) |
67 | 63 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) |
68 | 67 | dmeqd 5774 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (ℝ D 𝐹) = dom 𝐺) |
69 | | fourierdlem60.domg |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐺 = (𝐴(,)𝐵)) |
70 | 68, 69 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) = dom (ℝ D 𝐹)) |
71 | 70 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐴(,)𝐵) = dom (ℝ D 𝐹)) |
72 | 38, 71 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) ∈ dom (ℝ D 𝐹)) |
73 | 66, 72 | ffvelrnd 6905 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐺‘(𝐵 + 𝑠)) ∈ ℝ) |
74 | | 1red 10834 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 1 ∈
ℝ) |
75 | 9 | ffvelrnda 6904 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
76 | 75 | recnd 10861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
77 | 70 | feq2d 6531 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺:(𝐴(,)𝐵)⟶ℝ ↔ 𝐺:dom (ℝ D 𝐹)⟶ℝ)) |
78 | 65, 77 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
79 | 78 | ffvelrnda 6904 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) ∈ ℝ) |
80 | 19 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐵 ∈ ℂ) |
81 | 19 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝐵 ∈ ℂ) |
82 | | 0red 10836 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 0 ∈
ℝ) |
83 | 58, 19 | dvmptc 24855 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝐵)) = (𝑠 ∈ ℝ ↦ 0)) |
84 | | ioossre 12996 |
. . . . . . . . . . . . 13
⊢ ((𝐴 − 𝐵)(,)0) ⊆ ℝ |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 − 𝐵)(,)0) ⊆ ℝ) |
86 | | tgioo4 42786 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
87 | | iooretop 23663 |
. . . . . . . . . . . . 13
⊢ ((𝐴 − 𝐵)(,)0) ∈ (topGen‘ran
(,)) |
88 | 87 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 − 𝐵)(,)0) ∈ (topGen‘ran
(,))) |
89 | 58, 81, 82, 83, 85, 86, 44, 88 | dvmptres 24860 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝐵)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 0)) |
90 | 17 | recnd 10861 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑠 ∈ ℂ) |
91 | | recn 10819 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ → 𝑠 ∈
ℂ) |
92 | 91 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℂ) |
93 | | 1red 10834 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 1 ∈
ℝ) |
94 | 58 | dvmptid 24854 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝑠)) = (𝑠 ∈ ℝ ↦ 1)) |
95 | 58, 92, 93, 94, 85, 86, 44, 88 | dvmptres 24860 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)) |
96 | 58, 80, 32, 89, 90, 74, 95 | dvmptadd 24857 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (0 + 1))) |
97 | | 0p1e1 11952 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
98 | 97 | mpteq2i 5147 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (0 + 1)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) |
99 | 96, 98 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)) |
100 | 9 | feqmptd 6780 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) |
101 | 100 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) = 𝐹) |
102 | 101 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (ℝ D 𝐹)) |
103 | 78 | feqmptd 6780 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥))) |
104 | 102, 67, 103 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥))) |
105 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑥 = (𝐵 + 𝑠) → (𝐹‘𝑥) = (𝐹‘(𝐵 + 𝑠))) |
106 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑥 = (𝐵 + 𝑠) → (𝐺‘𝑥) = (𝐺‘(𝐵 + 𝑠))) |
107 | 58, 58, 38, 74, 76, 79, 99, 104, 105, 106 | dvmptco 24869 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐹‘(𝐵 + 𝑠)))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐺‘(𝐵 + 𝑠)) · 1))) |
108 | 73 | recnd 10861 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐺‘(𝐵 + 𝑠)) ∈ ℂ) |
109 | 108 | mulid1d 10850 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝐺‘(𝐵 + 𝑠)) · 1) = (𝐺‘(𝐵 + 𝑠))) |
110 | 109 | mpteq2dva 5150 |
. . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐺‘(𝐵 + 𝑠)) · 1)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
111 | 107, 110 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐹‘(𝐵 + 𝑠)))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
112 | | limccl 24772 |
. . . . . . . . 9
⊢ (𝐹 limℂ 𝐵) ⊆
ℂ |
113 | 112, 46 | sseldi 3899 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ ℂ) |
114 | 113 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑌 ∈ ℂ) |
115 | 113 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑌 ∈ ℂ) |
116 | 58, 113 | dvmptc 24855 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝑌)) = (𝑠 ∈ ℝ ↦ 0)) |
117 | 58, 115, 82, 116, 85, 86, 44, 88 | dvmptres 24860 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑌)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 0)) |
118 | 58, 59, 73, 111, 114, 27, 117 | dvmptsub 24864 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐺‘(𝐵 + 𝑠)) − 0))) |
119 | 108 | subid1d 11178 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝐺‘(𝐵 + 𝑠)) − 0) = (𝐺‘(𝐵 + 𝑠))) |
120 | 119 | mpteq2dva 5150 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐺‘(𝐵 + 𝑠)) − 0)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
121 | 118, 120 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
122 | 121 | dmeqd 5774 |
. . . 4
⊢ (𝜑 → dom (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌))) = dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
123 | 73 | ralrimiva 3105 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ ((𝐴 − 𝐵)(,)0)(𝐺‘(𝐵 + 𝑠)) ∈ ℝ) |
124 | | dmmptg 6105 |
. . . . 5
⊢
(∀𝑠 ∈
((𝐴 − 𝐵)(,)0)(𝐺‘(𝐵 + 𝑠)) ∈ ℝ → dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) = ((𝐴 − 𝐵)(,)0)) |
125 | 123, 124 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) = ((𝐴 − 𝐵)(,)0)) |
126 | 56, 122, 125 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝑁) = ((𝐴 − 𝐵)(,)0)) |
127 | 52 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠)) |
128 | 127 | oveq2d 7229 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐷) = (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠))) |
129 | 128, 95 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (ℝ D 𝐷) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)) |
130 | 129 | dmeqd 5774 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝐷) = dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)) |
131 | 74 | ralrimiva 3105 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ ((𝐴 − 𝐵)(,)0)1 ∈ ℝ) |
132 | | dmmptg 6105 |
. . . . 5
⊢
(∀𝑠 ∈
((𝐴 − 𝐵)(,)0)1 ∈ ℝ →
dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) = ((𝐴 − 𝐵)(,)0)) |
133 | 131, 132 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) = ((𝐴 − 𝐵)(,)0)) |
134 | 130, 133 | eqtrd 2777 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐷) = ((𝐴 − 𝐵)(,)0)) |
135 | | eqid 2737 |
. . . . 5
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐹‘(𝐵 + 𝑠))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐹‘(𝐵 + 𝑠))) |
136 | | eqid 2737 |
. . . . 5
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑌) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑌) |
137 | | eqid 2737 |
. . . . 5
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) |
138 | 38 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) ≠ 𝐵)) → (𝐵 + 𝑠) ∈ (𝐴(,)𝐵)) |
139 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝐵) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝐵) |
140 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠) |
141 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠)) |
142 | 85, 42 | sstrdi 3913 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 − 𝐵)(,)0) ⊆ ℂ) |
143 | 5 | recnd 10861 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℂ) |
144 | 139, 142,
19, 143 | constlimc 42840 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝐵) limℂ 0)) |
145 | 142, 140,
143 | idlimc 42842 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠) limℂ 0)) |
146 | 139, 140,
141, 80, 90, 144, 145 | addlimc 42864 |
. . . . . . 7
⊢ (𝜑 → (𝐵 + 0) ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠)) limℂ 0)) |
147 | 35, 146 | eqeltrrd 2839 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠)) limℂ 0)) |
148 | 100 | oveq1d 7228 |
. . . . . . 7
⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) limℂ 𝐵)) |
149 | 46, 148 | eleqtrd 2840 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) limℂ 𝐵)) |
150 | | simplrr 778 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) ∧ ¬ (𝐹‘(𝐵 + 𝑠)) = 𝑌) → (𝐵 + 𝑠) = 𝐵) |
151 | 18, 37 | ltned 10968 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) ≠ 𝐵) |
152 | 151 | neneqd 2945 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ¬ (𝐵 + 𝑠) = 𝐵) |
153 | 152 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) → ¬ (𝐵 + 𝑠) = 𝐵) |
154 | 153 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) ∧ ¬ (𝐹‘(𝐵 + 𝑠)) = 𝑌) → ¬ (𝐵 + 𝑠) = 𝐵) |
155 | 150, 154 | condan 818 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) → (𝐹‘(𝐵 + 𝑠)) = 𝑌) |
156 | 138, 76, 147, 149, 105, 155 | limcco 24790 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐹‘(𝐵 + 𝑠))) limℂ
0)) |
157 | 136, 142,
113, 143 | constlimc 42840 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑌) limℂ 0)) |
158 | 135, 136,
137, 59, 114, 156, 157 | sublimc 42868 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝑌) ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) limℂ
0)) |
159 | 113 | subidd 11177 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝑌) = 0) |
160 | 50 | eqcomi 2746 |
. . . . . 6
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) = 𝑁 |
161 | 160 | oveq1i 7223 |
. . . . 5
⊢ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) limℂ 0) = (𝑁 limℂ
0) |
162 | 161 | a1i 11 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) limℂ 0) = (𝑁 limℂ
0)) |
163 | 158, 159,
162 | 3eltr3d 2852 |
. . 3
⊢ (𝜑 → 0 ∈ (𝑁 limℂ
0)) |
164 | 142, 52, 143 | idlimc 42842 |
. . 3
⊢ (𝜑 → 0 ∈ (𝐷 limℂ
0)) |
165 | | ubioo 12967 |
. . . . 5
⊢ ¬ 0
∈ ((𝐴 − 𝐵)(,)0) |
166 | 165 | a1i 11 |
. . . 4
⊢ (𝜑 → ¬ 0 ∈ ((𝐴 − 𝐵)(,)0)) |
167 | | mptresid 5918 |
. . . . . . 7
⊢ ( I
↾ ((𝐴 − 𝐵)(,)0)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠) |
168 | 127, 167 | eqtr4di 2796 |
. . . . . 6
⊢ (𝜑 → 𝐷 = ( I ↾ ((𝐴 − 𝐵)(,)0))) |
169 | 168 | rneqd 5807 |
. . . . 5
⊢ (𝜑 → ran 𝐷 = ran ( I ↾ ((𝐴 − 𝐵)(,)0))) |
170 | | rnresi 5943 |
. . . . 5
⊢ ran ( I
↾ ((𝐴 − 𝐵)(,)0)) = ((𝐴 − 𝐵)(,)0) |
171 | 169, 170 | eqtr2di 2795 |
. . . 4
⊢ (𝜑 → ((𝐴 − 𝐵)(,)0) = ran 𝐷) |
172 | 166, 171 | neleqtrd 2859 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ran 𝐷) |
173 | | 0ne1 11901 |
. . . . . 6
⊢ 0 ≠
1 |
174 | 173 | neii 2942 |
. . . . 5
⊢ ¬ 0
= 1 |
175 | | elsng 4555 |
. . . . . 6
⊢ (0 ∈
ℝ → (0 ∈ {1} ↔ 0 = 1)) |
176 | 5, 175 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 ∈ {1} ↔ 0 =
1)) |
177 | 174, 176 | mtbiri 330 |
. . . 4
⊢ (𝜑 → ¬ 0 ∈
{1}) |
178 | 129 | rneqd 5807 |
. . . . 5
⊢ (𝜑 → ran (ℝ D 𝐷) = ran (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)) |
179 | | eqid 2737 |
. . . . . 6
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) |
180 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ*) |
181 | | ioon0 12961 |
. . . . . . . 8
⊢ (((𝐴 − 𝐵) ∈ ℝ* ∧ 0 ∈
ℝ*) → (((𝐴 − 𝐵)(,)0) ≠ ∅ ↔ (𝐴 − 𝐵) < 0)) |
182 | 4, 180, 181 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 − 𝐵)(,)0) ≠ ∅ ↔ (𝐴 − 𝐵) < 0)) |
183 | 8, 182 | mpbird 260 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 𝐵)(,)0) ≠ ∅) |
184 | 179, 183 | rnmptc 7022 |
. . . . 5
⊢ (𝜑 → ran (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) = {1}) |
185 | 178, 184 | eqtr2d 2778 |
. . . 4
⊢ (𝜑 → {1} = ran (ℝ D 𝐷)) |
186 | 177, 185 | neleqtrd 2859 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐷)) |
187 | 79 | recnd 10861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) ∈ ℂ) |
188 | | fourierdlem60.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ (𝐺 limℂ 𝐵)) |
189 | 103 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 → (𝐺 limℂ 𝐵) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥)) limℂ 𝐵)) |
190 | 188, 189 | eleqtrd 2840 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥)) limℂ 𝐵)) |
191 | | simplrr 778 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) ∧ ¬ (𝐺‘(𝐵 + 𝑠)) = 𝐸) → (𝐵 + 𝑠) = 𝐵) |
192 | 153 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) ∧ ¬ (𝐺‘(𝐵 + 𝑠)) = 𝐸) → ¬ (𝐵 + 𝑠) = 𝐵) |
193 | 191, 192 | condan 818 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) → (𝐺‘(𝐵 + 𝑠)) = 𝐸) |
194 | 138, 187,
147, 190, 106, 193 | limcco 24790 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) limℂ
0)) |
195 | 108 | div1d 11600 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝐺‘(𝐵 + 𝑠)) / 1) = (𝐺‘(𝐵 + 𝑠))) |
196 | 54, 121 | syl5eq 2790 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D 𝑁) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
197 | 196 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (ℝ D 𝑁) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
198 | 197 | fveq1d 6719 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((ℝ D 𝑁)‘𝑠) = ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))‘𝑠)) |
199 | | fvmpt4 42454 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐺‘(𝐵 + 𝑠)) ∈ ℝ) → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))‘𝑠) = (𝐺‘(𝐵 + 𝑠))) |
200 | 28, 73, 199 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))‘𝑠) = (𝐺‘(𝐵 + 𝑠))) |
201 | 198, 200 | eqtr2d 2778 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐺‘(𝐵 + 𝑠)) = ((ℝ D 𝑁)‘𝑠)) |
202 | 129 | fveq1d 6719 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D 𝐷)‘𝑠) = ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)‘𝑠)) |
203 | 202 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((ℝ D 𝐷)‘𝑠) = ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)‘𝑠)) |
204 | | fvmpt4 42454 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ 1 ∈ ℝ) →
((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)‘𝑠) = 1) |
205 | 28, 74, 204 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)‘𝑠) = 1) |
206 | 203, 205 | eqtr2d 2778 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 1 = ((ℝ D 𝐷)‘𝑠)) |
207 | 201, 206 | oveq12d 7231 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝐺‘(𝐵 + 𝑠)) / 1) = (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) |
208 | 195, 207 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐺‘(𝐵 + 𝑠)) = (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) |
209 | 208 | mpteq2dva 5150 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠)))) |
210 | 209 | oveq1d 7228 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) limℂ 0) = ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) limℂ
0)) |
211 | 194, 210 | eleqtrd 2840 |
. . 3
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) limℂ
0)) |
212 | 4, 5, 8, 51, 53, 126, 134, 163, 164, 172, 186, 211 | lhop2 24912 |
. 2
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) limℂ
0)) |
213 | 50 | fvmpt2 6829 |
. . . . . . 7
⊢ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ ((𝐹‘(𝐵 + 𝑠)) − 𝑌) ∈ ℝ) → (𝑁‘𝑠) = ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) |
214 | 28, 49, 213 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝑁‘𝑠) = ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) |
215 | 52 | fvmpt2 6829 |
. . . . . . 7
⊢ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐷‘𝑠) = 𝑠) |
216 | 28, 28, 215 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐷‘𝑠) = 𝑠) |
217 | 214, 216 | oveq12d 7231 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝑁‘𝑠) / (𝐷‘𝑠)) = (((𝐹‘(𝐵 + 𝑠)) − 𝑌) / 𝑠)) |
218 | 217 | mpteq2dva 5150 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((𝐹‘(𝐵 + 𝑠)) − 𝑌) / 𝑠))) |
219 | | fourierdlem60.h |
. . . 4
⊢ 𝐻 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((𝐹‘(𝐵 + 𝑠)) − 𝑌) / 𝑠)) |
220 | 218, 219 | eqtr4di 2796 |
. . 3
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) = 𝐻) |
221 | 220 | oveq1d 7228 |
. 2
⊢ (𝜑 → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) limℂ 0) = (𝐻 limℂ
0)) |
222 | 212, 221 | eleqtrd 2840 |
1
⊢ (𝜑 → 𝐸 ∈ (𝐻 limℂ 0)) |