Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem60.a |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
2 |
|
fourierdlem60.b |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
3 |
|
fourierdlem60.altb |
⊢ ( 𝜑 → 𝐴 < 𝐵 ) |
4 |
|
fourierdlem60.f |
⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) |
5 |
|
fourierdlem60.y |
⊢ ( 𝜑 → 𝑌 ∈ ( 𝐹 limℂ 𝐵 ) ) |
6 |
|
fourierdlem60.g |
⊢ 𝐺 = ( ℝ D 𝐹 ) |
7 |
|
fourierdlem60.domg |
⊢ ( 𝜑 → dom 𝐺 = ( 𝐴 (,) 𝐵 ) ) |
8 |
|
fourierdlem60.e |
⊢ ( 𝜑 → 𝐸 ∈ ( 𝐺 limℂ 𝐵 ) ) |
9 |
|
fourierdlem60.h |
⊢ 𝐻 = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) / 𝑠 ) ) |
10 |
|
fourierdlem60.n |
⊢ 𝑁 = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) |
11 |
|
fourierdlem60.d |
⊢ 𝐷 = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) |
12 |
1 2
|
resubcld |
⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℝ ) |
13 |
12
|
rexrd |
⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℝ* ) |
14 |
|
0red |
⊢ ( 𝜑 → 0 ∈ ℝ ) |
15 |
1 2
|
sublt0d |
⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) < 0 ↔ 𝐴 < 𝐵 ) ) |
16 |
3 15
|
mpbird |
⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) < 0 ) |
17 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) |
18 |
1
|
rexrd |
⊢ ( 𝜑 → 𝐴 ∈ ℝ* ) |
19 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐴 ∈ ℝ* ) |
20 |
2
|
rexrd |
⊢ ( 𝜑 → 𝐵 ∈ ℝ* ) |
21 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐵 ∈ ℝ* ) |
22 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐵 ∈ ℝ ) |
23 |
|
elioore |
⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) → 𝑠 ∈ ℝ ) |
24 |
23
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑠 ∈ ℝ ) |
25 |
22 24
|
readdcld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) ∈ ℝ ) |
26 |
2
|
recnd |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
27 |
1
|
recnd |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
28 |
26 27
|
pncan3d |
⊢ ( 𝜑 → ( 𝐵 + ( 𝐴 − 𝐵 ) ) = 𝐴 ) |
29 |
28
|
eqcomd |
⊢ ( 𝜑 → 𝐴 = ( 𝐵 + ( 𝐴 − 𝐵 ) ) ) |
30 |
29
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐴 = ( 𝐵 + ( 𝐴 − 𝐵 ) ) ) |
31 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐴 − 𝐵 ) ∈ ℝ ) |
32 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐴 − 𝐵 ) ∈ ℝ* ) |
33 |
|
0xr |
⊢ 0 ∈ ℝ* |
34 |
33
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 0 ∈ ℝ* ) |
35 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) |
36 |
32 34 35
|
ioogtlbd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐴 − 𝐵 ) < 𝑠 ) |
37 |
31 24 22 36
|
ltadd2dd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + ( 𝐴 − 𝐵 ) ) < ( 𝐵 + 𝑠 ) ) |
38 |
30 37
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐴 < ( 𝐵 + 𝑠 ) ) |
39 |
|
0red |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 0 ∈ ℝ ) |
40 |
32 34 35
|
iooltubd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑠 < 0 ) |
41 |
24 39 22 40
|
ltadd2dd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) < ( 𝐵 + 0 ) ) |
42 |
26
|
addid1d |
⊢ ( 𝜑 → ( 𝐵 + 0 ) = 𝐵 ) |
43 |
42
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 0 ) = 𝐵 ) |
44 |
41 43
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) < 𝐵 ) |
45 |
19 21 25 38 44
|
eliood |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) ∈ ( 𝐴 (,) 𝐵 ) ) |
46 |
17 45
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℝ ) |
47 |
|
ioossre |
⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ |
48 |
47
|
a1i |
⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) |
49 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
50 |
48 49
|
sstrdi |
⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ ) |
51 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
52 |
51 18 2 3
|
lptioo2cn |
⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ) |
53 |
4 50 52 5
|
limcrecl |
⊢ ( 𝜑 → 𝑌 ∈ ℝ ) |
54 |
53
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑌 ∈ ℝ ) |
55 |
46 54
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ∈ ℝ ) |
56 |
55 10
|
fmptd |
⊢ ( 𝜑 → 𝑁 : ( ( 𝐴 − 𝐵 ) (,) 0 ) ⟶ ℝ ) |
57 |
24 11
|
fmptd |
⊢ ( 𝜑 → 𝐷 : ( ( 𝐴 − 𝐵 ) (,) 0 ) ⟶ ℝ ) |
58 |
10
|
oveq2i |
⊢ ( ℝ D 𝑁 ) = ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) ) |
59 |
58
|
a1i |
⊢ ( 𝜑 → ( ℝ D 𝑁 ) = ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) ) ) |
60 |
59
|
dmeqd |
⊢ ( 𝜑 → dom ( ℝ D 𝑁 ) = dom ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) ) ) |
61 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
62 |
61
|
a1i |
⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } ) |
63 |
46
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℂ ) |
64 |
|
dvfre |
⊢ ( ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ) |
65 |
4 48 64
|
syl2anc |
⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ) |
66 |
6
|
a1i |
⊢ ( 𝜑 → 𝐺 = ( ℝ D 𝐹 ) ) |
67 |
66
|
feq1d |
⊢ ( 𝜑 → ( 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ) ) |
68 |
65 67
|
mpbird |
⊢ ( 𝜑 → 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ ) |
69 |
68
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ ) |
70 |
66
|
eqcomd |
⊢ ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 ) |
71 |
70
|
dmeqd |
⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = dom 𝐺 ) |
72 |
71 7
|
eqtr2d |
⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) = dom ( ℝ D 𝐹 ) ) |
73 |
72
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐴 (,) 𝐵 ) = dom ( ℝ D 𝐹 ) ) |
74 |
45 73
|
eleqtrd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) ∈ dom ( ℝ D 𝐹 ) ) |
75 |
69 74
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℝ ) |
76 |
|
1red |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 1 ∈ ℝ ) |
77 |
4
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) |
78 |
77
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ ) |
79 |
72
|
feq2d |
⊢ ( 𝜑 → ( 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ↔ 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ ) ) |
80 |
68 79
|
mpbird |
⊢ ( 𝜑 → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) |
81 |
80
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ ) |
82 |
26
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝐵 ∈ ℂ ) |
83 |
26
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 𝐵 ∈ ℂ ) |
84 |
|
0red |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 0 ∈ ℝ ) |
85 |
62 26
|
dvmptc |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ 𝐵 ) ) = ( 𝑠 ∈ ℝ ↦ 0 ) ) |
86 |
|
ioossre |
⊢ ( ( 𝐴 − 𝐵 ) (,) 0 ) ⊆ ℝ |
87 |
86
|
a1i |
⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) (,) 0 ) ⊆ ℝ ) |
88 |
|
tgioo4 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
89 |
|
iooretop |
⊢ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∈ ( topGen ‘ ran (,) ) |
90 |
89
|
a1i |
⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) (,) 0 ) ∈ ( topGen ‘ ran (,) ) ) |
91 |
62 83 84 85 87 88 51 90
|
dvmptres |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝐵 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 0 ) ) |
92 |
24
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑠 ∈ ℂ ) |
93 |
|
recn |
⊢ ( 𝑠 ∈ ℝ → 𝑠 ∈ ℂ ) |
94 |
93
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 𝑠 ∈ ℂ ) |
95 |
|
1red |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 1 ∈ ℝ ) |
96 |
62
|
dvmptid |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ 𝑠 ) ) = ( 𝑠 ∈ ℝ ↦ 1 ) ) |
97 |
62 94 95 96 87 88 51 90
|
dvmptres |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ) |
98 |
62 82 39 91 92 76 97
|
dvmptadd |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 0 + 1 ) ) ) |
99 |
|
0p1e1 |
⊢ ( 0 + 1 ) = 1 |
100 |
99
|
mpteq2i |
⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 0 + 1 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) |
101 |
98 100
|
eqtrdi |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ) |
102 |
4
|
feqmptd |
⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) |
103 |
102
|
eqcomd |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) = 𝐹 ) |
104 |
103
|
oveq2d |
⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( ℝ D 𝐹 ) ) |
105 |
80
|
feqmptd |
⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ) |
106 |
104 70 105
|
3eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ) |
107 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝐵 + 𝑠 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ) |
108 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝐵 + 𝑠 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) |
109 |
62 62 45 76 78 81 101 106 107 108
|
dvmptco |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) · 1 ) ) ) |
110 |
75
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℂ ) |
111 |
110
|
mulid1d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) · 1 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) |
112 |
111
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) · 1 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ) |
113 |
109 112
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ) |
114 |
|
limccl |
⊢ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ |
115 |
114 5
|
sselid |
⊢ ( 𝜑 → 𝑌 ∈ ℂ ) |
116 |
115
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 𝑌 ∈ ℂ ) |
117 |
115
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 𝑌 ∈ ℂ ) |
118 |
62 115
|
dvmptc |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ 𝑌 ) ) = ( 𝑠 ∈ ℝ ↦ 0 ) ) |
119 |
62 117 84 118 87 88 51 90
|
dvmptres |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑌 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 0 ) ) |
120 |
62 63 75 113 116 34 119
|
dvmptsub |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) − 0 ) ) ) |
121 |
110
|
subid1d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) − 0 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) |
122 |
121
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) − 0 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ) |
123 |
120 122
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ) |
124 |
123
|
dmeqd |
⊢ ( 𝜑 → dom ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) ) = dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ) |
125 |
75
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℝ ) |
126 |
|
dmmptg |
⊢ ( ∀ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℝ → dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) ) |
127 |
125 126
|
syl |
⊢ ( 𝜑 → dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) ) |
128 |
60 124 127
|
3eqtrd |
⊢ ( 𝜑 → dom ( ℝ D 𝑁 ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) ) |
129 |
11
|
a1i |
⊢ ( 𝜑 → 𝐷 = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) ) |
130 |
129
|
oveq2d |
⊢ ( 𝜑 → ( ℝ D 𝐷 ) = ( ℝ D ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) ) ) |
131 |
130 97
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D 𝐷 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ) |
132 |
131
|
dmeqd |
⊢ ( 𝜑 → dom ( ℝ D 𝐷 ) = dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ) |
133 |
76
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) 1 ∈ ℝ ) |
134 |
|
dmmptg |
⊢ ( ∀ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) 1 ∈ ℝ → dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) ) |
135 |
133 134
|
syl |
⊢ ( 𝜑 → dom ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) ) |
136 |
132 135
|
eqtrd |
⊢ ( 𝜑 → dom ( ℝ D 𝐷 ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) ) |
137 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ) |
138 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑌 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑌 ) |
139 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) |
140 |
45
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) ≠ 𝐵 ) ) → ( 𝐵 + 𝑠 ) ∈ ( 𝐴 (,) 𝐵 ) ) |
141 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝐵 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝐵 ) |
142 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) |
143 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) ) |
144 |
87 49
|
sstrdi |
⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) (,) 0 ) ⊆ ℂ ) |
145 |
14
|
recnd |
⊢ ( 𝜑 → 0 ∈ ℂ ) |
146 |
141 144 26 145
|
constlimc |
⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝐵 ) limℂ 0 ) ) |
147 |
144 142 145
|
idlimc |
⊢ ( 𝜑 → 0 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) limℂ 0 ) ) |
148 |
141 142 143 82 92 146 147
|
addlimc |
⊢ ( 𝜑 → ( 𝐵 + 0 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) ) limℂ 0 ) ) |
149 |
42 148
|
eqeltrrd |
⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐵 + 𝑠 ) ) limℂ 0 ) ) |
150 |
102
|
oveq1d |
⊢ ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) limℂ 𝐵 ) ) |
151 |
5 150
|
eleqtrd |
⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) limℂ 𝐵 ) ) |
152 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) ∧ ¬ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) = 𝑌 ) → ( 𝐵 + 𝑠 ) = 𝐵 ) |
153 |
25 44
|
ltned |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐵 + 𝑠 ) ≠ 𝐵 ) |
154 |
153
|
neneqd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ¬ ( 𝐵 + 𝑠 ) = 𝐵 ) |
155 |
154
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) → ¬ ( 𝐵 + 𝑠 ) = 𝐵 ) |
156 |
155
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) ∧ ¬ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) = 𝑌 ) → ¬ ( 𝐵 + 𝑠 ) = 𝐵 ) |
157 |
152 156
|
condan |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) → ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) = 𝑌 ) |
158 |
140 78 149 151 107 157
|
limcco |
⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) ) limℂ 0 ) ) |
159 |
138 144 115 145
|
constlimc |
⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑌 ) limℂ 0 ) ) |
160 |
137 138 139 63 116 158 159
|
sublimc |
⊢ ( 𝜑 → ( 𝑌 − 𝑌 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) limℂ 0 ) ) |
161 |
115
|
subidd |
⊢ ( 𝜑 → ( 𝑌 − 𝑌 ) = 0 ) |
162 |
10
|
eqcomi |
⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) = 𝑁 |
163 |
162
|
oveq1i |
⊢ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) limℂ 0 ) = ( 𝑁 limℂ 0 ) |
164 |
163
|
a1i |
⊢ ( 𝜑 → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) limℂ 0 ) = ( 𝑁 limℂ 0 ) ) |
165 |
160 161 164
|
3eltr3d |
⊢ ( 𝜑 → 0 ∈ ( 𝑁 limℂ 0 ) ) |
166 |
144 11 145
|
idlimc |
⊢ ( 𝜑 → 0 ∈ ( 𝐷 limℂ 0 ) ) |
167 |
|
ubioo |
⊢ ¬ 0 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) |
168 |
167
|
a1i |
⊢ ( 𝜑 → ¬ 0 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) |
169 |
|
mptresid |
⊢ ( I ↾ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 𝑠 ) |
170 |
129 169
|
eqtr4di |
⊢ ( 𝜑 → 𝐷 = ( I ↾ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) ) |
171 |
170
|
rneqd |
⊢ ( 𝜑 → ran 𝐷 = ran ( I ↾ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) ) |
172 |
|
rnresi |
⊢ ran ( I ↾ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) = ( ( 𝐴 − 𝐵 ) (,) 0 ) |
173 |
171 172
|
eqtr2di |
⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) (,) 0 ) = ran 𝐷 ) |
174 |
168 173
|
neleqtrd |
⊢ ( 𝜑 → ¬ 0 ∈ ran 𝐷 ) |
175 |
|
0ne1 |
⊢ 0 ≠ 1 |
176 |
175
|
neii |
⊢ ¬ 0 = 1 |
177 |
|
elsng |
⊢ ( 0 ∈ ℝ → ( 0 ∈ { 1 } ↔ 0 = 1 ) ) |
178 |
14 177
|
syl |
⊢ ( 𝜑 → ( 0 ∈ { 1 } ↔ 0 = 1 ) ) |
179 |
176 178
|
mtbiri |
⊢ ( 𝜑 → ¬ 0 ∈ { 1 } ) |
180 |
131
|
rneqd |
⊢ ( 𝜑 → ran ( ℝ D 𝐷 ) = ran ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ) |
181 |
|
eqid |
⊢ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) |
182 |
33
|
a1i |
⊢ ( 𝜑 → 0 ∈ ℝ* ) |
183 |
|
ioon0 |
⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( ( 𝐴 − 𝐵 ) (,) 0 ) ≠ ∅ ↔ ( 𝐴 − 𝐵 ) < 0 ) ) |
184 |
13 182 183
|
syl2anc |
⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) (,) 0 ) ≠ ∅ ↔ ( 𝐴 − 𝐵 ) < 0 ) ) |
185 |
16 184
|
mpbird |
⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) (,) 0 ) ≠ ∅ ) |
186 |
181 185
|
rnmptc |
⊢ ( 𝜑 → ran ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) = { 1 } ) |
187 |
180 186
|
eqtr2d |
⊢ ( 𝜑 → { 1 } = ran ( ℝ D 𝐷 ) ) |
188 |
179 187
|
neleqtrd |
⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐷 ) ) |
189 |
81
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ ) |
190 |
105
|
oveq1d |
⊢ ( 𝜑 → ( 𝐺 limℂ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) limℂ 𝐵 ) ) |
191 |
8 190
|
eleqtrd |
⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑥 ) ) limℂ 𝐵 ) ) |
192 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) ∧ ¬ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) = 𝐸 ) → ( 𝐵 + 𝑠 ) = 𝐵 ) |
193 |
155
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) ∧ ¬ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) = 𝐸 ) → ¬ ( 𝐵 + 𝑠 ) = 𝐵 ) |
194 |
192 193
|
condan |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐵 + 𝑠 ) = 𝐵 ) ) → ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) = 𝐸 ) |
195 |
140 189 149 191 108 194
|
limcco |
⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) limℂ 0 ) ) |
196 |
110
|
div1d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) / 1 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) |
197 |
58 123
|
eqtrid |
⊢ ( 𝜑 → ( ℝ D 𝑁 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ) |
198 |
197
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ℝ D 𝑁 ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ) |
199 |
198
|
fveq1d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( ℝ D 𝑁 ) ‘ 𝑠 ) = ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ‘ 𝑠 ) ) |
200 |
|
fvmpt4 |
⊢ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ∈ ℝ ) → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ‘ 𝑠 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) |
201 |
35 75 200
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) ‘ 𝑠 ) = ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) |
202 |
199 201
|
eqtr2d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) = ( ( ℝ D 𝑁 ) ‘ 𝑠 ) ) |
203 |
131
|
fveq1d |
⊢ ( 𝜑 → ( ( ℝ D 𝐷 ) ‘ 𝑠 ) = ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ‘ 𝑠 ) ) |
204 |
203
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( ℝ D 𝐷 ) ‘ 𝑠 ) = ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ‘ 𝑠 ) ) |
205 |
|
fvmpt4 |
⊢ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ 1 ∈ ℝ ) → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ‘ 𝑠 ) = 1 ) |
206 |
35 76 205
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ 1 ) ‘ 𝑠 ) = 1 ) |
207 |
204 206
|
eqtr2d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → 1 = ( ( ℝ D 𝐷 ) ‘ 𝑠 ) ) |
208 |
202 207
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) / 1 ) = ( ( ( ℝ D 𝑁 ) ‘ 𝑠 ) / ( ( ℝ D 𝐷 ) ‘ 𝑠 ) ) ) |
209 |
196 208
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) = ( ( ( ℝ D 𝑁 ) ‘ 𝑠 ) / ( ( ℝ D 𝐷 ) ‘ 𝑠 ) ) ) |
210 |
209
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( ( ℝ D 𝑁 ) ‘ 𝑠 ) / ( ( ℝ D 𝐷 ) ‘ 𝑠 ) ) ) ) |
211 |
210
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( 𝐺 ‘ ( 𝐵 + 𝑠 ) ) ) limℂ 0 ) = ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( ( ℝ D 𝑁 ) ‘ 𝑠 ) / ( ( ℝ D 𝐷 ) ‘ 𝑠 ) ) ) limℂ 0 ) ) |
212 |
195 211
|
eleqtrd |
⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( ( ℝ D 𝑁 ) ‘ 𝑠 ) / ( ( ℝ D 𝐷 ) ‘ 𝑠 ) ) ) limℂ 0 ) ) |
213 |
13 14 16 56 57 128 136 165 166 174 188 212
|
lhop2 |
⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝑁 ‘ 𝑠 ) / ( 𝐷 ‘ 𝑠 ) ) ) limℂ 0 ) ) |
214 |
10
|
fvmpt2 |
⊢ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ∈ ℝ ) → ( 𝑁 ‘ 𝑠 ) = ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) |
215 |
35 55 214
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝑁 ‘ 𝑠 ) = ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) ) |
216 |
11
|
fvmpt2 |
⊢ ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐷 ‘ 𝑠 ) = 𝑠 ) |
217 |
35 35 216
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( 𝐷 ‘ 𝑠 ) = 𝑠 ) |
218 |
215 217
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ) → ( ( 𝑁 ‘ 𝑠 ) / ( 𝐷 ‘ 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) / 𝑠 ) ) |
219 |
218
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝑁 ‘ 𝑠 ) / ( 𝐷 ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( ( 𝐹 ‘ ( 𝐵 + 𝑠 ) ) − 𝑌 ) / 𝑠 ) ) ) |
220 |
219 9
|
eqtr4di |
⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝑁 ‘ 𝑠 ) / ( 𝐷 ‘ 𝑠 ) ) ) = 𝐻 ) |
221 |
220
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝑠 ∈ ( ( 𝐴 − 𝐵 ) (,) 0 ) ↦ ( ( 𝑁 ‘ 𝑠 ) / ( 𝐷 ‘ 𝑠 ) ) ) limℂ 0 ) = ( 𝐻 limℂ 0 ) ) |
222 |
213 221
|
eleqtrd |
⊢ ( 𝜑 → 𝐸 ∈ ( 𝐻 limℂ 0 ) ) |