Proof of Theorem dvferm2lem
Step | Hyp | Ref
| Expression |
1 | | dvferm.u |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵)) |
2 | | ne0i 3921 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅) |
3 | | ndmioo 12202 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → (𝐴(,)𝐵) = ∅) |
4 | 3 | necon1ai 2821 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
5 | 1, 2, 4 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
6 | 5 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
7 | | eliooord 12233 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵)) |
8 | 1, 7 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵)) |
9 | 8 | simprd 479 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 < 𝐵) |
10 | | ioossre 12235 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴(,)𝐵) ⊆ ℝ |
11 | 10, 1 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈 ∈ ℝ) |
12 | 11 | rexrd 10089 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 ∈
ℝ*) |
13 | | xrltle 11982 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑈 < 𝐵 → 𝑈 ≤ 𝐵)) |
14 | 12, 6, 13 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 < 𝐵 → 𝑈 ≤ 𝐵)) |
15 | 9, 14 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ≤ 𝐵) |
16 | | iooss2 12211 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ*
∧ 𝑈 ≤ 𝐵) → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵)) |
17 | 6, 15, 16 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵)) |
18 | | dvferm.s |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋) |
19 | 17, 18 | sstrd 3613 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴(,)𝑈) ⊆ 𝑋) |
20 | | dvferm2.x |
. . . . . . . . . . . . . 14
⊢ 𝑆 = ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) |
21 | | mnfxr 10096 |
. . . . . . . . . . . . . . . . . 18
⊢ -∞
∈ ℝ* |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → -∞ ∈
ℝ*) |
23 | | dvferm2.t |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
24 | 23 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑇 ∈ ℝ) |
25 | 11, 24 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑈 − 𝑇) ∈ ℝ) |
26 | 25 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑈 − 𝑇) ∈
ℝ*) |
27 | 5 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
28 | 26, 27 | ifcld 4131 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈
ℝ*) |
29 | | mnflt 11957 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 − 𝑇) ∈ ℝ → -∞ < (𝑈 − 𝑇)) |
30 | 25, 29 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → -∞ < (𝑈 − 𝑇)) |
31 | | xrmax2 12007 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℝ*
∧ (𝑈 − 𝑇) ∈ ℝ*)
→ (𝑈 − 𝑇) ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
32 | 27, 26, 31 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑈 − 𝑇) ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
33 | 22, 26, 28, 30, 32 | xrltletrd 11992 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → -∞ < if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
34 | 11, 23 | ltsubrpd 11904 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑈 − 𝑇) < 𝑈) |
35 | 8 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 < 𝑈) |
36 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 − 𝑇) = if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) → ((𝑈 − 𝑇) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)) |
37 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 = if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) → (𝐴 < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)) |
38 | 36, 37 | ifboth 4124 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑈 − 𝑇) < 𝑈 ∧ 𝐴 < 𝑈) → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈) |
39 | 34, 35, 38 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈) |
40 | | xrre2 12001 |
. . . . . . . . . . . . . . . . 17
⊢
(((-∞ ∈ ℝ* ∧ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ* ∧ 𝑈 ∈ ℝ*)
∧ (-∞ < if(𝐴
≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∧ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)) → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ) |
41 | 22, 28, 12, 33, 39, 40 | syl32anc 1334 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ) |
42 | 41, 11 | readdcld 10069 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) ∈ ℝ) |
43 | 42 | rehalfcld 11279 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) ∈ ℝ) |
44 | 20, 43 | syl5eqel 2705 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ ℝ) |
45 | 44 | rexrd 10089 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
46 | | xrmax1 12006 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ (𝑈 − 𝑇) ∈ ℝ*)
→ 𝐴 ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
47 | 27, 26, 46 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
48 | | avglt1 11270 |
. . . . . . . . . . . . . . . . 17
⊢
((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ ∧ 𝑈 ∈ ℝ) → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2))) |
49 | 41, 11, 48 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2))) |
50 | 39, 49 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2)) |
51 | 50, 20 | syl6breqr 4695 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑆) |
52 | 27, 28, 45, 47, 51 | xrlelttrd 11991 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 < 𝑆) |
53 | | avglt2 11271 |
. . . . . . . . . . . . . . . 16
⊢
((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ ∧ 𝑈 ∈ ℝ) → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈)) |
54 | 41, 11, 53 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈)) |
55 | 39, 54 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈) |
56 | 20, 55 | syl5eqbr 4688 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 < 𝑈) |
57 | | elioo2 12216 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝑈 ∈
ℝ*) → (𝑆 ∈ (𝐴(,)𝑈) ↔ (𝑆 ∈ ℝ ∧ 𝐴 < 𝑆 ∧ 𝑆 < 𝑈))) |
58 | 27, 12, 57 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ∈ (𝐴(,)𝑈) ↔ (𝑆 ∈ ℝ ∧ 𝐴 < 𝑆 ∧ 𝑆 < 𝑈))) |
59 | 44, 52, 56, 58 | mpbir3and 1245 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ (𝐴(,)𝑈)) |
60 | 19, 59 | sseldd 3604 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ 𝑋) |
61 | 44, 56 | ltned 10173 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ≠ 𝑈) |
62 | | eldifsn 4317 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (𝑋 ∖ {𝑈}) ↔ (𝑆 ∈ 𝑋 ∧ 𝑆 ≠ 𝑈)) |
63 | 60, 61, 62 | sylanbrc 698 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ (𝑋 ∖ {𝑈})) |
64 | | dvferm2.l |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
65 | 44, 11, 56 | ltled 10185 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ≤ 𝑈) |
66 | 44, 11, 65 | abssuble0d 14171 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) = (𝑈 − 𝑆)) |
67 | 25, 41, 44, 32, 51 | lelttrd 10195 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 − 𝑇) < 𝑆) |
68 | 11, 24, 44, 67 | ltsub23d 10632 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 − 𝑆) < 𝑇) |
69 | 66, 68 | eqbrtrd 4675 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) < 𝑇) |
70 | 61, 69 | jca 554 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇)) |
71 | | neeq1 2856 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (𝑧 ≠ 𝑈 ↔ 𝑆 ≠ 𝑈)) |
72 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑆 → (𝑧 − 𝑈) = (𝑆 − 𝑈)) |
73 | 72 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑆 → (abs‘(𝑧 − 𝑈)) = (abs‘(𝑆 − 𝑈))) |
74 | 73 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → ((abs‘(𝑧 − 𝑈)) < 𝑇 ↔ (abs‘(𝑆 − 𝑈)) < 𝑇)) |
75 | 71, 74 | anbi12d 747 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → ((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) ↔ (𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇))) |
76 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑆 → (𝐹‘𝑧) = (𝐹‘𝑆)) |
77 | 76 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑆 → ((𝐹‘𝑧) − (𝐹‘𝑈)) = ((𝐹‘𝑆) − (𝐹‘𝑈))) |
78 | 77, 72 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑆 → (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) = (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) |
79 | 78 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑆 → ((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈)) = ((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) |
80 | 79 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) = (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈)))) |
81 | 80 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → ((abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈) ↔ (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
82 | 75, 81 | imbi12d 334 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → (((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)) ↔ ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))) |
83 | 82 | rspcv 3305 |
. . . . . . . . . 10
⊢ (𝑆 ∈ (𝑋 ∖ {𝑈}) → (∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)) → ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))) |
84 | 63, 64, 70, 83 | syl3c 66 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)) |
85 | | dvferm.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
86 | 85, 60 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ) |
87 | 18, 1 | sseldd 3604 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ 𝑋) |
88 | 85, 87 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑈) ∈ ℝ) |
89 | 86, 88 | resubcld 10458 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ) |
90 | 44, 11 | resubcld 10458 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 − 𝑈) ∈ ℝ) |
91 | 44 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ ℂ) |
92 | 11 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ ℂ) |
93 | 91, 92, 61 | subne0d 10401 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 − 𝑈) ≠ 0) |
94 | 89, 90, 93 | redivcld 10853 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∈ ℝ) |
95 | | dvferm.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
96 | | dvfre 23714 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
97 | 85, 95, 96 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
98 | | dvferm.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹)) |
99 | 97, 98 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ) |
100 | 99 | renegcld 10457 |
. . . . . . . . . 10
⊢ (𝜑 → -((ℝ D 𝐹)‘𝑈) ∈ ℝ) |
101 | 94, 99, 100 | absdifltd 14172 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈) ↔ ((((ℝ D 𝐹)‘𝑈) − -((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈))))) |
102 | 84, 101 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → ((((ℝ D 𝐹)‘𝑈) − -((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)))) |
103 | 102 | simprd 479 |
. . . . . . 7
⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈))) |
104 | 99 | recnd 10068 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℂ) |
105 | 104 | negidd 10382 |
. . . . . . 7
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)) = 0) |
106 | 103, 105 | breqtrd 4679 |
. . . . . 6
⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < 0) |
107 | 94 | lt0neg1d 10597 |
. . . . . 6
⊢ (𝜑 → ((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < 0 ↔ 0 < -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)))) |
108 | 106, 107 | mpbid 222 |
. . . . 5
⊢ (𝜑 → 0 < -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) |
109 | 89 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℂ) |
110 | 90 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → (𝑆 − 𝑈) ∈ ℂ) |
111 | 109, 110,
93 | divneg2d 10815 |
. . . . 5
⊢ (𝜑 → -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) = (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈))) |
112 | 108, 111 | breqtrd 4679 |
. . . 4
⊢ (𝜑 → 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈))) |
113 | 90 | renegcld 10457 |
. . . . 5
⊢ (𝜑 → -(𝑆 − 𝑈) ∈ ℝ) |
114 | 44, 11 | posdifd 10614 |
. . . . . . 7
⊢ (𝜑 → (𝑆 < 𝑈 ↔ 0 < (𝑈 − 𝑆))) |
115 | 56, 114 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → 0 < (𝑈 − 𝑆)) |
116 | 91, 92 | negsubdi2d 10408 |
. . . . . 6
⊢ (𝜑 → -(𝑆 − 𝑈) = (𝑈 − 𝑆)) |
117 | 115, 116 | breqtrrd 4681 |
. . . . 5
⊢ (𝜑 → 0 < -(𝑆 − 𝑈)) |
118 | | gt0div 10889 |
. . . . 5
⊢ ((((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ ∧ -(𝑆 − 𝑈) ∈ ℝ ∧ 0 < -(𝑆 − 𝑈)) → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈)))) |
119 | 89, 113, 117, 118 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈)))) |
120 | 112, 119 | mpbird 247 |
. . 3
⊢ (𝜑 → 0 < ((𝐹‘𝑆) − (𝐹‘𝑈))) |
121 | 88, 86 | posdifd 10614 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑈) < (𝐹‘𝑆) ↔ 0 < ((𝐹‘𝑆) − (𝐹‘𝑈)))) |
122 | 120, 121 | mpbird 247 |
. 2
⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑆)) |
123 | | dvferm2.r |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) |
124 | | fveq2 6191 |
. . . . . 6
⊢ (𝑦 = 𝑆 → (𝐹‘𝑦) = (𝐹‘𝑆)) |
125 | 124 | breq1d 4663 |
. . . . 5
⊢ (𝑦 = 𝑆 → ((𝐹‘𝑦) ≤ (𝐹‘𝑈) ↔ (𝐹‘𝑆) ≤ (𝐹‘𝑈))) |
126 | 125 | rspcv 3305 |
. . . 4
⊢ (𝑆 ∈ (𝐴(,)𝑈) → (∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈) → (𝐹‘𝑆) ≤ (𝐹‘𝑈))) |
127 | 59, 123, 126 | sylc 65 |
. . 3
⊢ (𝜑 → (𝐹‘𝑆) ≤ (𝐹‘𝑈)) |
128 | 86, 88 | lenltd 10183 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑆) ≤ (𝐹‘𝑈) ↔ ¬ (𝐹‘𝑈) < (𝐹‘𝑆))) |
129 | 127, 128 | mpbid 222 |
. 2
⊢ (𝜑 → ¬ (𝐹‘𝑈) < (𝐹‘𝑆)) |
130 | 122, 129 | pm2.65i 185 |
1
⊢ ¬
𝜑 |