Step | Hyp | Ref
| Expression |
1 | | fourierdlem60.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | fourierdlem60.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | 1, 2 | resubcld 10869 |
. . . 4
⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ) |
4 | 3 | rexrd 10490 |
. . 3
⊢ (𝜑 → (𝐴 − 𝐵) ∈
ℝ*) |
5 | | 0red 10443 |
. . 3
⊢ (𝜑 → 0 ∈
ℝ) |
6 | | fourierdlem60.altb |
. . . 4
⊢ (𝜑 → 𝐴 < 𝐵) |
7 | 1, 2 | sublt0d 11067 |
. . . 4
⊢ (𝜑 → ((𝐴 − 𝐵) < 0 ↔ 𝐴 < 𝐵)) |
8 | 6, 7 | mpbird 249 |
. . 3
⊢ (𝜑 → (𝐴 − 𝐵) < 0) |
9 | | fourierdlem60.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
10 | 9 | adantr 473 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
11 | 1 | rexrd 10490 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
12 | 11 | adantr 473 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐴 ∈
ℝ*) |
13 | 2 | rexrd 10490 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
14 | 13 | adantr 473 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐵 ∈
ℝ*) |
15 | 2 | adantr 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐵 ∈ ℝ) |
16 | | elioore 12584 |
. . . . . . . . 9
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) → 𝑠 ∈ ℝ) |
17 | 16 | adantl 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑠 ∈ ℝ) |
18 | 15, 17 | readdcld 10469 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) ∈ ℝ) |
19 | 2 | recnd 10468 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
20 | 1 | recnd 10468 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
21 | 19, 20 | pncan3d 10801 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 + (𝐴 − 𝐵)) = 𝐴) |
22 | 21 | eqcomd 2784 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝐵 + (𝐴 − 𝐵))) |
23 | 22 | adantr 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐴 = (𝐵 + (𝐴 − 𝐵))) |
24 | 3 | adantr 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐴 − 𝐵) ∈ ℝ) |
25 | 4 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐴 − 𝐵) ∈
ℝ*) |
26 | | 0xr 10487 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 0 ∈
ℝ*) |
28 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) |
29 | | ioogtlb 41207 |
. . . . . . . . . 10
⊢ (((𝐴 − 𝐵) ∈ ℝ* ∧ 0 ∈
ℝ* ∧ 𝑠
∈ ((𝐴 − 𝐵)(,)0)) → (𝐴 − 𝐵) < 𝑠) |
30 | 25, 27, 28, 29 | syl3anc 1351 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐴 − 𝐵) < 𝑠) |
31 | 24, 17, 15, 30 | ltadd2dd 10599 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + (𝐴 − 𝐵)) < (𝐵 + 𝑠)) |
32 | 23, 31 | eqbrtrd 4951 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐴 < (𝐵 + 𝑠)) |
33 | | 0red 10443 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 0 ∈
ℝ) |
34 | | iooltub 41223 |
. . . . . . . . . 10
⊢ (((𝐴 − 𝐵) ∈ ℝ* ∧ 0 ∈
ℝ* ∧ 𝑠
∈ ((𝐴 − 𝐵)(,)0)) → 𝑠 < 0) |
35 | 25, 27, 28, 34 | syl3anc 1351 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑠 < 0) |
36 | 17, 33, 15, 35 | ltadd2dd 10599 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) < (𝐵 + 0)) |
37 | 19 | addid1d 10640 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 + 0) = 𝐵) |
38 | 37 | adantr 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 0) = 𝐵) |
39 | 36, 38 | breqtrd 4955 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) < 𝐵) |
40 | 12, 14, 18, 32, 39 | eliood 41210 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) ∈ (𝐴(,)𝐵)) |
41 | 10, 40 | ffvelrnd 6677 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐹‘(𝐵 + 𝑠)) ∈ ℝ) |
42 | | ioossre 12614 |
. . . . . . . . 9
⊢ (𝐴(,)𝐵) ⊆ ℝ |
43 | 42 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
44 | | ax-resscn 10392 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
45 | 43, 44 | syl6ss 3870 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
46 | | eqid 2778 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
47 | 46, 11, 2, 6 | lptioo2cn 41363 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴(,)𝐵))) |
48 | | fourierdlem60.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐵)) |
49 | 9, 45, 47, 48 | limcrecl 41347 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ℝ) |
50 | 49 | adantr 473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑌 ∈ ℝ) |
51 | 41, 50 | resubcld 10869 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝐹‘(𝐵 + 𝑠)) − 𝑌) ∈ ℝ) |
52 | | fourierdlem60.n |
. . . 4
⊢ 𝑁 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) |
53 | 51, 52 | fmptd 6701 |
. . 3
⊢ (𝜑 → 𝑁:((𝐴 − 𝐵)(,)0)⟶ℝ) |
54 | | fourierdlem60.d |
. . . 4
⊢ 𝐷 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠) |
55 | 17, 54 | fmptd 6701 |
. . 3
⊢ (𝜑 → 𝐷:((𝐴 − 𝐵)(,)0)⟶ℝ) |
56 | 52 | oveq2i 6987 |
. . . . . 6
⊢ (ℝ
D 𝑁) = (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌))) |
57 | 56 | a1i 11 |
. . . . 5
⊢ (𝜑 → (ℝ D 𝑁) = (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)))) |
58 | 57 | dmeqd 5624 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝑁) = dom (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)))) |
59 | | reelprrecn 10427 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
60 | 59 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
61 | 41 | recnd 10468 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐹‘(𝐵 + 𝑠)) ∈ ℂ) |
62 | | dvfre 24251 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
63 | 9, 43, 62 | syl2anc 576 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
64 | | fourierdlem60.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (ℝ D 𝐹) |
65 | 64 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 = (ℝ D 𝐹)) |
66 | 65 | feq1d 6329 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺:dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)) |
67 | 63, 66 | mpbird 249 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:dom (ℝ D 𝐹)⟶ℝ) |
68 | 67 | adantr 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐺:dom (ℝ D 𝐹)⟶ℝ) |
69 | 65 | eqcomd 2784 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) |
70 | 69 | dmeqd 5624 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (ℝ D 𝐹) = dom 𝐺) |
71 | | fourierdlem60.domg |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐺 = (𝐴(,)𝐵)) |
72 | 70, 71 | eqtr2d 2815 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) = dom (ℝ D 𝐹)) |
73 | 72 | adantr 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐴(,)𝐵) = dom (ℝ D 𝐹)) |
74 | 40, 73 | eleqtrd 2868 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) ∈ dom (ℝ D 𝐹)) |
75 | 68, 74 | ffvelrnd 6677 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐺‘(𝐵 + 𝑠)) ∈ ℝ) |
76 | | 1red 10440 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 1 ∈
ℝ) |
77 | 9 | ffvelrnda 6676 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
78 | 77 | recnd 10468 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
79 | 72 | feq2d 6330 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺:(𝐴(,)𝐵)⟶ℝ ↔ 𝐺:dom (ℝ D 𝐹)⟶ℝ)) |
80 | 67, 79 | mpbird 249 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
81 | 80 | ffvelrnda 6676 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) ∈ ℝ) |
82 | 19 | adantr 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝐵 ∈ ℂ) |
83 | 19 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝐵 ∈ ℂ) |
84 | | 0red 10443 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 0 ∈
ℝ) |
85 | 60, 19 | dvmptc 24258 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝐵)) = (𝑠 ∈ ℝ ↦ 0)) |
86 | | ioossre 12614 |
. . . . . . . . . . . . 13
⊢ ((𝐴 − 𝐵)(,)0) ⊆ ℝ |
87 | 86 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 − 𝐵)(,)0) ⊆ ℝ) |
88 | 46 | tgioo2 23114 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
89 | | iooretop 23077 |
. . . . . . . . . . . . 13
⊢ ((𝐴 − 𝐵)(,)0) ∈ (topGen‘ran
(,)) |
90 | 89 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 − 𝐵)(,)0) ∈ (topGen‘ran
(,))) |
91 | 60, 83, 84, 85, 87, 88, 46, 90 | dvmptres 24263 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝐵)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 0)) |
92 | 17 | recnd 10468 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑠 ∈ ℂ) |
93 | | recn 10425 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ → 𝑠 ∈
ℂ) |
94 | 93 | adantl 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℂ) |
95 | | 1red 10440 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 1 ∈
ℝ) |
96 | 60 | dvmptid 24257 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝑠)) = (𝑠 ∈ ℝ ↦ 1)) |
97 | 60, 94, 95, 96, 87, 88, 46, 90 | dvmptres 24263 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)) |
98 | 60, 82, 33, 91, 92, 76, 97 | dvmptadd 24260 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (0 + 1))) |
99 | | 0p1e1 11569 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
100 | 99 | mpteq2i 5019 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (0 + 1)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) |
101 | 98, 100 | syl6eq 2830 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)) |
102 | 9 | feqmptd 6562 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) |
103 | 102 | eqcomd 2784 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) = 𝐹) |
104 | 103 | oveq2d 6992 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (ℝ D 𝐹)) |
105 | 80 | feqmptd 6562 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥))) |
106 | 104, 69, 105 | 3eqtrd 2818 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥))) |
107 | | fveq2 6499 |
. . . . . . . . 9
⊢ (𝑥 = (𝐵 + 𝑠) → (𝐹‘𝑥) = (𝐹‘(𝐵 + 𝑠))) |
108 | | fveq2 6499 |
. . . . . . . . 9
⊢ (𝑥 = (𝐵 + 𝑠) → (𝐺‘𝑥) = (𝐺‘(𝐵 + 𝑠))) |
109 | 60, 60, 40, 76, 78, 81, 101, 106, 107, 108 | dvmptco 24272 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐹‘(𝐵 + 𝑠)))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐺‘(𝐵 + 𝑠)) · 1))) |
110 | 75 | recnd 10468 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐺‘(𝐵 + 𝑠)) ∈ ℂ) |
111 | 110 | mulid1d 10457 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝐺‘(𝐵 + 𝑠)) · 1) = (𝐺‘(𝐵 + 𝑠))) |
112 | 111 | mpteq2dva 5022 |
. . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐺‘(𝐵 + 𝑠)) · 1)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
113 | 109, 112 | eqtrd 2814 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐹‘(𝐵 + 𝑠)))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
114 | | limccl 24176 |
. . . . . . . . 9
⊢ (𝐹 limℂ 𝐵) ⊆
ℂ |
115 | 114, 48 | sseldi 3856 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ ℂ) |
116 | 115 | adantr 473 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 𝑌 ∈ ℂ) |
117 | 115 | adantr 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑌 ∈ ℂ) |
118 | 60, 115 | dvmptc 24258 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝑌)) = (𝑠 ∈ ℝ ↦ 0)) |
119 | 60, 117, 84, 118, 87, 88, 46, 90 | dvmptres 24263 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑌)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 0)) |
120 | 60, 61, 75, 113, 116, 27, 119 | dvmptsub 24267 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐺‘(𝐵 + 𝑠)) − 0))) |
121 | 110 | subid1d 10787 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝐺‘(𝐵 + 𝑠)) − 0) = (𝐺‘(𝐵 + 𝑠))) |
122 | 121 | mpteq2dva 5022 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐺‘(𝐵 + 𝑠)) − 0)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
123 | 120, 122 | eqtrd 2814 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
124 | 123 | dmeqd 5624 |
. . . 4
⊢ (𝜑 → dom (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌))) = dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
125 | 75 | ralrimiva 3132 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ ((𝐴 − 𝐵)(,)0)(𝐺‘(𝐵 + 𝑠)) ∈ ℝ) |
126 | | dmmptg 5935 |
. . . . 5
⊢
(∀𝑠 ∈
((𝐴 − 𝐵)(,)0)(𝐺‘(𝐵 + 𝑠)) ∈ ℝ → dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) = ((𝐴 − 𝐵)(,)0)) |
127 | 125, 126 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) = ((𝐴 − 𝐵)(,)0)) |
128 | 58, 124, 127 | 3eqtrd 2818 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝑁) = ((𝐴 − 𝐵)(,)0)) |
129 | 54 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠)) |
130 | 129 | oveq2d 6992 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐷) = (ℝ D (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠))) |
131 | 130, 97 | eqtrd 2814 |
. . . . 5
⊢ (𝜑 → (ℝ D 𝐷) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)) |
132 | 131 | dmeqd 5624 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝐷) = dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)) |
133 | 76 | ralrimiva 3132 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ ((𝐴 − 𝐵)(,)0)1 ∈ ℝ) |
134 | | dmmptg 5935 |
. . . . 5
⊢
(∀𝑠 ∈
((𝐴 − 𝐵)(,)0)1 ∈ ℝ →
dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) = ((𝐴 − 𝐵)(,)0)) |
135 | 133, 134 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) = ((𝐴 − 𝐵)(,)0)) |
136 | 132, 135 | eqtrd 2814 |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐷) = ((𝐴 − 𝐵)(,)0)) |
137 | | eqid 2778 |
. . . . 5
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐹‘(𝐵 + 𝑠))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐹‘(𝐵 + 𝑠))) |
138 | | eqid 2778 |
. . . . 5
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑌) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑌) |
139 | | eqid 2778 |
. . . . 5
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) |
140 | 40 | adantrr 704 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) ≠ 𝐵)) → (𝐵 + 𝑠) ∈ (𝐴(,)𝐵)) |
141 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝐵) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝐵) |
142 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠) |
143 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠)) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠)) |
144 | 87, 44 | syl6ss 3870 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 − 𝐵)(,)0) ⊆ ℂ) |
145 | 5 | recnd 10468 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℂ) |
146 | 141, 144,
19, 145 | constlimc 41342 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝐵) limℂ 0)) |
147 | 144, 142,
145 | idlimc 41344 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠) limℂ 0)) |
148 | 141, 142,
143, 82, 92, 146, 147 | addlimc 41366 |
. . . . . . 7
⊢ (𝜑 → (𝐵 + 0) ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠)) limℂ 0)) |
149 | 37, 148 | eqeltrrd 2867 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐵 + 𝑠)) limℂ 0)) |
150 | 102 | oveq1d 6991 |
. . . . . . 7
⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) limℂ 𝐵)) |
151 | 48, 150 | eleqtrd 2868 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) limℂ 𝐵)) |
152 | | simplrr 765 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) ∧ ¬ (𝐹‘(𝐵 + 𝑠)) = 𝑌) → (𝐵 + 𝑠) = 𝐵) |
153 | 18, 39 | ltned 10576 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐵 + 𝑠) ≠ 𝐵) |
154 | 153 | neneqd 2972 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ¬ (𝐵 + 𝑠) = 𝐵) |
155 | 154 | adantrr 704 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) → ¬ (𝐵 + 𝑠) = 𝐵) |
156 | 155 | adantr 473 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) ∧ ¬ (𝐹‘(𝐵 + 𝑠)) = 𝑌) → ¬ (𝐵 + 𝑠) = 𝐵) |
157 | 152, 156 | condan 805 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) → (𝐹‘(𝐵 + 𝑠)) = 𝑌) |
158 | 140, 78, 149, 151, 107, 157 | limcco 24194 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐹‘(𝐵 + 𝑠))) limℂ
0)) |
159 | 138, 144,
115, 145 | constlimc 41342 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑌) limℂ 0)) |
160 | 137, 138,
139, 61, 116, 158, 159 | sublimc 41370 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝑌) ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) limℂ
0)) |
161 | 115 | subidd 10786 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝑌) = 0) |
162 | 52 | eqcomi 2787 |
. . . . . 6
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) = 𝑁 |
163 | 162 | oveq1i 6986 |
. . . . 5
⊢ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) limℂ 0) = (𝑁 limℂ
0) |
164 | 163 | a1i 11 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) limℂ 0) = (𝑁 limℂ
0)) |
165 | 160, 161,
164 | 3eltr3d 2880 |
. . 3
⊢ (𝜑 → 0 ∈ (𝑁 limℂ
0)) |
166 | 144, 54, 145 | idlimc 41344 |
. . 3
⊢ (𝜑 → 0 ∈ (𝐷 limℂ
0)) |
167 | | ubioo 12586 |
. . . . 5
⊢ ¬ 0
∈ ((𝐴 − 𝐵)(,)0) |
168 | 167 | a1i 11 |
. . . 4
⊢ (𝜑 → ¬ 0 ∈ ((𝐴 − 𝐵)(,)0)) |
169 | | mptresid 5762 |
. . . . . . 7
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠) = ( I ↾ ((𝐴 − 𝐵)(,)0)) |
170 | 129, 169 | syl6eq 2830 |
. . . . . 6
⊢ (𝜑 → 𝐷 = ( I ↾ ((𝐴 − 𝐵)(,)0))) |
171 | 170 | rneqd 5651 |
. . . . 5
⊢ (𝜑 → ran 𝐷 = ran ( I ↾ ((𝐴 − 𝐵)(,)0))) |
172 | | rnresi 5783 |
. . . . 5
⊢ ran ( I
↾ ((𝐴 − 𝐵)(,)0)) = ((𝐴 − 𝐵)(,)0) |
173 | 171, 172 | syl6req 2831 |
. . . 4
⊢ (𝜑 → ((𝐴 − 𝐵)(,)0) = ran 𝐷) |
174 | 168, 173 | neleqtrd 2887 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ran 𝐷) |
175 | | 0ne1 11511 |
. . . . . 6
⊢ 0 ≠
1 |
176 | 175 | neii 2969 |
. . . . 5
⊢ ¬ 0
= 1 |
177 | | elsng 4455 |
. . . . . 6
⊢ (0 ∈
ℝ → (0 ∈ {1} ↔ 0 = 1)) |
178 | 5, 177 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 ∈ {1} ↔ 0 =
1)) |
179 | 176, 178 | mtbiri 319 |
. . . 4
⊢ (𝜑 → ¬ 0 ∈
{1}) |
180 | 131 | rneqd 5651 |
. . . . 5
⊢ (𝜑 → ran (ℝ D 𝐷) = ran (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)) |
181 | | eqid 2778 |
. . . . . 6
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) |
182 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ*) |
183 | | ioon0 12580 |
. . . . . . . 8
⊢ (((𝐴 − 𝐵) ∈ ℝ* ∧ 0 ∈
ℝ*) → (((𝐴 − 𝐵)(,)0) ≠ ∅ ↔ (𝐴 − 𝐵) < 0)) |
184 | 4, 182, 183 | syl2anc 576 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 − 𝐵)(,)0) ≠ ∅ ↔ (𝐴 − 𝐵) < 0)) |
185 | 8, 184 | mpbird 249 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 𝐵)(,)0) ≠ ∅) |
186 | 181, 76, 185 | rnmptc 6796 |
. . . . 5
⊢ (𝜑 → ran (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1) = {1}) |
187 | 180, 186 | eqtr2d 2815 |
. . . 4
⊢ (𝜑 → {1} = ran (ℝ D 𝐷)) |
188 | 179, 187 | neleqtrd 2887 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐷)) |
189 | 81 | recnd 10468 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) ∈ ℂ) |
190 | | fourierdlem60.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ (𝐺 limℂ 𝐵)) |
191 | 105 | oveq1d 6991 |
. . . . . 6
⊢ (𝜑 → (𝐺 limℂ 𝐵) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥)) limℂ 𝐵)) |
192 | 190, 191 | eleqtrd 2868 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ ((𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥)) limℂ 𝐵)) |
193 | | simplrr 765 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) ∧ ¬ (𝐺‘(𝐵 + 𝑠)) = 𝐸) → (𝐵 + 𝑠) = 𝐵) |
194 | 155 | adantr 473 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) ∧ ¬ (𝐺‘(𝐵 + 𝑠)) = 𝐸) → ¬ (𝐵 + 𝑠) = 𝐵) |
195 | 193, 194 | condan 805 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐵 + 𝑠) = 𝐵)) → (𝐺‘(𝐵 + 𝑠)) = 𝐸) |
196 | 140, 189,
149, 192, 108, 195 | limcco 24194 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) limℂ
0)) |
197 | 110 | div1d 11209 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝐺‘(𝐵 + 𝑠)) / 1) = (𝐺‘(𝐵 + 𝑠))) |
198 | 56, 123 | syl5eq 2826 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D 𝑁) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
199 | 198 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (ℝ D 𝑁) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))) |
200 | 199 | fveq1d 6501 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((ℝ D 𝑁)‘𝑠) = ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))‘𝑠)) |
201 | | eqid 2778 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) |
202 | 201 | fvmpt2 6605 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ (𝐺‘(𝐵 + 𝑠)) ∈ ℝ) → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))‘𝑠) = (𝐺‘(𝐵 + 𝑠))) |
203 | 28, 75, 202 | syl2anc 576 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠)))‘𝑠) = (𝐺‘(𝐵 + 𝑠))) |
204 | 200, 203 | eqtr2d 2815 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐺‘(𝐵 + 𝑠)) = ((ℝ D 𝑁)‘𝑠)) |
205 | 131 | fveq1d 6501 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D 𝐷)‘𝑠) = ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)‘𝑠)) |
206 | 205 | adantr 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((ℝ D 𝐷)‘𝑠) = ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)‘𝑠)) |
207 | 181 | fvmpt2 6605 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ 1 ∈ ℝ) →
((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)‘𝑠) = 1) |
208 | 28, 76, 207 | syl2anc 576 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 1)‘𝑠) = 1) |
209 | 206, 208 | eqtr2d 2815 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → 1 = ((ℝ D 𝐷)‘𝑠)) |
210 | 204, 209 | oveq12d 6994 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝐺‘(𝐵 + 𝑠)) / 1) = (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) |
211 | 197, 210 | eqtr3d 2816 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐺‘(𝐵 + 𝑠)) = (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) |
212 | 211 | mpteq2dva 5022 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠)))) |
213 | 212 | oveq1d 6991 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (𝐺‘(𝐵 + 𝑠))) limℂ 0) = ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) limℂ
0)) |
214 | 196, 213 | eleqtrd 2868 |
. . 3
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((ℝ D 𝑁)‘𝑠) / ((ℝ D 𝐷)‘𝑠))) limℂ
0)) |
215 | 4, 5, 8, 53, 55, 128, 136, 165, 166, 174, 188, 214 | lhop2 24315 |
. 2
⊢ (𝜑 → 𝐸 ∈ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) limℂ
0)) |
216 | 52 | fvmpt2 6605 |
. . . . . . 7
⊢ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ ((𝐹‘(𝐵 + 𝑠)) − 𝑌) ∈ ℝ) → (𝑁‘𝑠) = ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) |
217 | 28, 51, 216 | syl2anc 576 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝑁‘𝑠) = ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) |
218 | 54 | fvmpt2 6605 |
. . . . . . 7
⊢ ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐷‘𝑠) = 𝑠) |
219 | 28, 28, 218 | syl2anc 576 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → (𝐷‘𝑠) = 𝑠) |
220 | 217, 219 | oveq12d 6994 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ((𝐴 − 𝐵)(,)0)) → ((𝑁‘𝑠) / (𝐷‘𝑠)) = (((𝐹‘(𝐵 + 𝑠)) − 𝑌) / 𝑠)) |
221 | 220 | mpteq2dva 5022 |
. . . 4
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((𝐹‘(𝐵 + 𝑠)) − 𝑌) / 𝑠))) |
222 | | fourierdlem60.h |
. . . 4
⊢ 𝐻 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((𝐹‘(𝐵 + 𝑠)) − 𝑌) / 𝑠)) |
223 | 221, 222 | syl6eqr 2832 |
. . 3
⊢ (𝜑 → (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) = 𝐻) |
224 | 223 | oveq1d 6991 |
. 2
⊢ (𝜑 → ((𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝑁‘𝑠) / (𝐷‘𝑠))) limℂ 0) = (𝐻 limℂ
0)) |
225 | 215, 224 | eleqtrd 2868 |
1
⊢ (𝜑 → 𝐸 ∈ (𝐻 limℂ 0)) |