Proof of Theorem dvferm2lem
| Step | Hyp | Ref
| Expression |
| 1 | | dvferm2.x |
. . . . . . . . . . . 12
⊢ 𝑆 = ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) |
| 2 | | mnfxr 11318 |
. . . . . . . . . . . . . . . 16
⊢ -∞
∈ ℝ* |
| 3 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → -∞ ∈
ℝ*) |
| 4 | | ioossre 13448 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 5 | | dvferm.u |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵)) |
| 6 | 4, 5 | sselid 3981 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑈 ∈ ℝ) |
| 7 | | dvferm2.t |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
| 8 | 7 | rpred 13077 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 9 | 6, 8 | resubcld 11691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 − 𝑇) ∈ ℝ) |
| 10 | 9 | rexrd 11311 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑈 − 𝑇) ∈
ℝ*) |
| 11 | | ne0i 4341 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅) |
| 12 | | ndmioo 13414 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → (𝐴(,)𝐵) = ∅) |
| 13 | 12 | necon1ai 2968 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
| 14 | 5, 11, 13 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
| 15 | 14 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 16 | 10, 15 | ifcld 4572 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈
ℝ*) |
| 17 | 6 | rexrd 11311 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ∈
ℝ*) |
| 18 | 9 | mnfltd 13166 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -∞ < (𝑈 − 𝑇)) |
| 19 | | xrmax2 13218 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ*
∧ (𝑈 − 𝑇) ∈ ℝ*)
→ (𝑈 − 𝑇) ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
| 20 | 15, 10, 19 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑈 − 𝑇) ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
| 21 | 3, 10, 16, 18, 20 | xrltletrd 13203 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → -∞ < if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
| 22 | 6, 7 | ltsubrpd 13109 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑈 − 𝑇) < 𝑈) |
| 23 | | eliooord 13446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵)) |
| 24 | 5, 23 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵)) |
| 25 | 24 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 < 𝑈) |
| 26 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 − 𝑇) = if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) → ((𝑈 − 𝑇) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)) |
| 27 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 = if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) → (𝐴 < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)) |
| 28 | 26, 27 | ifboth 4565 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 − 𝑇) < 𝑈 ∧ 𝐴 < 𝑈) → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈) |
| 29 | 22, 25, 28 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈) |
| 30 | | xrre2 13212 |
. . . . . . . . . . . . . . 15
⊢
(((-∞ ∈ ℝ* ∧ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ* ∧ 𝑈 ∈ ℝ*)
∧ (-∞ < if(𝐴
≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∧ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)) → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ) |
| 31 | 3, 16, 17, 21, 29, 30 | syl32anc 1380 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ) |
| 32 | 31, 6 | readdcld 11290 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) ∈ ℝ) |
| 33 | 32 | rehalfcld 12513 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) ∈ ℝ) |
| 34 | 1, 33 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ℝ) |
| 35 | | avglt2 12505 |
. . . . . . . . . . . . . 14
⊢
((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ ∧ 𝑈 ∈ ℝ) → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈)) |
| 36 | 31, 6, 35 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈)) |
| 37 | 29, 36 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈) |
| 38 | 1, 37 | eqbrtrid 5178 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 < 𝑈) |
| 39 | 34, 38 | ltned 11397 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ≠ 𝑈) |
| 40 | 34, 6, 38 | ltled 11409 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ≤ 𝑈) |
| 41 | 34, 6, 40 | abssuble0d 15471 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) = (𝑈 − 𝑆)) |
| 42 | | avglt1 12504 |
. . . . . . . . . . . . . . . 16
⊢
((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ ∧ 𝑈 ∈ ℝ) → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2))) |
| 43 | 31, 6, 42 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2))) |
| 44 | 29, 43 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2)) |
| 45 | 44, 1 | breqtrrdi 5185 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑆) |
| 46 | 9, 31, 34, 20, 45 | lelttrd 11419 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 − 𝑇) < 𝑆) |
| 47 | 6, 8, 34, 46 | ltsub23d 11868 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈 − 𝑆) < 𝑇) |
| 48 | 41, 47 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) < 𝑇) |
| 49 | | neeq1 3003 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (𝑧 ≠ 𝑈 ↔ 𝑆 ≠ 𝑈)) |
| 50 | | fvoveq1 7454 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑆 → (abs‘(𝑧 − 𝑈)) = (abs‘(𝑆 − 𝑈))) |
| 51 | 50 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → ((abs‘(𝑧 − 𝑈)) < 𝑇 ↔ (abs‘(𝑆 − 𝑈)) < 𝑇)) |
| 52 | 49, 51 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → ((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) ↔ (𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇))) |
| 53 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑆 → (𝐹‘𝑧) = (𝐹‘𝑆)) |
| 54 | 53 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑆 → ((𝐹‘𝑧) − (𝐹‘𝑈)) = ((𝐹‘𝑆) − (𝐹‘𝑈))) |
| 55 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑆 → (𝑧 − 𝑈) = (𝑆 − 𝑈)) |
| 56 | 54, 55 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑆 → (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) = (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) |
| 57 | 56 | fvoveq1d 7453 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) = (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈)))) |
| 58 | 57 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → ((abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈) ↔ (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
| 59 | 52, 58 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → (((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)) ↔ ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))) |
| 60 | | dvferm2.l |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
| 61 | 14 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 62 | 24 | simprd 495 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 < 𝐵) |
| 63 | 17, 61, 62 | xrltled 13192 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ≤ 𝐵) |
| 64 | | iooss2 13423 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ*
∧ 𝑈 ≤ 𝐵) → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵)) |
| 65 | 61, 63, 64 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵)) |
| 66 | | dvferm.s |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋) |
| 67 | 65, 66 | sstrd 3994 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴(,)𝑈) ⊆ 𝑋) |
| 68 | 34 | rexrd 11311 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
| 69 | | xrmax1 13217 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ*
∧ (𝑈 − 𝑇) ∈ ℝ*)
→ 𝐴 ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
| 70 | 15, 10, 69 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴)) |
| 71 | 15, 16, 68, 70, 45 | xrlelttrd 13202 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 < 𝑆) |
| 72 | | elioo2 13428 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ 𝑈 ∈
ℝ*) → (𝑆 ∈ (𝐴(,)𝑈) ↔ (𝑆 ∈ ℝ ∧ 𝐴 < 𝑆 ∧ 𝑆 < 𝑈))) |
| 73 | 15, 17, 72 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆 ∈ (𝐴(,)𝑈) ↔ (𝑆 ∈ ℝ ∧ 𝐴 < 𝑆 ∧ 𝑆 < 𝑈))) |
| 74 | 34, 71, 38, 73 | mpbir3and 1343 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ (𝐴(,)𝑈)) |
| 75 | 67, 74 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ 𝑋) |
| 76 | | eldifsn 4786 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (𝑋 ∖ {𝑈}) ↔ (𝑆 ∈ 𝑋 ∧ 𝑆 ≠ 𝑈)) |
| 77 | 75, 39, 76 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ (𝑋 ∖ {𝑈})) |
| 78 | 59, 60, 77 | rspcdva 3623 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))) |
| 79 | 39, 48, 78 | mp2and 699 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)) |
| 80 | | dvferm.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
| 81 | 80, 75 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ) |
| 82 | 66, 5 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ 𝑋) |
| 83 | 80, 82 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑈) ∈ ℝ) |
| 84 | 81, 83 | resubcld 11691 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ) |
| 85 | 34, 6 | resubcld 11691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 − 𝑈) ∈ ℝ) |
| 86 | 34 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ ℂ) |
| 87 | 6 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ ℂ) |
| 88 | 86, 87, 39 | subne0d 11629 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 − 𝑈) ≠ 0) |
| 89 | 84, 85, 88 | redivcld 12095 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∈ ℝ) |
| 90 | | dvferm.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
| 91 | | dvfre 25989 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
| 92 | 80, 90, 91 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
| 93 | | dvferm.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹)) |
| 94 | 92, 93 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ) |
| 95 | 94 | renegcld 11690 |
. . . . . . . . . 10
⊢ (𝜑 → -((ℝ D 𝐹)‘𝑈) ∈ ℝ) |
| 96 | 89, 94, 95 | absdifltd 15472 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈) ↔ ((((ℝ D 𝐹)‘𝑈) − -((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈))))) |
| 97 | 79, 96 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → ((((ℝ D 𝐹)‘𝑈) − -((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)))) |
| 98 | 97 | simprd 495 |
. . . . . . 7
⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈))) |
| 99 | 94 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℂ) |
| 100 | 99 | negidd 11610 |
. . . . . . 7
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)) = 0) |
| 101 | 98, 100 | breqtrd 5169 |
. . . . . 6
⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < 0) |
| 102 | 89 | lt0neg1d 11832 |
. . . . . 6
⊢ (𝜑 → ((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < 0 ↔ 0 < -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)))) |
| 103 | 101, 102 | mpbid 232 |
. . . . 5
⊢ (𝜑 → 0 < -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) |
| 104 | 84 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℂ) |
| 105 | 85 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → (𝑆 − 𝑈) ∈ ℂ) |
| 106 | 104, 105,
88 | divneg2d 12057 |
. . . . 5
⊢ (𝜑 → -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) = (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈))) |
| 107 | 103, 106 | breqtrd 5169 |
. . . 4
⊢ (𝜑 → 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈))) |
| 108 | 85 | renegcld 11690 |
. . . . 5
⊢ (𝜑 → -(𝑆 − 𝑈) ∈ ℝ) |
| 109 | 34, 6 | posdifd 11850 |
. . . . . . 7
⊢ (𝜑 → (𝑆 < 𝑈 ↔ 0 < (𝑈 − 𝑆))) |
| 110 | 38, 109 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → 0 < (𝑈 − 𝑆)) |
| 111 | 86, 87 | negsubdi2d 11636 |
. . . . . 6
⊢ (𝜑 → -(𝑆 − 𝑈) = (𝑈 − 𝑆)) |
| 112 | 110, 111 | breqtrrd 5171 |
. . . . 5
⊢ (𝜑 → 0 < -(𝑆 − 𝑈)) |
| 113 | | gt0div 12134 |
. . . . 5
⊢ ((((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ ∧ -(𝑆 − 𝑈) ∈ ℝ ∧ 0 < -(𝑆 − 𝑈)) → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈)))) |
| 114 | 84, 108, 112, 113 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈)))) |
| 115 | 107, 114 | mpbird 257 |
. . 3
⊢ (𝜑 → 0 < ((𝐹‘𝑆) − (𝐹‘𝑈))) |
| 116 | 83, 81 | posdifd 11850 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑈) < (𝐹‘𝑆) ↔ 0 < ((𝐹‘𝑆) − (𝐹‘𝑈)))) |
| 117 | 115, 116 | mpbird 257 |
. 2
⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑆)) |
| 118 | | fveq2 6906 |
. . . . 5
⊢ (𝑦 = 𝑆 → (𝐹‘𝑦) = (𝐹‘𝑆)) |
| 119 | 118 | breq1d 5153 |
. . . 4
⊢ (𝑦 = 𝑆 → ((𝐹‘𝑦) ≤ (𝐹‘𝑈) ↔ (𝐹‘𝑆) ≤ (𝐹‘𝑈))) |
| 120 | | dvferm2.r |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) |
| 121 | 119, 120,
74 | rspcdva 3623 |
. . 3
⊢ (𝜑 → (𝐹‘𝑆) ≤ (𝐹‘𝑈)) |
| 122 | 81, 83, 121 | lensymd 11412 |
. 2
⊢ (𝜑 → ¬ (𝐹‘𝑈) < (𝐹‘𝑆)) |
| 123 | 117, 122 | pm2.65i 194 |
1
⊢ ¬
𝜑 |