MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvferm1 Structured version   Visualization version   GIF version

Theorem dvferm1 23967
Description: One-sided version of dvferm 23970. A point 𝑈 which is the local maximum of its right neighborhood has derivative at most zero. (Contributed by Mario Carneiro, 24-Feb-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
Hypotheses
Ref Expression
dvferm.a (𝜑𝐹:𝑋⟶ℝ)
dvferm.b (𝜑𝑋 ⊆ ℝ)
dvferm.u (𝜑𝑈 ∈ (𝐴(,)𝐵))
dvferm.s (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)
dvferm.d (𝜑𝑈 ∈ dom (ℝ D 𝐹))
dvferm1.r (𝜑 → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹𝑦) ≤ (𝐹𝑈))
Assertion
Ref Expression
dvferm1 (𝜑 → ((ℝ D 𝐹)‘𝑈) ≤ 0)
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑦,𝐹   𝑦,𝑈   𝑦,𝑋   𝜑,𝑦

Proof of Theorem dvferm1
Dummy variables 𝑧 𝑥 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6333 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
21oveq1d 6810 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((𝐹𝑥) − (𝐹𝑈)) = ((𝐹𝑧) − (𝐹𝑈)))
3 oveq1 6802 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝑥𝑈) = (𝑧𝑈))
42, 3oveq12d 6813 . . . . . . . . . 10 (𝑥 = 𝑧 → (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)) = (((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)))
5 eqid 2771 . . . . . . . . . 10 (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈))) = (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)))
6 ovex 6826 . . . . . . . . . 10 (((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) ∈ V
74, 5, 6fvmpt 6426 . . . . . . . . 9 (𝑧 ∈ (𝑋 ∖ {𝑈}) → ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)))‘𝑧) = (((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)))
87fvoveq1d 6817 . . . . . . . 8 (𝑧 ∈ (𝑋 ∖ {𝑈}) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) = (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))))
9 id 22 . . . . . . . 8 (𝑦 = ((ℝ D 𝐹)‘𝑈) → 𝑦 = ((ℝ D 𝐹)‘𝑈))
108, 9breqan12rd 4804 . . . . . . 7 ((𝑦 = ((ℝ D 𝐹)‘𝑈) ∧ 𝑧 ∈ (𝑋 ∖ {𝑈})) → ((abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦 ↔ (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))
1110imbi2d 329 . . . . . 6 ((𝑦 = ((ℝ D 𝐹)‘𝑈) ∧ 𝑧 ∈ (𝑋 ∖ {𝑈})) → (((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦) ↔ ((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))))
1211ralbidva 3134 . . . . 5 (𝑦 = ((ℝ D 𝐹)‘𝑈) → (∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦) ↔ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))))
1312rexbidv 3200 . . . 4 (𝑦 = ((ℝ D 𝐹)‘𝑈) → (∃𝑢 ∈ ℝ+𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦) ↔ ∃𝑢 ∈ ℝ+𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))))
14 dvferm.d . . . . . . . . . 10 (𝜑𝑈 ∈ dom (ℝ D 𝐹))
15 dvf 23890 . . . . . . . . . . 11 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
16 ffun 6187 . . . . . . . . . . 11 ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun (ℝ D 𝐹))
17 funfvbrb 6475 . . . . . . . . . . 11 (Fun (ℝ D 𝐹) → (𝑈 ∈ dom (ℝ D 𝐹) ↔ 𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈)))
1815, 16, 17mp2b 10 . . . . . . . . . 10 (𝑈 ∈ dom (ℝ D 𝐹) ↔ 𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈))
1914, 18sylib 208 . . . . . . . . 9 (𝜑𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈))
20 eqid 2771 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t ℝ) = ((TopOpen‘ℂfld) ↾t ℝ)
21 eqid 2771 . . . . . . . . . 10 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
22 ax-resscn 10198 . . . . . . . . . . 11 ℝ ⊆ ℂ
2322a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
24 dvferm.a . . . . . . . . . . 11 (𝜑𝐹:𝑋⟶ℝ)
25 fss 6197 . . . . . . . . . . 11 ((𝐹:𝑋⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝑋⟶ℂ)
2624, 22, 25sylancl 574 . . . . . . . . . 10 (𝜑𝐹:𝑋⟶ℂ)
27 dvferm.b . . . . . . . . . 10 (𝜑𝑋 ⊆ ℝ)
2820, 21, 5, 23, 26, 27eldv 23881 . . . . . . . . 9 (𝜑 → (𝑈(ℝ D 𝐹)((ℝ D 𝐹)‘𝑈) ↔ (𝑈 ∈ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘𝑋) ∧ ((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈))) lim 𝑈))))
2919, 28mpbid 222 . . . . . . . 8 (𝜑 → (𝑈 ∈ ((int‘((TopOpen‘ℂfld) ↾t ℝ))‘𝑋) ∧ ((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈))) lim 𝑈)))
3029simprd 483 . . . . . . 7 (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈))) lim 𝑈))
3130adantr 466 . . . . . 6 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → ((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈))) lim 𝑈))
3227, 22syl6ss 3764 . . . . . . . . . 10 (𝜑𝑋 ⊆ ℂ)
33 dvferm.s . . . . . . . . . . 11 (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)
34 dvferm.u . . . . . . . . . . 11 (𝜑𝑈 ∈ (𝐴(,)𝐵))
3533, 34sseldd 3753 . . . . . . . . . 10 (𝜑𝑈𝑋)
3626, 32, 35dvlem 23879 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋 ∖ {𝑈})) → (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)) ∈ ℂ)
3736, 5fmptd 6529 . . . . . . . 8 (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈))):(𝑋 ∖ {𝑈})⟶ℂ)
3837adantr 466 . . . . . . 7 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → (𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈))):(𝑋 ∖ {𝑈})⟶ℂ)
3932adantr 466 . . . . . . . 8 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → 𝑋 ⊆ ℂ)
4039ssdifssd 3899 . . . . . . 7 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → (𝑋 ∖ {𝑈}) ⊆ ℂ)
4132, 35sseldd 3753 . . . . . . . 8 (𝜑𝑈 ∈ ℂ)
4241adantr 466 . . . . . . 7 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → 𝑈 ∈ ℂ)
4338, 40, 42ellimc3 23862 . . . . . 6 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → (((ℝ D 𝐹)‘𝑈) ∈ ((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈))) lim 𝑈) ↔ (((ℝ D 𝐹)‘𝑈) ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑢 ∈ ℝ+𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦))))
4431, 43mpbid 222 . . . . 5 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → (((ℝ D 𝐹)‘𝑈) ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑢 ∈ ℝ+𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦)))
4544simprd 483 . . . 4 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → ∀𝑦 ∈ ℝ+𝑢 ∈ ℝ+𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘(((𝑥 ∈ (𝑋 ∖ {𝑈}) ↦ (((𝐹𝑥) − (𝐹𝑈)) / (𝑥𝑈)))‘𝑧) − ((ℝ D 𝐹)‘𝑈))) < 𝑦))
46 dvfre 23933 . . . . . . . 8 ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
4724, 27, 46syl2anc 573 . . . . . . 7 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
4847, 14ffvelrnd 6505 . . . . . 6 (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ)
4948anim1i 602 . . . . 5 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → (((ℝ D 𝐹)‘𝑈) ∈ ℝ ∧ 0 < ((ℝ D 𝐹)‘𝑈)))
50 elrp 12036 . . . . 5 (((ℝ D 𝐹)‘𝑈) ∈ ℝ+ ↔ (((ℝ D 𝐹)‘𝑈) ∈ ℝ ∧ 0 < ((ℝ D 𝐹)‘𝑈)))
5149, 50sylibr 224 . . . 4 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → ((ℝ D 𝐹)‘𝑈) ∈ ℝ+)
5213, 45, 51rspcdva 3466 . . 3 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → ∃𝑢 ∈ ℝ+𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))
5324ad3antrrr 709 . . . . . 6 ((((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) → 𝐹:𝑋⟶ℝ)
5427ad3antrrr 709 . . . . . 6 ((((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) → 𝑋 ⊆ ℝ)
5534ad3antrrr 709 . . . . . 6 ((((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) → 𝑈 ∈ (𝐴(,)𝐵))
5633ad3antrrr 709 . . . . . 6 ((((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) → (𝐴(,)𝐵) ⊆ 𝑋)
5714ad3antrrr 709 . . . . . 6 ((((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) → 𝑈 ∈ dom (ℝ D 𝐹))
58 dvferm1.r . . . . . . 7 (𝜑 → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹𝑦) ≤ (𝐹𝑈))
5958ad3antrrr 709 . . . . . 6 ((((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹𝑦) ≤ (𝐹𝑈))
60 simpllr 760 . . . . . 6 ((((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) → 0 < ((ℝ D 𝐹)‘𝑈))
61 simplr 752 . . . . . 6 ((((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) → 𝑢 ∈ ℝ+)
62 simpr 471 . . . . . 6 ((((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))
63 eqid 2771 . . . . . 6 ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑢), 𝐵, (𝑈 + 𝑢))) / 2) = ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑢), 𝐵, (𝑈 + 𝑢))) / 2)
6453, 54, 55, 56, 57, 59, 60, 61, 62, 63dvferm1lem 23966 . . . . 5 ¬ (((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) ∧ 𝑢 ∈ ℝ+) ∧ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))
6564imnani 387 . . . 4 (((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) ∧ 𝑢 ∈ ℝ+) → ¬ ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))
6665nrexdv 3149 . . 3 ((𝜑 ∧ 0 < ((ℝ D 𝐹)‘𝑈)) → ¬ ∃𝑢 ∈ ℝ+𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑢) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))
6752, 66pm2.65da 818 . 2 (𝜑 → ¬ 0 < ((ℝ D 𝐹)‘𝑈))
68 0re 10245 . . 3 0 ∈ ℝ
69 lenlt 10321 . . 3 ((((ℝ D 𝐹)‘𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → (((ℝ D 𝐹)‘𝑈) ≤ 0 ↔ ¬ 0 < ((ℝ D 𝐹)‘𝑈)))
7048, 68, 69sylancl 574 . 2 (𝜑 → (((ℝ D 𝐹)‘𝑈) ≤ 0 ↔ ¬ 0 < ((ℝ D 𝐹)‘𝑈)))
7167, 70mpbird 247 1 (𝜑 → ((ℝ D 𝐹)‘𝑈) ≤ 0)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  cdif 3720  wss 3723  ifcif 4226  {csn 4317   class class class wbr 4787  cmpt 4864  dom cdm 5250  Fun wfun 6024  wf 6026  cfv 6030  (class class class)co 6795  cc 10139  cr 10140  0cc0 10141   + caddc 10144   < clt 10279  cle 10280  cmin 10471   / cdiv 10889  2c2 11275  +crp 12034  (,)cioo 12379  abscabs 14181  t crest 16288  TopOpenctopn 16289  fldccnfld 19960  intcnt 21041   lim climc 23845   D cdv 23846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099  ax-cnex 10197  ax-resscn 10198  ax-1cn 10199  ax-icn 10200  ax-addcl 10201  ax-addrcl 10202  ax-mulcl 10203  ax-mulrcl 10204  ax-mulcom 10205  ax-addass 10206  ax-mulass 10207  ax-distr 10208  ax-i2m1 10209  ax-1ne0 10210  ax-1rid 10211  ax-rnegex 10212  ax-rrecex 10213  ax-cnre 10214  ax-pre-lttri 10215  ax-pre-lttrn 10216  ax-pre-ltadd 10217  ax-pre-mulgt0 10218  ax-pre-sup 10219
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-riota 6756  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-om 7216  df-1st 7318  df-2nd 7319  df-wrecs 7562  df-recs 7624  df-rdg 7662  df-1o 7716  df-oadd 7720  df-er 7899  df-map 8014  df-pm 8015  df-en 8113  df-dom 8114  df-sdom 8115  df-fin 8116  df-fi 8476  df-sup 8507  df-inf 8508  df-pnf 10281  df-mnf 10282  df-xr 10283  df-ltxr 10284  df-le 10285  df-sub 10473  df-neg 10474  df-div 10890  df-nn 11226  df-2 11284  df-3 11285  df-4 11286  df-5 11287  df-6 11288  df-7 11289  df-8 11290  df-9 11291  df-n0 11499  df-z 11584  df-dec 11700  df-uz 11893  df-q 11996  df-rp 12035  df-xneg 12150  df-xadd 12151  df-xmul 12152  df-ioo 12383  df-icc 12386  df-fz 12533  df-seq 13008  df-exp 13067  df-cj 14046  df-re 14047  df-im 14048  df-sqrt 14182  df-abs 14183  df-struct 16065  df-ndx 16066  df-slot 16067  df-base 16069  df-plusg 16161  df-mulr 16162  df-starv 16163  df-tset 16167  df-ple 16168  df-ds 16171  df-unif 16172  df-rest 16290  df-topn 16291  df-topgen 16311  df-psmet 19952  df-xmet 19953  df-met 19954  df-bl 19955  df-mopn 19956  df-fbas 19957  df-fg 19958  df-cnfld 19961  df-top 20918  df-topon 20935  df-topsp 20957  df-bases 20970  df-cld 21043  df-ntr 21044  df-cls 21045  df-nei 21122  df-lp 21160  df-perf 21161  df-cn 21251  df-cnp 21252  df-haus 21339  df-fil 21869  df-fm 21961  df-flim 21962  df-flf 21963  df-xms 22344  df-ms 22345  df-cncf 22900  df-limc 23849  df-dv 23850
This theorem is referenced by:  dvferm  23970  dvivthlem1  23990
  Copyright terms: Public domain W3C validator