Step |
Hyp |
Ref |
Expression |
1 |
|
lhop2.a |
⊢ ( 𝜑 → 𝐴 ∈ ℝ* ) |
2 |
|
lhop2.b |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
3 |
|
lhop2.l |
⊢ ( 𝜑 → 𝐴 < 𝐵 ) |
4 |
|
lhop2.f |
⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) |
5 |
|
lhop2.g |
⊢ ( 𝜑 → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) |
6 |
|
lhop2.if |
⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) ) |
7 |
|
lhop2.ig |
⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) ) |
8 |
|
lhop2.f0 |
⊢ ( 𝜑 → 0 ∈ ( 𝐹 limℂ 𝐵 ) ) |
9 |
|
lhop2.g0 |
⊢ ( 𝜑 → 0 ∈ ( 𝐺 limℂ 𝐵 ) ) |
10 |
|
lhop2.gn0 |
⊢ ( 𝜑 → ¬ 0 ∈ ran 𝐺 ) |
11 |
|
lhop2.gd0 |
⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐺 ) ) |
12 |
|
lhop2.c |
⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) ) |
13 |
|
qssre |
⊢ ℚ ⊆ ℝ |
14 |
2
|
rexrd |
⊢ ( 𝜑 → 𝐵 ∈ ℝ* ) |
15 |
|
qbtwnxr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ∃ 𝑎 ∈ ℚ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) |
16 |
1 14 3 15
|
syl3anc |
⊢ ( 𝜑 → ∃ 𝑎 ∈ ℚ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) |
17 |
|
ssrexv |
⊢ ( ℚ ⊆ ℝ → ( ∃ 𝑎 ∈ ℚ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) → ∃ 𝑎 ∈ ℝ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) |
18 |
13 16 17
|
mpsyl |
⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) |
19 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) |
20 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝑎 ∈ ℝ ) |
21 |
20
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → 𝑎 ∈ ℝ ) |
22 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → 𝐵 ∈ ℝ ) |
23 |
|
elioore |
⊢ ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) → 𝑧 ∈ ℝ ) |
24 |
23
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → 𝑧 ∈ ℝ ) |
25 |
|
iooneg |
⊢ ( ( 𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↔ - 𝑧 ∈ ( - 𝐵 (,) - 𝑎 ) ) ) |
26 |
21 22 24 25
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↔ - 𝑧 ∈ ( - 𝐵 (,) - 𝑎 ) ) ) |
27 |
19 26
|
mpbid |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → - 𝑧 ∈ ( - 𝐵 (,) - 𝑎 ) ) |
28 |
27
|
adantrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ∧ - 𝑧 ≠ - 𝐵 ) ) → - 𝑧 ∈ ( - 𝐵 (,) - 𝑎 ) ) |
29 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) |
30 |
|
elioore |
⊢ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) → 𝑥 ∈ ℝ ) |
31 |
30
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → 𝑥 ∈ ℝ ) |
32 |
31
|
recnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → 𝑥 ∈ ℂ ) |
33 |
32
|
negnegd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → - - 𝑥 = 𝑥 ) |
34 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) |
35 |
33 34
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → - - 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) |
36 |
20
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → 𝑎 ∈ ℝ ) |
37 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → 𝐵 ∈ ℝ ) |
38 |
31
|
renegcld |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → - 𝑥 ∈ ℝ ) |
39 |
|
iooneg |
⊢ ( ( 𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ - 𝑥 ∈ ℝ ) → ( - 𝑥 ∈ ( 𝑎 (,) 𝐵 ) ↔ - - 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) ) |
40 |
36 37 38 39
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( - 𝑥 ∈ ( 𝑎 (,) 𝐵 ) ↔ - - 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) ) |
41 |
35 40
|
mpbird |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → - 𝑥 ∈ ( 𝑎 (,) 𝐵 ) ) |
42 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐴 ∈ ℝ* ) |
43 |
20
|
rexrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝑎 ∈ ℝ* ) |
44 |
|
simprrl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐴 < 𝑎 ) |
45 |
42 43 44
|
xrltled |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐴 ≤ 𝑎 ) |
46 |
|
iooss1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑎 ) → ( 𝑎 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) ) |
47 |
42 45 46
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑎 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) ) |
48 |
47
|
sselda |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ - 𝑥 ∈ ( 𝑎 (,) 𝐵 ) ) → - 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) |
49 |
41 48
|
syldan |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → - 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) |
50 |
29 49
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( 𝐹 ‘ - 𝑥 ) ∈ ℝ ) |
51 |
50
|
recnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( 𝐹 ‘ - 𝑥 ) ∈ ℂ ) |
52 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) |
53 |
52 49
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( 𝐺 ‘ - 𝑥 ) ∈ ℝ ) |
54 |
53
|
recnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( 𝐺 ‘ - 𝑥 ) ∈ ℂ ) |
55 |
10
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ¬ 0 ∈ ran 𝐺 ) |
56 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) |
57 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
58 |
|
fss |
⊢ ( ( 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) |
59 |
56 57 58
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) |
60 |
59
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) |
61 |
60
|
ffnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → 𝐺 Fn ( 𝐴 (,) 𝐵 ) ) |
62 |
|
fnfvelrn |
⊢ ( ( 𝐺 Fn ( 𝐴 (,) 𝐵 ) ∧ - 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ - 𝑥 ) ∈ ran 𝐺 ) |
63 |
61 49 62
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( 𝐺 ‘ - 𝑥 ) ∈ ran 𝐺 ) |
64 |
|
eleq1 |
⊢ ( ( 𝐺 ‘ - 𝑥 ) = 0 → ( ( 𝐺 ‘ - 𝑥 ) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺 ) ) |
65 |
63 64
|
syl5ibcom |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( 𝐺 ‘ - 𝑥 ) = 0 → 0 ∈ ran 𝐺 ) ) |
66 |
65
|
necon3bd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ¬ 0 ∈ ran 𝐺 → ( 𝐺 ‘ - 𝑥 ) ≠ 0 ) ) |
67 |
55 66
|
mpd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( 𝐺 ‘ - 𝑥 ) ≠ 0 ) |
68 |
51 54 67
|
divcld |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( 𝐹 ‘ - 𝑥 ) / ( 𝐺 ‘ - 𝑥 ) ) ∈ ℂ ) |
69 |
|
limcresi |
⊢ ( ( 𝑧 ∈ ℝ ↦ - 𝑧 ) limℂ 𝐵 ) ⊆ ( ( ( 𝑧 ∈ ℝ ↦ - 𝑧 ) ↾ ( 𝑎 (,) 𝐵 ) ) limℂ 𝐵 ) |
70 |
|
ioossre |
⊢ ( 𝑎 (,) 𝐵 ) ⊆ ℝ |
71 |
|
resmpt |
⊢ ( ( 𝑎 (,) 𝐵 ) ⊆ ℝ → ( ( 𝑧 ∈ ℝ ↦ - 𝑧 ) ↾ ( 𝑎 (,) 𝐵 ) ) = ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ - 𝑧 ) ) |
72 |
70 71
|
ax-mp |
⊢ ( ( 𝑧 ∈ ℝ ↦ - 𝑧 ) ↾ ( 𝑎 (,) 𝐵 ) ) = ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ - 𝑧 ) |
73 |
72
|
oveq1i |
⊢ ( ( ( 𝑧 ∈ ℝ ↦ - 𝑧 ) ↾ ( 𝑎 (,) 𝐵 ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ - 𝑧 ) limℂ 𝐵 ) |
74 |
69 73
|
sseqtri |
⊢ ( ( 𝑧 ∈ ℝ ↦ - 𝑧 ) limℂ 𝐵 ) ⊆ ( ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ - 𝑧 ) limℂ 𝐵 ) |
75 |
|
eqid |
⊢ ( 𝑧 ∈ ℝ ↦ - 𝑧 ) = ( 𝑧 ∈ ℝ ↦ - 𝑧 ) |
76 |
75
|
negcncf |
⊢ ( ℝ ⊆ ℂ → ( 𝑧 ∈ ℝ ↦ - 𝑧 ) ∈ ( ℝ –cn→ ℂ ) ) |
77 |
57 76
|
mp1i |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑧 ∈ ℝ ↦ - 𝑧 ) ∈ ( ℝ –cn→ ℂ ) ) |
78 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐵 ∈ ℝ ) |
79 |
|
negeq |
⊢ ( 𝑧 = 𝐵 → - 𝑧 = - 𝐵 ) |
80 |
77 78 79
|
cnmptlimc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → - 𝐵 ∈ ( ( 𝑧 ∈ ℝ ↦ - 𝑧 ) limℂ 𝐵 ) ) |
81 |
74 80
|
sselid |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → - 𝐵 ∈ ( ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ - 𝑧 ) limℂ 𝐵 ) ) |
82 |
78
|
renegcld |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → - 𝐵 ∈ ℝ ) |
83 |
20
|
renegcld |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → - 𝑎 ∈ ℝ ) |
84 |
83
|
rexrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → - 𝑎 ∈ ℝ* ) |
85 |
|
simprrr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝑎 < 𝐵 ) |
86 |
20 78
|
ltnegd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑎 < 𝐵 ↔ - 𝐵 < - 𝑎 ) ) |
87 |
85 86
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → - 𝐵 < - 𝑎 ) |
88 |
50
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) : ( - 𝐵 (,) - 𝑎 ) ⟶ ℝ ) |
89 |
53
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) : ( - 𝐵 (,) - 𝑎 ) ⟶ ℝ ) |
90 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
91 |
90
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ℝ ∈ { ℝ , ℂ } ) |
92 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
93 |
92
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → - 1 ∈ ℂ ) |
94 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) |
95 |
94
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) |
96 |
95
|
recnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ ) |
97 |
|
fvexd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ V ) |
98 |
|
1cnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → 1 ∈ ℂ ) |
99 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ ) |
100 |
99
|
recnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ ) |
101 |
|
1cnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℂ ) |
102 |
91
|
dvmptid |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D ( 𝑥 ∈ ℝ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ 1 ) ) |
103 |
|
ioossre |
⊢ ( - 𝐵 (,) - 𝑎 ) ⊆ ℝ |
104 |
103
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( - 𝐵 (,) - 𝑎 ) ⊆ ℝ ) |
105 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
106 |
105
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
107 |
|
iooretop |
⊢ ( - 𝐵 (,) - 𝑎 ) ∈ ( topGen ‘ ran (,) ) |
108 |
107
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( - 𝐵 (,) - 𝑎 ) ∈ ( topGen ‘ ran (,) ) ) |
109 |
91 100 101 102 104 106 105 108
|
dvmptres |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ 𝑥 ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ 1 ) ) |
110 |
91 32 98 109
|
dvmptneg |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - 𝑥 ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - 1 ) ) |
111 |
94
|
feqmptd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐹 = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑦 ) ) ) |
112 |
111
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑦 ) ) ) ) |
113 |
|
dvf |
⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ |
114 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) ) |
115 |
114
|
feq2d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) ) |
116 |
113 115
|
mpbii |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) |
117 |
116
|
feqmptd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D 𝐹 ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) |
118 |
112 117
|
eqtr3d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) |
119 |
|
fveq2 |
⊢ ( 𝑦 = - 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ - 𝑥 ) ) |
120 |
|
fveq2 |
⊢ ( 𝑦 = - 𝑥 → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) |
121 |
91 91 49 93 96 97 110 118 119 120
|
dvmptco |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) · - 1 ) ) ) |
122 |
116
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) |
123 |
122 49
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ∈ ℂ ) |
124 |
123 93
|
mulcomd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) · - 1 ) = ( - 1 · ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) ) |
125 |
123
|
mulm1d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( - 1 · ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) = - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) |
126 |
124 125
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) · - 1 ) = - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) |
127 |
126
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) · - 1 ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) ) |
128 |
121 127
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) ) |
129 |
128
|
dmeqd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → dom ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) = dom ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) ) |
130 |
|
negex |
⊢ - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ∈ V |
131 |
|
eqid |
⊢ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) |
132 |
130 131
|
dmmpti |
⊢ dom ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) = ( - 𝐵 (,) - 𝑎 ) |
133 |
129 132
|
eqtrdi |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → dom ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) = ( - 𝐵 (,) - 𝑎 ) ) |
134 |
56
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ℝ ) |
135 |
134
|
recnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ℂ ) |
136 |
|
fvexd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ∈ V ) |
137 |
56
|
feqmptd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐺 = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑦 ) ) ) |
138 |
137
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D 𝐺 ) = ( ℝ D ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑦 ) ) ) ) |
139 |
|
dvf |
⊢ ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ |
140 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) ) |
141 |
140
|
feq2d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ ↔ ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) ) |
142 |
139 141
|
mpbii |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) |
143 |
142
|
feqmptd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D 𝐺 ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) ) |
144 |
138 143
|
eqtr3d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐺 ) ‘ 𝑦 ) ) ) |
145 |
|
fveq2 |
⊢ ( 𝑦 = - 𝑥 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ - 𝑥 ) ) |
146 |
|
fveq2 |
⊢ ( 𝑦 = - 𝑥 → ( ( ℝ D 𝐺 ) ‘ 𝑦 ) = ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) |
147 |
91 91 49 93 135 136 110 144 145 146
|
dvmptco |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) · - 1 ) ) ) |
148 |
142
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) |
149 |
148 49
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ∈ ℂ ) |
150 |
149 93
|
mulcomd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) · - 1 ) = ( - 1 · ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) |
151 |
149
|
mulm1d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( - 1 · ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) = - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) |
152 |
150 151
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) · - 1 ) = - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) |
153 |
152
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) · - 1 ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) |
154 |
147 153
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) |
155 |
154
|
dmeqd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → dom ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) = dom ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) |
156 |
|
negex |
⊢ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ∈ V |
157 |
|
eqid |
⊢ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) |
158 |
156 157
|
dmmpti |
⊢ dom ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) = ( - 𝐵 (,) - 𝑎 ) |
159 |
155 158
|
eqtrdi |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → dom ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) = ( - 𝐵 (,) - 𝑎 ) ) |
160 |
49
|
adantrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ∧ - 𝑥 ≠ 𝐵 ) ) → - 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) |
161 |
|
limcresi |
⊢ ( ( 𝑥 ∈ ℝ ↦ - 𝑥 ) limℂ - 𝐵 ) ⊆ ( ( ( 𝑥 ∈ ℝ ↦ - 𝑥 ) ↾ ( - 𝐵 (,) - 𝑎 ) ) limℂ - 𝐵 ) |
162 |
|
resmpt |
⊢ ( ( - 𝐵 (,) - 𝑎 ) ⊆ ℝ → ( ( 𝑥 ∈ ℝ ↦ - 𝑥 ) ↾ ( - 𝐵 (,) - 𝑎 ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - 𝑥 ) ) |
163 |
103 162
|
ax-mp |
⊢ ( ( 𝑥 ∈ ℝ ↦ - 𝑥 ) ↾ ( - 𝐵 (,) - 𝑎 ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - 𝑥 ) |
164 |
163
|
oveq1i |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ - 𝑥 ) ↾ ( - 𝐵 (,) - 𝑎 ) ) limℂ - 𝐵 ) = ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - 𝑥 ) limℂ - 𝐵 ) |
165 |
161 164
|
sseqtri |
⊢ ( ( 𝑥 ∈ ℝ ↦ - 𝑥 ) limℂ - 𝐵 ) ⊆ ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - 𝑥 ) limℂ - 𝐵 ) |
166 |
78
|
recnd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐵 ∈ ℂ ) |
167 |
166
|
negnegd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → - - 𝐵 = 𝐵 ) |
168 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ - 𝑥 ) = ( 𝑥 ∈ ℝ ↦ - 𝑥 ) |
169 |
168
|
negcncf |
⊢ ( ℝ ⊆ ℂ → ( 𝑥 ∈ ℝ ↦ - 𝑥 ) ∈ ( ℝ –cn→ ℂ ) ) |
170 |
57 169
|
mp1i |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑥 ∈ ℝ ↦ - 𝑥 ) ∈ ( ℝ –cn→ ℂ ) ) |
171 |
|
negeq |
⊢ ( 𝑥 = - 𝐵 → - 𝑥 = - - 𝐵 ) |
172 |
170 82 171
|
cnmptlimc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → - - 𝐵 ∈ ( ( 𝑥 ∈ ℝ ↦ - 𝑥 ) limℂ - 𝐵 ) ) |
173 |
167 172
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐵 ∈ ( ( 𝑥 ∈ ℝ ↦ - 𝑥 ) limℂ - 𝐵 ) ) |
174 |
165 173
|
sselid |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐵 ∈ ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - 𝑥 ) limℂ - 𝐵 ) ) |
175 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 0 ∈ ( 𝐹 limℂ 𝐵 ) ) |
176 |
111
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝐹 limℂ 𝐵 ) = ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑦 ) ) limℂ 𝐵 ) ) |
177 |
175 176
|
eleqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 0 ∈ ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑦 ) ) limℂ 𝐵 ) ) |
178 |
|
eliooord |
⊢ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) → ( - 𝐵 < 𝑥 ∧ 𝑥 < - 𝑎 ) ) |
179 |
178
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( - 𝐵 < 𝑥 ∧ 𝑥 < - 𝑎 ) ) |
180 |
179
|
simpld |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → - 𝐵 < 𝑥 ) |
181 |
37 31 180
|
ltnegcon1d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → - 𝑥 < 𝐵 ) |
182 |
38 181
|
ltned |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → - 𝑥 ≠ 𝐵 ) |
183 |
182
|
neneqd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ¬ - 𝑥 = 𝐵 ) |
184 |
183
|
pm2.21d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( - 𝑥 = 𝐵 → ( 𝐹 ‘ - 𝑥 ) = 0 ) ) |
185 |
184
|
impr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ∧ - 𝑥 = 𝐵 ) ) → ( 𝐹 ‘ - 𝑥 ) = 0 ) |
186 |
160 96 174 177 119 185
|
limcco |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 0 ∈ ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) limℂ - 𝐵 ) ) |
187 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 0 ∈ ( 𝐺 limℂ 𝐵 ) ) |
188 |
137
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝐺 limℂ 𝐵 ) = ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑦 ) ) limℂ 𝐵 ) ) |
189 |
187 188
|
eleqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 0 ∈ ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑦 ) ) limℂ 𝐵 ) ) |
190 |
183
|
pm2.21d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( - 𝑥 = 𝐵 → ( 𝐺 ‘ - 𝑥 ) = 0 ) ) |
191 |
190
|
impr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ∧ - 𝑥 = 𝐵 ) ) → ( 𝐺 ‘ - 𝑥 ) = 0 ) |
192 |
160 135 174 189 145 191
|
limcco |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 0 ∈ ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) limℂ - 𝐵 ) ) |
193 |
63
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) : ( - 𝐵 (,) - 𝑎 ) ⟶ ran 𝐺 ) |
194 |
193
|
frnd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ran ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ⊆ ran 𝐺 ) |
195 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ¬ 0 ∈ ran 𝐺 ) |
196 |
194 195
|
ssneldd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ¬ 0 ∈ ran ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) |
197 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ¬ 0 ∈ ran ( ℝ D 𝐺 ) ) |
198 |
154
|
rneqd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ran ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) = ran ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) |
199 |
198
|
eleq2d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 0 ∈ ran ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ↔ 0 ∈ ran ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) ) |
200 |
157 156
|
elrnmpti |
⊢ ( 0 ∈ ran ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ↔ ∃ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) 0 = - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) |
201 |
|
eqcom |
⊢ ( 0 = - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ↔ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) = 0 ) |
202 |
149
|
negeq0d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) = 0 ↔ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) = 0 ) ) |
203 |
148
|
ffnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) ) |
204 |
|
fnfvelrn |
⊢ ( ( ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) ∧ - 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ∈ ran ( ℝ D 𝐺 ) ) |
205 |
203 49 204
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ∈ ran ( ℝ D 𝐺 ) ) |
206 |
|
eleq1 |
⊢ ( ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) = 0 → ( ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ∈ ran ( ℝ D 𝐺 ) ↔ 0 ∈ ran ( ℝ D 𝐺 ) ) ) |
207 |
205 206
|
syl5ibcom |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) = 0 → 0 ∈ ran ( ℝ D 𝐺 ) ) ) |
208 |
202 207
|
sylbird |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) = 0 → 0 ∈ ran ( ℝ D 𝐺 ) ) ) |
209 |
201 208
|
syl5bi |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( 0 = - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) → 0 ∈ ran ( ℝ D 𝐺 ) ) ) |
210 |
209
|
rexlimdva |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ∃ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) 0 = - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) → 0 ∈ ran ( ℝ D 𝐺 ) ) ) |
211 |
200 210
|
syl5bi |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 0 ∈ ran ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) → 0 ∈ ran ( ℝ D 𝐺 ) ) ) |
212 |
199 211
|
sylbid |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 0 ∈ ran ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) → 0 ∈ ran ( ℝ D 𝐺 ) ) ) |
213 |
197 212
|
mtod |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ¬ 0 ∈ ran ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ) |
214 |
116
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ ℂ ) |
215 |
142
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ∈ ℂ ) |
216 |
11
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 0 ∈ ran ( ℝ D 𝐺 ) ) |
217 |
142
|
ffnd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) ) |
218 |
|
fnfvelrn |
⊢ ( ( ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ∈ ran ( ℝ D 𝐺 ) ) |
219 |
217 218
|
sylan |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ∈ ran ( ℝ D 𝐺 ) ) |
220 |
|
eleq1 |
⊢ ( ( ( ℝ D 𝐺 ) ‘ 𝑧 ) = 0 → ( ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ∈ ran ( ℝ D 𝐺 ) ↔ 0 ∈ ran ( ℝ D 𝐺 ) ) ) |
221 |
219 220
|
syl5ibcom |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D 𝐺 ) ‘ 𝑧 ) = 0 → 0 ∈ ran ( ℝ D 𝐺 ) ) ) |
222 |
221
|
necon3bd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ¬ 0 ∈ ran ( ℝ D 𝐺 ) → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ≠ 0 ) ) |
223 |
216 222
|
mpd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ≠ 0 ) |
224 |
214 215 223
|
divcld |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ∈ ℂ ) |
225 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) ) |
226 |
|
fveq2 |
⊢ ( 𝑧 = - 𝑥 → ( ( ℝ D 𝐹 ) ‘ 𝑧 ) = ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) |
227 |
|
fveq2 |
⊢ ( 𝑧 = - 𝑥 → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) = ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) |
228 |
226 227
|
oveq12d |
⊢ ( 𝑧 = - 𝑥 → ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) = ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) / ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) |
229 |
183
|
pm2.21d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( - 𝑥 = 𝐵 → ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) / ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) = 𝐶 ) ) |
230 |
229
|
impr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ∧ - 𝑥 = 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) / ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) = 𝐶 ) |
231 |
160 224 174 225 228 230
|
limcco |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐶 ∈ ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) / ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) limℂ - 𝐵 ) ) |
232 |
|
nfcv |
⊢ Ⅎ 𝑥 ℝ |
233 |
|
nfcv |
⊢ Ⅎ 𝑥 D |
234 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) |
235 |
232 233 234
|
nfov |
⊢ Ⅎ 𝑥 ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) |
236 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑦 |
237 |
235 236
|
nffv |
⊢ Ⅎ 𝑥 ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) |
238 |
|
nfcv |
⊢ Ⅎ 𝑥 / |
239 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) |
240 |
232 233 239
|
nfov |
⊢ Ⅎ 𝑥 ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) |
241 |
240 236
|
nffv |
⊢ Ⅎ 𝑥 ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) |
242 |
237 238 241
|
nfov |
⊢ Ⅎ 𝑥 ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) ) |
243 |
|
nfcv |
⊢ Ⅎ 𝑦 ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) ) |
244 |
|
fveq2 |
⊢ ( 𝑦 = 𝑥 → ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) = ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) ) |
245 |
|
fveq2 |
⊢ ( 𝑦 = 𝑥 → ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) = ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) ) |
246 |
244 245
|
oveq12d |
⊢ ( 𝑦 = 𝑥 → ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) ) = ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) ) ) |
247 |
242 243 246
|
cbvmpt |
⊢ ( 𝑦 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) ) ) |
248 |
128
|
fveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) ‘ 𝑥 ) ) |
249 |
131
|
fvmpt2 |
⊢ ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ∧ - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ∈ V ) → ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) ‘ 𝑥 ) = - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) |
250 |
130 249
|
mpan2 |
⊢ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) → ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) ‘ 𝑥 ) = - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) |
251 |
248 250
|
sylan9eq |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) = - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) ) |
252 |
154
|
fveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ‘ 𝑥 ) ) |
253 |
157
|
fvmpt2 |
⊢ ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ∧ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ∈ V ) → ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ‘ 𝑥 ) = - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) |
254 |
156 253
|
mpan2 |
⊢ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) → ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ‘ 𝑥 ) = - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) |
255 |
252 254
|
sylan9eq |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) = - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) |
256 |
251 255
|
oveq12d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) ) = ( - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) / - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) |
257 |
11
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ¬ 0 ∈ ran ( ℝ D 𝐺 ) ) |
258 |
207
|
necon3bd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ¬ 0 ∈ ran ( ℝ D 𝐺 ) → ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ≠ 0 ) ) |
259 |
257 258
|
mpd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ≠ 0 ) |
260 |
123 149 259
|
div2negd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( - ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) / - ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) = ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) / ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) |
261 |
256 260
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) ) = ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) / ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) |
262 |
261
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) / ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) ) |
263 |
247 262
|
eqtrid |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑦 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) / ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) ) |
264 |
263
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑦 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) ) ) limℂ - 𝐵 ) = ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ - 𝑥 ) / ( ( ℝ D 𝐺 ) ‘ - 𝑥 ) ) ) limℂ - 𝐵 ) ) |
265 |
231 264
|
eleqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐶 ∈ ( ( 𝑦 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) / ( ( ℝ D ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ) ‘ 𝑦 ) ) ) limℂ - 𝐵 ) ) |
266 |
82 84 87 88 89 133 159 186 192 196 213 265
|
lhop1 |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐶 ∈ ( ( 𝑦 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑦 ) / ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑦 ) ) ) limℂ - 𝐵 ) ) |
267 |
|
nffvmpt1 |
⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑦 ) |
268 |
|
nffvmpt1 |
⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑦 ) |
269 |
267 238 268
|
nfov |
⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑦 ) / ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑦 ) ) |
270 |
|
nfcv |
⊢ Ⅎ 𝑦 ( ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑥 ) / ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑥 ) ) |
271 |
|
fveq2 |
⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑥 ) ) |
272 |
|
fveq2 |
⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑥 ) ) |
273 |
271 272
|
oveq12d |
⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑦 ) / ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑦 ) ) = ( ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑥 ) / ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑥 ) ) ) |
274 |
269 270 273
|
cbvmpt |
⊢ ( 𝑦 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑦 ) / ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑥 ) / ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑥 ) ) ) |
275 |
|
fvex |
⊢ ( 𝐹 ‘ - 𝑥 ) ∈ V |
276 |
|
eqid |
⊢ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) |
277 |
276
|
fvmpt2 |
⊢ ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ∧ ( 𝐹 ‘ - 𝑥 ) ∈ V ) → ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ - 𝑥 ) ) |
278 |
34 275 277
|
sylancl |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ - 𝑥 ) ) |
279 |
|
fvex |
⊢ ( 𝐺 ‘ - 𝑥 ) ∈ V |
280 |
|
eqid |
⊢ ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) |
281 |
280
|
fvmpt2 |
⊢ ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ∧ ( 𝐺 ‘ - 𝑥 ) ∈ V ) → ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑥 ) = ( 𝐺 ‘ - 𝑥 ) ) |
282 |
34 279 281
|
sylancl |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑥 ) = ( 𝐺 ‘ - 𝑥 ) ) |
283 |
278 282
|
oveq12d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ) → ( ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑥 ) / ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ - 𝑥 ) / ( 𝐺 ‘ - 𝑥 ) ) ) |
284 |
283
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑥 ) / ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( 𝐹 ‘ - 𝑥 ) / ( 𝐺 ‘ - 𝑥 ) ) ) ) |
285 |
274 284
|
eqtrid |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑦 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑦 ) / ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( 𝐹 ‘ - 𝑥 ) / ( 𝐺 ‘ - 𝑥 ) ) ) ) |
286 |
285
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑦 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐹 ‘ - 𝑥 ) ) ‘ 𝑦 ) / ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( 𝐺 ‘ - 𝑥 ) ) ‘ 𝑦 ) ) ) limℂ - 𝐵 ) = ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( 𝐹 ‘ - 𝑥 ) / ( 𝐺 ‘ - 𝑥 ) ) ) limℂ - 𝐵 ) ) |
287 |
266 286
|
eleqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐶 ∈ ( ( 𝑥 ∈ ( - 𝐵 (,) - 𝑎 ) ↦ ( ( 𝐹 ‘ - 𝑥 ) / ( 𝐺 ‘ - 𝑥 ) ) ) limℂ - 𝐵 ) ) |
288 |
|
negeq |
⊢ ( 𝑥 = - 𝑧 → - 𝑥 = - - 𝑧 ) |
289 |
288
|
fveq2d |
⊢ ( 𝑥 = - 𝑧 → ( 𝐹 ‘ - 𝑥 ) = ( 𝐹 ‘ - - 𝑧 ) ) |
290 |
288
|
fveq2d |
⊢ ( 𝑥 = - 𝑧 → ( 𝐺 ‘ - 𝑥 ) = ( 𝐺 ‘ - - 𝑧 ) ) |
291 |
289 290
|
oveq12d |
⊢ ( 𝑥 = - 𝑧 → ( ( 𝐹 ‘ - 𝑥 ) / ( 𝐺 ‘ - 𝑥 ) ) = ( ( 𝐹 ‘ - - 𝑧 ) / ( 𝐺 ‘ - - 𝑧 ) ) ) |
292 |
82
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → - 𝐵 ∈ ℝ ) |
293 |
|
eliooord |
⊢ ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) → ( 𝑎 < 𝑧 ∧ 𝑧 < 𝐵 ) ) |
294 |
293
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → ( 𝑎 < 𝑧 ∧ 𝑧 < 𝐵 ) ) |
295 |
294
|
simprd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → 𝑧 < 𝐵 ) |
296 |
24 22
|
ltnegd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → ( 𝑧 < 𝐵 ↔ - 𝐵 < - 𝑧 ) ) |
297 |
295 296
|
mpbid |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → - 𝐵 < - 𝑧 ) |
298 |
292 297
|
gtned |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → - 𝑧 ≠ - 𝐵 ) |
299 |
298
|
neneqd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → ¬ - 𝑧 = - 𝐵 ) |
300 |
299
|
pm2.21d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → ( - 𝑧 = - 𝐵 → ( ( 𝐹 ‘ - - 𝑧 ) / ( 𝐺 ‘ - - 𝑧 ) ) = 𝐶 ) ) |
301 |
300
|
impr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ∧ - 𝑧 = - 𝐵 ) ) → ( ( 𝐹 ‘ - - 𝑧 ) / ( 𝐺 ‘ - - 𝑧 ) ) = 𝐶 ) |
302 |
28 68 81 287 291 301
|
limcco |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ - - 𝑧 ) / ( 𝐺 ‘ - - 𝑧 ) ) ) limℂ 𝐵 ) ) |
303 |
24
|
recnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → 𝑧 ∈ ℂ ) |
304 |
303
|
negnegd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → - - 𝑧 = 𝑧 ) |
305 |
304
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → ( 𝐹 ‘ - - 𝑧 ) = ( 𝐹 ‘ 𝑧 ) ) |
306 |
304
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → ( 𝐺 ‘ - - 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) |
307 |
305 306
|
oveq12d |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ) → ( ( 𝐹 ‘ - - 𝑧 ) / ( 𝐺 ‘ - - 𝑧 ) ) = ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) |
308 |
307
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ - - 𝑧 ) / ( 𝐺 ‘ - - 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ) |
309 |
308
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ - - 𝑧 ) / ( 𝐺 ‘ - - 𝑧 ) ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) ) |
310 |
47
|
resmptd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( 𝑎 (,) 𝐵 ) ) = ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ) |
311 |
310
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( 𝑎 (,) 𝐵 ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) ) |
312 |
|
fss |
⊢ ( ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) |
313 |
94 57 312
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) |
314 |
313
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) |
315 |
59
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) |
316 |
10
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 0 ∈ ran 𝐺 ) |
317 |
56
|
ffnd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐺 Fn ( 𝐴 (,) 𝐵 ) ) |
318 |
|
fnfvelrn |
⊢ ( ( 𝐺 Fn ( 𝐴 (,) 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 ) |
319 |
317 318
|
sylan |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 ) |
320 |
|
eleq1 |
⊢ ( ( 𝐺 ‘ 𝑧 ) = 0 → ( ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 ↔ 0 ∈ ran 𝐺 ) ) |
321 |
319 320
|
syl5ibcom |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐺 ‘ 𝑧 ) = 0 → 0 ∈ ran 𝐺 ) ) |
322 |
321
|
necon3bd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ¬ 0 ∈ ran 𝐺 → ( 𝐺 ‘ 𝑧 ) ≠ 0 ) ) |
323 |
316 322
|
mpd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 ) |
324 |
314 315 323
|
divcld |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ ) |
325 |
324
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) |
326 |
|
ioossre |
⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ |
327 |
326 57
|
sstri |
⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ |
328 |
327
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ℂ ) |
329 |
|
eqid |
⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) |
330 |
|
ssun2 |
⊢ { 𝐵 } ⊆ ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) |
331 |
|
snssg |
⊢ ( 𝐵 ∈ ℝ → ( 𝐵 ∈ ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) |
332 |
78 331
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝐵 ∈ ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) |
333 |
330 332
|
mpbiri |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐵 ∈ ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ) |
334 |
105
|
cnfldtopon |
⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) |
335 |
326
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) |
336 |
78
|
snssd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → { 𝐵 } ⊆ ℝ ) |
337 |
335 336
|
unssd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ⊆ ℝ ) |
338 |
337 57
|
sstrdi |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ⊆ ℂ ) |
339 |
|
resttopon |
⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) |
340 |
334 338 339
|
sylancr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) |
341 |
|
topontop |
⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ∈ Top ) |
342 |
340 341
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ∈ Top ) |
343 |
|
indi |
⊢ ( ( 𝑎 (,) +∞ ) ∩ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) = ( ( ( 𝑎 (,) +∞ ) ∩ ( 𝐴 (,) 𝐵 ) ) ∪ ( ( 𝑎 (,) +∞ ) ∩ { 𝐵 } ) ) |
344 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
345 |
344
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → +∞ ∈ ℝ* ) |
346 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐵 ∈ ℝ* ) |
347 |
|
iooin |
⊢ ( ( ( 𝑎 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ) → ( ( 𝑎 (,) +∞ ) ∩ ( 𝐴 (,) 𝐵 ) ) = ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( +∞ ≤ 𝐵 , +∞ , 𝐵 ) ) ) |
348 |
43 345 42 346 347
|
syl22anc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑎 (,) +∞ ) ∩ ( 𝐴 (,) 𝐵 ) ) = ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( +∞ ≤ 𝐵 , +∞ , 𝐵 ) ) ) |
349 |
|
xrltnle |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑎 ∈ ℝ* ) → ( 𝐴 < 𝑎 ↔ ¬ 𝑎 ≤ 𝐴 ) ) |
350 |
42 43 349
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝐴 < 𝑎 ↔ ¬ 𝑎 ≤ 𝐴 ) ) |
351 |
44 350
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ¬ 𝑎 ≤ 𝐴 ) |
352 |
351
|
iffalsed |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) = 𝑎 ) |
353 |
78
|
ltpnfd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐵 < +∞ ) |
354 |
|
xrltnle |
⊢ ( ( 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵 ) ) |
355 |
346 344 354
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝐵 < +∞ ↔ ¬ +∞ ≤ 𝐵 ) ) |
356 |
353 355
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ¬ +∞ ≤ 𝐵 ) |
357 |
356
|
iffalsed |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → if ( +∞ ≤ 𝐵 , +∞ , 𝐵 ) = 𝐵 ) |
358 |
352 357
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( if ( 𝑎 ≤ 𝐴 , 𝐴 , 𝑎 ) (,) if ( +∞ ≤ 𝐵 , +∞ , 𝐵 ) ) = ( 𝑎 (,) 𝐵 ) ) |
359 |
348 358
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑎 (,) +∞ ) ∩ ( 𝐴 (,) 𝐵 ) ) = ( 𝑎 (,) 𝐵 ) ) |
360 |
|
elioopnf |
⊢ ( 𝑎 ∈ ℝ* → ( 𝐵 ∈ ( 𝑎 (,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑎 < 𝐵 ) ) ) |
361 |
43 360
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝐵 ∈ ( 𝑎 (,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑎 < 𝐵 ) ) ) |
362 |
78 85 361
|
mpbir2and |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐵 ∈ ( 𝑎 (,) +∞ ) ) |
363 |
362
|
snssd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → { 𝐵 } ⊆ ( 𝑎 (,) +∞ ) ) |
364 |
|
sseqin2 |
⊢ ( { 𝐵 } ⊆ ( 𝑎 (,) +∞ ) ↔ ( ( 𝑎 (,) +∞ ) ∩ { 𝐵 } ) = { 𝐵 } ) |
365 |
363 364
|
sylib |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑎 (,) +∞ ) ∩ { 𝐵 } ) = { 𝐵 } ) |
366 |
359 365
|
uneq12d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( ( 𝑎 (,) +∞ ) ∩ ( 𝐴 (,) 𝐵 ) ) ∪ ( ( 𝑎 (,) +∞ ) ∩ { 𝐵 } ) ) = ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ) |
367 |
343 366
|
eqtrid |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑎 (,) +∞ ) ∩ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) = ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ) |
368 |
|
retop |
⊢ ( topGen ‘ ran (,) ) ∈ Top |
369 |
|
reex |
⊢ ℝ ∈ V |
370 |
369
|
ssex |
⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ⊆ ℝ → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∈ V ) |
371 |
337 370
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∈ V ) |
372 |
|
iooretop |
⊢ ( 𝑎 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) |
373 |
372
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( 𝑎 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) ) |
374 |
|
elrestr |
⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∈ V ∧ ( 𝑎 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) ) → ( ( 𝑎 (,) +∞ ) ∩ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) |
375 |
368 371 373 374
|
mp3an2i |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑎 (,) +∞ ) ∩ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) |
376 |
367 375
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) |
377 |
|
eqid |
⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) ) |
378 |
105 377
|
rerest |
⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) |
379 |
337 378
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) |
380 |
376 379
|
eleqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) |
381 |
|
isopn3i |
⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ∈ Top ∧ ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) ‘ ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ) = ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ) |
382 |
342 380 381
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) ‘ ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ) = ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ) |
383 |
333 382
|
eleqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐵 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) ‘ ( ( 𝑎 (,) 𝐵 ) ∪ { 𝐵 } ) ) ) |
384 |
325 47 328 105 329 383
|
limcres |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( 𝑎 (,) 𝐵 ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) ) |
385 |
309 311 384
|
3eqtr2d |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → ( ( 𝑧 ∈ ( 𝑎 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ - - 𝑧 ) / ( 𝐺 ‘ - - 𝑧 ) ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) ) |
386 |
302 385
|
eleqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ ( 𝐴 < 𝑎 ∧ 𝑎 < 𝐵 ) ) ) → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) ) |
387 |
18 386
|
rexlimddv |
⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) ) |