Proof of Theorem dvferm1lem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dvferm.a | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) | 
| 2 |  | dvferm.b | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℝ) | 
| 3 |  | dvfre 25990 | . . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) | 
| 4 | 1, 2, 3 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) | 
| 5 |  | dvferm.d | . . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹)) | 
| 6 | 4, 5 | ffvelcdmd 7104 | . . . . . . 7
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ) | 
| 7 | 6 | recnd 11290 | . . . . . 6
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℂ) | 
| 8 | 7 | subidd 11609 | . . . . 5
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) = 0) | 
| 9 |  | ioossre 13449 | . . . . . . . . . 10
⊢ (𝐴(,)𝐵) ⊆ ℝ | 
| 10 |  | dvferm.u | . . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵)) | 
| 11 | 9, 10 | sselid 3980 | . . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ ℝ) | 
| 12 |  | eliooord 13447 | . . . . . . . . . . . . . 14
⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵)) | 
| 13 | 10, 12 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵)) | 
| 14 | 13 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 < 𝐵) | 
| 15 |  | dvferm1.t | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈
ℝ+) | 
| 16 | 11, 15 | ltaddrpd 13111 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 < (𝑈 + 𝑇)) | 
| 17 |  | breq2 5146 | . . . . . . . . . . . . 13
⊢ (𝐵 = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (𝑈 < 𝐵 ↔ 𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) | 
| 18 |  | breq2 5146 | . . . . . . . . . . . . 13
⊢ ((𝑈 + 𝑇) = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (𝑈 < (𝑈 + 𝑇) ↔ 𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) | 
| 19 | 17, 18 | ifboth 4564 | . . . . . . . . . . . 12
⊢ ((𝑈 < 𝐵 ∧ 𝑈 < (𝑈 + 𝑇)) → 𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) | 
| 20 | 14, 16, 19 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) | 
| 21 |  | ne0i 4340 | . . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅) | 
| 22 |  | ndmioo 13415 | . . . . . . . . . . . . . . . . 17
⊢ (¬
(𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → (𝐴(,)𝐵) = ∅) | 
| 23 | 22 | necon1ai 2967 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) | 
| 24 | 10, 21, 23 | 3syl 18 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) | 
| 25 | 24 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 26 | 15 | rpred 13078 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑇 ∈ ℝ) | 
| 27 | 11, 26 | readdcld 11291 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 + 𝑇) ∈ ℝ) | 
| 28 | 27 | rexrd 11312 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 + 𝑇) ∈
ℝ*) | 
| 29 | 25, 28 | ifcld 4571 | . . . . . . . . . . . . 13
⊢ (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈
ℝ*) | 
| 30 |  | mnfxr 11319 | . . . . . . . . . . . . . . . 16
⊢ -∞
∈ ℝ* | 
| 31 | 30 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → -∞ ∈
ℝ*) | 
| 32 | 11 | rexrd 11312 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ∈
ℝ*) | 
| 33 | 11 | mnfltd 13167 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → -∞ < 𝑈) | 
| 34 | 31, 32, 25, 33, 14 | xrlttrd 13202 | . . . . . . . . . . . . . 14
⊢ (𝜑 → -∞ < 𝐵) | 
| 35 | 27 | mnfltd 13167 | . . . . . . . . . . . . . 14
⊢ (𝜑 → -∞ < (𝑈 + 𝑇)) | 
| 36 |  | breq2 5146 | . . . . . . . . . . . . . . 15
⊢ (𝐵 = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (-∞ < 𝐵 ↔ -∞ < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) | 
| 37 |  | breq2 5146 | . . . . . . . . . . . . . . 15
⊢ ((𝑈 + 𝑇) = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (-∞ < (𝑈 + 𝑇) ↔ -∞ < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) | 
| 38 | 36, 37 | ifboth 4564 | . . . . . . . . . . . . . 14
⊢
((-∞ < 𝐵
∧ -∞ < (𝑈 +
𝑇)) → -∞ <
if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) | 
| 39 | 34, 35, 38 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → -∞ < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) | 
| 40 |  | xrmin2 13221 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ*
∧ (𝑈 + 𝑇) ∈ ℝ*)
→ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ (𝑈 + 𝑇)) | 
| 41 | 25, 28, 40 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ (𝑈 + 𝑇)) | 
| 42 |  | xrre 13212 | . . . . . . . . . . . . 13
⊢
(((if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ* ∧ (𝑈 + 𝑇) ∈ ℝ) ∧ (-∞ <
if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∧ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ (𝑈 + 𝑇))) → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ) | 
| 43 | 29, 27, 39, 41, 42 | syl22anc 838 | . . . . . . . . . . . 12
⊢ (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ) | 
| 44 |  | avglt1 12506 | . . . . . . . . . . . 12
⊢ ((𝑈 ∈ ℝ ∧ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ) → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ 𝑈 < ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2))) | 
| 45 | 11, 43, 44 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ 𝑈 < ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2))) | 
| 46 | 20, 45 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → 𝑈 < ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2)) | 
| 47 |  | dvferm1.x | . . . . . . . . . 10
⊢ 𝑆 = ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) | 
| 48 | 46, 47 | breqtrrdi 5184 | . . . . . . . . 9
⊢ (𝜑 → 𝑈 < 𝑆) | 
| 49 | 11, 48 | gtned 11397 | . . . . . . . 8
⊢ (𝜑 → 𝑆 ≠ 𝑈) | 
| 50 | 11, 43 | readdcld 11291 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) ∈ ℝ) | 
| 51 | 50 | rehalfcld 12515 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) ∈ ℝ) | 
| 52 | 47, 51 | eqeltrid 2844 | . . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℝ) | 
| 53 | 11, 52, 48 | ltled 11410 | . . . . . . . . . 10
⊢ (𝜑 → 𝑈 ≤ 𝑆) | 
| 54 | 11, 52, 53 | abssubge0d 15471 | . . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) = (𝑆 − 𝑈)) | 
| 55 |  | avglt2 12507 | . . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ ℝ ∧ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ) → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) | 
| 56 | 11, 43, 55 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) | 
| 57 | 20, 56 | mpbid 232 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) | 
| 58 | 47, 57 | eqbrtrid 5177 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) | 
| 59 | 52, 43, 27, 58, 41 | ltletrd 11422 | . . . . . . . . . 10
⊢ (𝜑 → 𝑆 < (𝑈 + 𝑇)) | 
| 60 | 52, 11, 26 | ltsubadd2d 11862 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑆 − 𝑈) < 𝑇 ↔ 𝑆 < (𝑈 + 𝑇))) | 
| 61 | 59, 60 | mpbird 257 | . . . . . . . . 9
⊢ (𝜑 → (𝑆 − 𝑈) < 𝑇) | 
| 62 | 54, 61 | eqbrtrd 5164 | . . . . . . . 8
⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) < 𝑇) | 
| 63 |  | neeq1 3002 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → (𝑧 ≠ 𝑈 ↔ 𝑆 ≠ 𝑈)) | 
| 64 |  | fvoveq1 7455 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → (abs‘(𝑧 − 𝑈)) = (abs‘(𝑆 − 𝑈))) | 
| 65 | 64 | breq1d 5152 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → ((abs‘(𝑧 − 𝑈)) < 𝑇 ↔ (abs‘(𝑆 − 𝑈)) < 𝑇)) | 
| 66 | 63, 65 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑧 = 𝑆 → ((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) ↔ (𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇))) | 
| 67 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑆 → (𝐹‘𝑧) = (𝐹‘𝑆)) | 
| 68 | 67 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → ((𝐹‘𝑧) − (𝐹‘𝑈)) = ((𝐹‘𝑆) − (𝐹‘𝑈))) | 
| 69 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (𝑧 − 𝑈) = (𝑆 − 𝑈)) | 
| 70 | 68, 69 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) = (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) | 
| 71 | 70 | fvoveq1d 7454 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) = (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈)))) | 
| 72 | 71 | breq1d 5152 | . . . . . . . . . 10
⊢ (𝑧 = 𝑆 → ((abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈) ↔ (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) | 
| 73 | 66, 72 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑧 = 𝑆 → (((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)) ↔ ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))) | 
| 74 |  | dvferm1.l | . . . . . . . . 9
⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) | 
| 75 | 24 | simpld 494 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 76 | 13 | simpld 494 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 < 𝑈) | 
| 77 | 75, 32, 76 | xrltled 13193 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ≤ 𝑈) | 
| 78 |  | iooss1 13423 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑈) → (𝑈(,)𝐵) ⊆ (𝐴(,)𝐵)) | 
| 79 | 75, 77, 78 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑈(,)𝐵) ⊆ (𝐴(,)𝐵)) | 
| 80 |  | dvferm.s | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋) | 
| 81 | 79, 80 | sstrd 3993 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑈(,)𝐵) ⊆ 𝑋) | 
| 82 | 52 | rexrd 11312 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈
ℝ*) | 
| 83 |  | xrmin1 13220 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ*
∧ (𝑈 + 𝑇) ∈ ℝ*)
→ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ 𝐵) | 
| 84 | 25, 28, 83 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ 𝐵) | 
| 85 | 82, 29, 25, 58, 84 | xrltletrd 13204 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 < 𝐵) | 
| 86 |  | elioo2 13429 | . . . . . . . . . . . . 13
⊢ ((𝑈 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑆 ∈ (𝑈(,)𝐵) ↔ (𝑆 ∈ ℝ ∧ 𝑈 < 𝑆 ∧ 𝑆 < 𝐵))) | 
| 87 | 32, 25, 86 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ∈ (𝑈(,)𝐵) ↔ (𝑆 ∈ ℝ ∧ 𝑈 < 𝑆 ∧ 𝑆 < 𝐵))) | 
| 88 | 52, 48, 85, 87 | mpbir3and 1342 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ (𝑈(,)𝐵)) | 
| 89 | 81, 88 | sseldd 3983 | . . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ 𝑋) | 
| 90 |  | eldifsn 4785 | . . . . . . . . . 10
⊢ (𝑆 ∈ (𝑋 ∖ {𝑈}) ↔ (𝑆 ∈ 𝑋 ∧ 𝑆 ≠ 𝑈)) | 
| 91 | 89, 49, 90 | sylanbrc 583 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ (𝑋 ∖ {𝑈})) | 
| 92 | 73, 74, 91 | rspcdva 3622 | . . . . . . . 8
⊢ (𝜑 → ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) | 
| 93 | 49, 62, 92 | mp2and 699 | . . . . . . 7
⊢ (𝜑 → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)) | 
| 94 | 1, 89 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ) | 
| 95 | 80, 10 | sseldd 3983 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ 𝑋) | 
| 96 | 1, 95 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑈) ∈ ℝ) | 
| 97 | 94, 96 | resubcld 11692 | . . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ) | 
| 98 | 52, 11 | resubcld 11692 | . . . . . . . . . 10
⊢ (𝜑 → (𝑆 − 𝑈) ∈ ℝ) | 
| 99 | 11, 52 | posdifd 11851 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑈 < 𝑆 ↔ 0 < (𝑆 − 𝑈))) | 
| 100 | 48, 99 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → 0 < (𝑆 − 𝑈)) | 
| 101 | 98, 100 | elrpd 13075 | . . . . . . . . 9
⊢ (𝜑 → (𝑆 − 𝑈) ∈
ℝ+) | 
| 102 | 97, 101 | rerpdivcld 13109 | . . . . . . . 8
⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∈ ℝ) | 
| 103 | 102, 6, 6 | absdifltd 15473 | . . . . . . 7
⊢ (𝜑 → ((abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈) ↔ ((((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + ((ℝ D 𝐹)‘𝑈))))) | 
| 104 | 93, 103 | mpbid 232 | . . . . . 6
⊢ (𝜑 → ((((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + ((ℝ D 𝐹)‘𝑈)))) | 
| 105 | 104 | simpld 494 | . . . . 5
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) | 
| 106 | 8, 105 | eqbrtrrd 5166 | . . . 4
⊢ (𝜑 → 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) | 
| 107 |  | gt0div 12135 | . . . . 5
⊢ ((((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ ∧ (𝑆 − 𝑈) ∈ ℝ ∧ 0 < (𝑆 − 𝑈)) → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)))) | 
| 108 | 97, 98, 100, 107 | syl3anc 1372 | . . . 4
⊢ (𝜑 → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)))) | 
| 109 | 106, 108 | mpbird 257 | . . 3
⊢ (𝜑 → 0 < ((𝐹‘𝑆) − (𝐹‘𝑈))) | 
| 110 | 96, 94 | posdifd 11851 | . . 3
⊢ (𝜑 → ((𝐹‘𝑈) < (𝐹‘𝑆) ↔ 0 < ((𝐹‘𝑆) − (𝐹‘𝑈)))) | 
| 111 | 109, 110 | mpbird 257 | . 2
⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑆)) | 
| 112 |  | fveq2 6905 | . . . . 5
⊢ (𝑦 = 𝑆 → (𝐹‘𝑦) = (𝐹‘𝑆)) | 
| 113 | 112 | breq1d 5152 | . . . 4
⊢ (𝑦 = 𝑆 → ((𝐹‘𝑦) ≤ (𝐹‘𝑈) ↔ (𝐹‘𝑆) ≤ (𝐹‘𝑈))) | 
| 114 |  | dvferm1.r | . . . 4
⊢ (𝜑 → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) | 
| 115 | 113, 114,
88 | rspcdva 3622 | . . 3
⊢ (𝜑 → (𝐹‘𝑆) ≤ (𝐹‘𝑈)) | 
| 116 | 94, 96, 115 | lensymd 11413 | . 2
⊢ (𝜑 → ¬ (𝐹‘𝑈) < (𝐹‘𝑆)) | 
| 117 | 111, 116 | pm2.65i 194 | 1
⊢  ¬
𝜑 |