| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) | 
| 2 | 1 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) − (𝐹‘𝑈)) = ((𝐹‘𝑧) − (𝐹‘𝑈))) | 
| 3 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑥 − 𝑈) = (𝑧 − 𝑈)) | 
| 4 | 2, 3 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)) = (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈))) | 
| 5 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) = (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) | 
| 6 |  | ovex 7465 | . . . . . . . . . 10
⊢ (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) ∈ V | 
| 7 | 4, 5, 6 | fvmpt 7015 | . . . . . . . . 9
⊢ (𝑧 ∈ (𝑋 ∖ {𝑈}) → ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) = (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈))) | 
| 8 | 7 | fvoveq1d 7454 | . . . . . . . 8
⊢ (𝑧 ∈ (𝑋 ∖ {𝑈}) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) = (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈)))) | 
| 9 |  | id 22 | . . . . . . . 8
⊢ (𝑦 = -((ℝ D 𝐹)‘𝑈) → 𝑦 = -((ℝ D 𝐹)‘𝑈)) | 
| 10 | 8, 9 | breqan12rd 5159 | . . . . . . 7
⊢ ((𝑦 = -((ℝ D 𝐹)‘𝑈) ∧ 𝑧 ∈ (𝑋 ∖ {𝑈})) → ((abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦 ↔ (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) | 
| 11 | 10 | imbi2d 340 | . . . . . 6
⊢ ((𝑦 = -((ℝ D 𝐹)‘𝑈) ∧ 𝑧 ∈ (𝑋 ∖ {𝑈})) → (((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦) ↔ ((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))) | 
| 12 | 11 | ralbidva 3175 | . . . . 5
⊢ (𝑦 = -((ℝ D 𝐹)‘𝑈) → (∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦) ↔ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))) | 
| 13 | 12 | rexbidv 3178 | . . . 4
⊢ (𝑦 = -((ℝ D 𝐹)‘𝑈) → (∃𝑢 ∈ ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦) ↔ ∃𝑢 ∈ ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))) | 
| 14 |  | dvferm.d | . . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹)) | 
| 15 |  | dvf 25943 | . . . . . . . . . . 11
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ | 
| 16 |  | ffun 6738 | . . . . . . . . . . 11
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun
(ℝ D 𝐹)) | 
| 17 |  | funfvbrb 7070 | . . . . . . . . . . 11
⊢ (Fun
(ℝ D 𝐹) → (𝑈 ∈ dom (ℝ D 𝐹) ↔ 𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈))) | 
| 18 | 15, 16, 17 | mp2b 10 | . . . . . . . . . 10
⊢ (𝑈 ∈ dom (ℝ D 𝐹) ↔ 𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈)) | 
| 19 | 14, 18 | sylib 218 | . . . . . . . . 9
⊢ (𝜑 → 𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈)) | 
| 20 |  | eqid 2736 | . . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ℝ) =
((TopOpen‘ℂfld) ↾t
ℝ) | 
| 21 |  | eqid 2736 | . . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 22 |  | ax-resscn 11213 | . . . . . . . . . . 11
⊢ ℝ
⊆ ℂ | 
| 23 | 22 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) | 
| 24 |  | dvferm.a | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) | 
| 25 |  | fss 6751 | . . . . . . . . . . 11
⊢ ((𝐹:𝑋⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:𝑋⟶ℂ) | 
| 26 | 24, 22, 25 | sylancl 586 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) | 
| 27 |  | dvferm.b | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆ ℝ) | 
| 28 | 20, 21, 5, 23, 26, 27 | eldv 25934 | . . . . . . . . 9
⊢ (𝜑 → (𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈) ↔ (𝑈 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘𝑋) ∧
((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) limℂ 𝑈)))) | 
| 29 | 19, 28 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → (𝑈 ∈
((int‘((TopOpen‘ℂfld) ↾t
ℝ))‘𝑋) ∧
((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) limℂ 𝑈))) | 
| 30 | 29 | simprd 495 | . . . . . . 7
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) limℂ 𝑈)) | 
| 31 | 30 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → ((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) limℂ 𝑈)) | 
| 32 | 27, 22 | sstrdi 3995 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆ ℂ) | 
| 33 |  | dvferm.s | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋) | 
| 34 |  | dvferm.u | . . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵)) | 
| 35 | 33, 34 | sseldd 3983 | . . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ 𝑋) | 
| 36 | 26, 32, 35 | dvlem 25932 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝑈})) → (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)) ∈ ℂ) | 
| 37 | 36 | fmpttd 7134 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))):(𝑋 ∖ {𝑈})⟶ℂ) | 
| 38 | 37 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))):(𝑋 ∖ {𝑈})⟶ℂ) | 
| 39 | 32 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → 𝑋 ⊆ ℂ) | 
| 40 | 39 | ssdifssd 4146 | . . . . . . 7
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → (𝑋 ∖ {𝑈}) ⊆ ℂ) | 
| 41 | 32, 35 | sseldd 3983 | . . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ ℂ) | 
| 42 | 41 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → 𝑈 ∈ ℂ) | 
| 43 | 38, 40, 42 | ellimc3 25915 | . . . . . 6
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → (((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈))) limℂ 𝑈) ↔ (((ℝ D 𝐹)‘𝑈) ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑢 ∈
ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦)))) | 
| 44 | 31, 43 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → (((ℝ D 𝐹)‘𝑈) ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑢 ∈
ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦))) | 
| 45 | 44 | simprd 495 | . . . 4
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → ∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ℝ+
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹‘𝑥) − (𝐹‘𝑈)) / (𝑥 − 𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦)) | 
| 46 |  | dvfre 25990 | . . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) | 
| 47 | 24, 27, 46 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) | 
| 48 | 47, 14 | ffvelcdmd 7104 | . . . . . . 7
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ) | 
| 49 | 48 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → ((ℝ D 𝐹)‘𝑈) ∈ ℝ) | 
| 50 | 49 | renegcld 11691 | . . . . 5
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → -((ℝ D 𝐹)‘𝑈) ∈ ℝ) | 
| 51 | 48 | lt0neg1d 11833 | . . . . . 6
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑈) < 0 ↔ 0 < -((ℝ D 𝐹)‘𝑈))) | 
| 52 | 51 | biimpa 476 | . . . . 5
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → 0 < -((ℝ D 𝐹)‘𝑈)) | 
| 53 | 50, 52 | elrpd 13075 | . . . 4
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → -((ℝ D 𝐹)‘𝑈) ∈
ℝ+) | 
| 54 | 13, 45, 53 | rspcdva 3622 | . . 3
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → ∃𝑢 ∈ ℝ+ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) | 
| 55 | 24 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → 𝐹:𝑋⟶ℝ) | 
| 56 | 27 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → 𝑋 ⊆ ℝ) | 
| 57 | 34 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → 𝑈 ∈ (𝐴(,)𝐵)) | 
| 58 | 33 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → (𝐴(,)𝐵) ⊆ 𝑋) | 
| 59 | 14 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → 𝑈 ∈ dom (ℝ D 𝐹)) | 
| 60 |  | dvferm2.r | . . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) | 
| 61 | 60 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) | 
| 62 |  | simpllr 775 | . . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → ((ℝ D 𝐹)‘𝑈) < 0) | 
| 63 |  | simplr 768 | . . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → 𝑢 ∈ ℝ+) | 
| 64 |  | simpr 484 | . . . . . 6
⊢ ((((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) | 
| 65 |  | eqid 2736 | . . . . . 6
⊢
((if(𝐴 ≤ (𝑈 − 𝑢), (𝑈 − 𝑢), 𝐴) + 𝑈) / 2) = ((if(𝐴 ≤ (𝑈 − 𝑢), (𝑈 − 𝑢), 𝐴) + 𝑈) / 2) | 
| 66 | 55, 56, 57, 58, 59, 61, 62, 63, 64, 65 | dvferm2lem 26025 | . . . . 5
⊢  ¬
(((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) ∧
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) | 
| 67 | 66 | imnani 400 | . . . 4
⊢ (((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) ∧ 𝑢 ∈ ℝ+) → ¬
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) | 
| 68 | 67 | nrexdv 3148 | . . 3
⊢ ((𝜑 ∧ ((ℝ D 𝐹)‘𝑈) < 0) → ¬ ∃𝑢 ∈ ℝ+
∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑢) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) | 
| 69 | 54, 68 | pm2.65da 816 | . 2
⊢ (𝜑 → ¬ ((ℝ D 𝐹)‘𝑈) < 0) | 
| 70 |  | 0re 11264 | . . 3
⊢ 0 ∈
ℝ | 
| 71 |  | lenlt 11340 | . . 3
⊢ ((0
∈ ℝ ∧ ((ℝ D 𝐹)‘𝑈) ∈ ℝ) → (0 ≤ ((ℝ D
𝐹)‘𝑈) ↔ ¬ ((ℝ D 𝐹)‘𝑈) < 0)) | 
| 72 | 70, 48, 71 | sylancr 587 | . 2
⊢ (𝜑 → (0 ≤ ((ℝ D 𝐹)‘𝑈) ↔ ¬ ((ℝ D 𝐹)‘𝑈) < 0)) | 
| 73 | 69, 72 | mpbird 257 | 1
⊢ (𝜑 → 0 ≤ ((ℝ D 𝐹)‘𝑈)) |