Step | Hyp | Ref
| Expression |
1 | | dvferm.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
2 | | dvferm.b |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
3 | | dvfre 23714 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
4 | 1, 2, 3 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
5 | | dvferm.d |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹)) |
6 | 4, 5 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ) |
7 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → ((ℝ D 𝐹)‘𝑈) ∈ ℝ) |
8 | 7 | renegcld 10457 |
. . . . 5
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → -((ℝ D 𝐹)‘𝑈) ∈ ℝ) |
9 | 6 | lt0neg1d 10597 |
. . . . . 6
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑈) < 0 ↔ 0 < -((ℝ D 𝐹)‘𝑈))) |
10 | 9 | biimpa 501 |
. . . . 5
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → 0 < -((ℝ D 𝐹)‘𝑈)) |
11 | 8, 10 | elrpd 11869 |
. . . 4
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → -((ℝ D 𝐹)‘𝑈) ∈
ℝ+) |
12 | | dvf 23671 |
. . . . . . . . . . 11
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
13 | | ffun 6048 |
. . . . . . . . . . 11
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun
(ℝ D 𝐹)) |
14 | | funfvbrb 6330 |
. . . . . . . . . . 11
⊢ (Fun
(ℝ D 𝐹) → (𝑈 ∈ dom (ℝ D 𝐹) ↔ 𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈))) |
15 | 12, 13, 14 | mp2b 10 |
. . . . . . . . . 10
⊢ (𝑈 ∈ dom (ℝ D 𝐹) ↔ 𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈)) |
16 | 5, 15 | sylib 208 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈)) |
17 | | eqid 2622 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ℝ) =
((TopOpen‘ℂfld) ↾t
ℝ) |
18 | | eqid 2622 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
19 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) = (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) |
20 | | ax-resscn 9993 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
21 | 20 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) |
22 | | fss 6056 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑋⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:𝑋⟶ℂ) |
23 | 1, 20, 22 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
24 | 17, 18, 19, 21, 23, 2 | eldv 23662 |
. . . . . . . . 9
⊢ (𝜑 → (𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈) ↔ (𝑈 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘𝑋) ∧
((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) limℂ 𝑈)))) |
25 | 16, 24 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → (𝑈 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘𝑋) ∧
((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) limℂ 𝑈))) |
26 | 25 | simprd 479 |
. . . . . . 7
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) limℂ 𝑈)) |
27 | 26 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → ((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) limℂ 𝑈)) |
28 | 2, 20 | syl6ss 3615 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
29 | | dvferm.s |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋) |
30 | | dvferm.u |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵)) |
31 | 29, 30 | sseldd 3604 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ 𝑋) |
32 | 23, 28, 31 | dvlem 23660 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝑈})) → (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)) ∈ ℂ) |
33 | 32, 19 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))):(𝑋 ∖ {𝑈})⟶ℂ) |
34 | 33 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))):(𝑋 ∖ {𝑈})⟶ℂ) |
35 | 28 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → 𝑋 ⊆ ℂ) |
36 | 35 | ssdifssd 3748 |
. . . . . . 7
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → (𝑋 ∖ {𝑈}) ⊆ ℂ) |
37 | 28, 31 | sseldd 3604 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ ℂ) |
38 | 37 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → 𝑈 ∈ ℂ) |
39 | 34, 36, 38 | ellimc3 23643 |
. . . . . 6
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → (((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) limℂ 𝑈) ↔ (((ℝ D 𝐹)‘𝑈) ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑢 ∈
ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦)))) |
40 | 27, 39 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → (((ℝ D 𝐹)‘𝑈) ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑢 ∈
ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦))) |
41 | 40 | simprd 479 |
. . . 4
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → ∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ℝ+
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦)) |
42 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
43 | 42 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) − (𝐹‘𝑈)) = ((𝐹‘𝑧) − (𝐹‘𝑈))) |
44 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝑥 − 𝑈) = (𝑧 − 𝑈)) |
45 | 43, 44 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)) = (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈))) |
46 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) ∈ V |
47 | 45, 19, 46 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑋 ∖ {𝑈}) → ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) = (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈))) |
48 | 47 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 ∖ {𝑈}) → (((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈)) = ((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) |
49 | 48 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑋 ∖ {𝑈}) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) = (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈)))) |
50 | | id 22 |
. . . . . . . . 9
⊢ (𝑦 = -((ℝ D 𝐹)‘𝑈) → 𝑦 = -((ℝ D 𝐹)‘𝑈)) |
51 | 49, 50 | breqan12rd 4670 |
. . . . . . . 8
⊢ ((𝑦 = -((ℝ D 𝐹)‘𝑈) ∧ 𝑧 ∈ (𝑋 ∖ {𝑈})) → ((abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦 ↔ (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
52 | 51 | imbi2d 330 |
. . . . . . 7
⊢ ((𝑦 = -((ℝ D 𝐹)‘𝑈) ∧ 𝑧 ∈ (𝑋 ∖ {𝑈})) → (((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦) ↔ ((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))) |
53 | 52 | ralbidva 2985 |
. . . . . 6
⊢ (𝑦 = -((ℝ D 𝐹)‘𝑈) → (∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦) ↔ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))) |
54 | 53 | rexbidv 3052 |
. . . . 5
⊢ (𝑦 = -((ℝ D 𝐹)‘𝑈) → (∃𝑢 ∈ ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦) ↔ ∃𝑢 ∈ ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))) |
55 | 54 | rspcv 3305 |
. . . 4
⊢
(-((ℝ D 𝐹)‘𝑈) ∈ ℝ+ →
(∀𝑦 ∈
ℝ+ ∃𝑢 ∈ ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦) → ∃𝑢 ∈ ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))) |
56 | 11, 41, 55 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → ∃𝑢 ∈ ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
57 | 1 | ad3antrrr 766 |
. . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → 𝐹:𝑋⟶ℝ) |
58 | 2 | ad3antrrr 766 |
. . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → 𝑋 ⊆ ℝ) |
59 | 30 | ad3antrrr 766 |
. . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → 𝑈 ∈ (𝐴(,)𝐵)) |
60 | 29 | ad3antrrr 766 |
. . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → (𝐴(,)𝐵) ⊆ 𝑋) |
61 | 5 | ad3antrrr 766 |
. . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → 𝑈 ∈ dom (ℝ D 𝐹)) |
62 | | dvferm2.r |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) |
63 | 62 | ad3antrrr 766 |
. . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) |
64 | | simpllr 799 |
. . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → ((ℝ D 𝐹)‘𝑈) < 0) |
65 | | simplr 792 |
. . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → 𝑢 ∈ ℝ+) |
66 | | simpr 477 |
. . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
67 | | eqid 2622 |
. . . . . 6
⊢
((if(𝐴 ≤ (𝑈 − 𝑢), (𝑈 − 𝑢), 𝐴) + 𝑈) / 2) = ((if(𝐴 ≤ (𝑈 − 𝑢), (𝑈 − 𝑢), 𝐴) + 𝑈) / 2) |
68 | 57, 58, 59, 60, 61, 63, 64, 65, 66, 67 | dvferm2lem 23749 |
. . . . 5
⊢ ¬
(((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
69 | 68 | imnani 439 |
. . . 4
⊢ (((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) → ¬
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
70 | 69 | nrexdv 3001 |
. . 3
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → ¬ ∃𝑢 ∈ ℝ+
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
71 | 56, 70 | pm2.65da 600 |
. 2
⊢ (𝜑 → ¬ ((ℝ D 𝐹)‘𝑈) < 0) |
72 | | 0re 10040 |
. . 3
⊢ 0 ∈
ℝ |
73 | | lenlt 10116 |
. . 3
⊢ ((0
∈ ℝ ∧ ((ℝ D 𝐹)‘𝑈) ∈ ℝ) → (0 ≤ ((ℝ D
𝐹)‘𝑈) ↔ ¬ ((ℝ D 𝐹)‘𝑈) < 0)) |
74 | 72, 6, 73 | sylancr 695 |
. 2
⊢ (𝜑 → (0 ≤ ((ℝ D 𝐹)‘𝑈) ↔ ¬ ((ℝ D 𝐹)‘𝑈) < 0)) |
75 | 71, 74 | mpbird 247 |
1
⊢ (𝜑 → 0 ≤ ((ℝ D 𝐹)‘𝑈)) |