Proof of Theorem dvferm2lem
Step | Hyp | Ref
| Expression |
1 | | dvferm2.x |
. . . . . . . . . . . . 13
⊢ 𝑆 = ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) |
2 | | mnfxr 10421 |
. . . . . . . . . . . . . . . . 17
⊢ -∞
∈ ℝ* |
3 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -∞ ∈
ℝ*) |
4 | | ioossre 12530 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴(,)𝐵) ⊆ ℝ |
5 | | dvferm.u |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵)) |
6 | 4, 5 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑈 ∈ ℝ) |
7 | | dvferm2.t |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
8 | 7 | rpred 12163 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑇 ∈ ℝ) |
9 | 6, 8 | resubcld 10789 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑈 − 𝑇) ∈ ℝ) |
10 | 9 | rexrd 10413 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 − 𝑇) ∈
ℝ*) |
11 | | ne0i 4152 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅) |
12 | | ndmioo 12497 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
(𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → (𝐴(,)𝐵) = ∅) |
13 | 12 | necon1ai 3026 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
14 | 5, 11, 13 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
15 | 14 | simpld 490 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
16 | 10, 15 | ifcld 4353 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈
ℝ*) |
17 | 6 | rexrd 10413 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 ∈
ℝ*) |
18 | | mnflt 12250 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 − 𝑇) ∈ ℝ → -∞ < (𝑈 − 𝑇)) |
19 | 9, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → -∞ < (𝑈 − 𝑇)) |
20 | | xrmax2 12302 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℝ*
∧ (𝑈 − 𝑇) ∈ ℝ*)
→ (𝑈 − 𝑇) ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
21 | 15, 10, 20 | syl2anc 579 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 − 𝑇) ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
22 | 3, 10, 16, 19, 21 | xrltletrd 12287 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -∞ < if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
23 | 6, 7 | ltsubrpd 12195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 − 𝑇) < 𝑈) |
24 | | eliooord 12528 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵)) |
25 | 5, 24 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵)) |
26 | 25 | simpld 490 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 < 𝑈) |
27 | | breq1 4878 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 − 𝑇) = if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) → ((𝑈 − 𝑇) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)) |
28 | | breq1 4878 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) → (𝐴 < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)) |
29 | 27, 28 | ifboth 4346 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑈 − 𝑇) < 𝑈 ∧ 𝐴 < 𝑈) → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈) |
30 | 23, 26, 29 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈) |
31 | | xrre2 12296 |
. . . . . . . . . . . . . . . 16
⊢
(((-∞ ∈ ℝ* ∧ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ* ∧ 𝑈 ∈ ℝ*)
∧ (-∞ < if(𝐴
≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∧ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)) → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ) |
32 | 3, 16, 17, 22, 30, 31 | syl32anc 1501 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ) |
33 | 32, 6 | readdcld 10393 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) ∈ ℝ) |
34 | 33 | rehalfcld 11612 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) ∈ ℝ) |
35 | 1, 34 | syl5eqel 2910 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ ℝ) |
36 | | avglt2 11604 |
. . . . . . . . . . . . . . 15
⊢
((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ ∧ 𝑈 ∈ ℝ) → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈)) |
37 | 32, 6, 36 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈)) |
38 | 30, 37 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈) |
39 | 1, 38 | syl5eqbr 4910 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 < 𝑈) |
40 | 35, 39 | ltned 10499 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ≠ 𝑈) |
41 | 35, 6, 39 | ltled 10511 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ≤ 𝑈) |
42 | 35, 6, 41 | abssuble0d 14555 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) = (𝑈 − 𝑆)) |
43 | | avglt1 11603 |
. . . . . . . . . . . . . . . . 17
⊢
((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ ∧ 𝑈 ∈ ℝ) → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2))) |
44 | 32, 6, 43 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2))) |
45 | 30, 44 | mpbid 224 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2)) |
46 | 45, 1 | syl6breqr 4917 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑆) |
47 | 9, 32, 35, 21, 46 | lelttrd 10521 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 − 𝑇) < 𝑆) |
48 | 6, 8, 35, 47 | ltsub23d 10964 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 − 𝑆) < 𝑇) |
49 | 42, 48 | eqbrtrd 4897 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) < 𝑇) |
50 | 40, 49 | jca 507 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇)) |
51 | | neeq1 3061 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (𝑧 ≠ 𝑈 ↔ 𝑆 ≠ 𝑈)) |
52 | | fvoveq1 6933 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑆 → (abs‘(𝑧 − 𝑈)) = (abs‘(𝑆 − 𝑈))) |
53 | 52 | breq1d 4885 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → ((abs‘(𝑧 − 𝑈)) < 𝑇 ↔ (abs‘(𝑆 − 𝑈)) < 𝑇)) |
54 | 51, 53 | anbi12d 624 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → ((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) ↔ (𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇))) |
55 | | fveq2 6437 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑆 → (𝐹‘𝑧) = (𝐹‘𝑆)) |
56 | 55 | oveq1d 6925 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑆 → ((𝐹‘𝑧) − (𝐹‘𝑈)) = ((𝐹‘𝑆) − (𝐹‘𝑈))) |
57 | | oveq1 6917 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑆 → (𝑧 − 𝑈) = (𝑆 − 𝑈)) |
58 | 56, 57 | oveq12d 6928 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑆 → (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) = (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) |
59 | 58 | fvoveq1d 6932 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) = (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈)))) |
60 | 59 | breq1d 4885 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → ((abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈) ↔ (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
61 | 54, 60 | imbi12d 336 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → (((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)) ↔ ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))) |
62 | | dvferm2.l |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
63 | 14 | simprd 491 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
64 | 25 | simprd 491 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 < 𝐵) |
65 | 17, 63, 64 | xrltled 12276 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ≤ 𝐵) |
66 | | iooss2 12506 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ*
∧ 𝑈 ≤ 𝐵) → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵)) |
67 | 63, 65, 66 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵)) |
68 | | dvferm.s |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋) |
69 | 67, 68 | sstrd 3837 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴(,)𝑈) ⊆ 𝑋) |
70 | 35 | rexrd 10413 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
71 | | xrmax1 12301 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ*
∧ (𝑈 − 𝑇) ∈ ℝ*)
→ 𝐴 ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
72 | 15, 10, 71 | syl2anc 579 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
73 | 15, 16, 70, 72, 46 | xrlelttrd 12286 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 < 𝑆) |
74 | | elioo2 12511 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ 𝑈 ∈
ℝ*) → (𝑆 ∈ (𝐴(,)𝑈) ↔ (𝑆 ∈ ℝ ∧ 𝐴 < 𝑆 ∧ 𝑆 < 𝑈))) |
75 | 15, 17, 74 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆 ∈ (𝐴(,)𝑈) ↔ (𝑆 ∈ ℝ ∧ 𝐴 < 𝑆 ∧ 𝑆 < 𝑈))) |
76 | 35, 73, 39, 75 | mpbir3and 1446 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ (𝐴(,)𝑈)) |
77 | 69, 76 | sseldd 3828 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ 𝑋) |
78 | | eldifsn 4538 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (𝑋 ∖ {𝑈}) ↔ (𝑆 ∈ 𝑋 ∧ 𝑆 ≠ 𝑈)) |
79 | 77, 40, 78 | sylanbrc 578 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ (𝑋 ∖ {𝑈})) |
80 | 61, 62, 79 | rspcdva 3532 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
81 | 50, 80 | mpd 15 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)) |
82 | | dvferm.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
83 | 82, 77 | ffvelrnd 6614 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ) |
84 | 68, 5 | sseldd 3828 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ 𝑋) |
85 | 82, 84 | ffvelrnd 6614 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑈) ∈ ℝ) |
86 | 83, 85 | resubcld 10789 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ) |
87 | 35, 6 | resubcld 10789 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 − 𝑈) ∈ ℝ) |
88 | 35 | recnd 10392 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ ℂ) |
89 | 6 | recnd 10392 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ ℂ) |
90 | 88, 89, 40 | subne0d 10729 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 − 𝑈) ≠ 0) |
91 | 86, 87, 90 | redivcld 11186 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∈ ℝ) |
92 | | dvferm.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
93 | | dvfre 24120 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
94 | 82, 92, 93 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
95 | | dvferm.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹)) |
96 | 94, 95 | ffvelrnd 6614 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ) |
97 | 96 | renegcld 10788 |
. . . . . . . . . 10
⊢ (𝜑 → -((ℝ D 𝐹)‘𝑈) ∈ ℝ) |
98 | 91, 96, 97 | absdifltd 14556 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈) ↔ ((((ℝ D 𝐹)‘𝑈) − -((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈))))) |
99 | 81, 98 | mpbid 224 |
. . . . . . . 8
⊢ (𝜑 → ((((ℝ D 𝐹)‘𝑈) − -((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)))) |
100 | 99 | simprd 491 |
. . . . . . 7
⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈))) |
101 | 96 | recnd 10392 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℂ) |
102 | 101 | negidd 10710 |
. . . . . . 7
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)) = 0) |
103 | 100, 102 | breqtrd 4901 |
. . . . . 6
⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < 0) |
104 | 91 | lt0neg1d 10928 |
. . . . . 6
⊢ (𝜑 → ((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < 0 ↔ 0 < -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)))) |
105 | 103, 104 | mpbid 224 |
. . . . 5
⊢ (𝜑 → 0 < -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) |
106 | 86 | recnd 10392 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℂ) |
107 | 87 | recnd 10392 |
. . . . . 6
⊢ (𝜑 → (𝑆 − 𝑈) ∈ ℂ) |
108 | 106, 107,
90 | divneg2d 11148 |
. . . . 5
⊢ (𝜑 → -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) = (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈))) |
109 | 105, 108 | breqtrd 4901 |
. . . 4
⊢ (𝜑 → 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈))) |
110 | 87 | renegcld 10788 |
. . . . 5
⊢ (𝜑 → -(𝑆 − 𝑈) ∈ ℝ) |
111 | 35, 6 | posdifd 10946 |
. . . . . . 7
⊢ (𝜑 → (𝑆 < 𝑈 ↔ 0 < (𝑈 − 𝑆))) |
112 | 39, 111 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → 0 < (𝑈 − 𝑆)) |
113 | 88, 89 | negsubdi2d 10736 |
. . . . . 6
⊢ (𝜑 → -(𝑆 − 𝑈) = (𝑈 − 𝑆)) |
114 | 112, 113 | breqtrrd 4903 |
. . . . 5
⊢ (𝜑 → 0 < -(𝑆 − 𝑈)) |
115 | | gt0div 11226 |
. . . . 5
⊢ ((((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ ∧ -(𝑆 − 𝑈) ∈ ℝ ∧ 0 < -(𝑆 − 𝑈)) → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈)))) |
116 | 86, 110, 114, 115 | syl3anc 1494 |
. . . 4
⊢ (𝜑 → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈)))) |
117 | 109, 116 | mpbird 249 |
. . 3
⊢ (𝜑 → 0 < ((𝐹‘𝑆) − (𝐹‘𝑈))) |
118 | 85, 83 | posdifd 10946 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑈) < (𝐹‘𝑆) ↔ 0 < ((𝐹‘𝑆) − (𝐹‘𝑈)))) |
119 | 117, 118 | mpbird 249 |
. 2
⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑆)) |
120 | | fveq2 6437 |
. . . . 5
⊢ (𝑦 = 𝑆 → (𝐹‘𝑦) = (𝐹‘𝑆)) |
121 | 120 | breq1d 4885 |
. . . 4
⊢ (𝑦 = 𝑆 → ((𝐹‘𝑦) ≤ (𝐹‘𝑈) ↔ (𝐹‘𝑆) ≤ (𝐹‘𝑈))) |
122 | | dvferm2.r |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) |
123 | 121, 122,
76 | rspcdva 3532 |
. . 3
⊢ (𝜑 → (𝐹‘𝑆) ≤ (𝐹‘𝑈)) |
124 | 83, 85 | lenltd 10509 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑆) ≤ (𝐹‘𝑈) ↔ ¬ (𝐹‘𝑈) < (𝐹‘𝑆))) |
125 | 123, 124 | mpbid 224 |
. 2
⊢ (𝜑 → ¬ (𝐹‘𝑈) < (𝐹‘𝑆)) |
126 | 119, 125 | pm2.65i 186 |
1
⊢ ¬
𝜑 |