Proof of Theorem dvferm1lem
Step | Hyp | Ref
| Expression |
1 | | dvferm.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
2 | | dvferm.b |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
3 | | dvfre 23714 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
4 | 1, 2, 3 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
5 | | dvferm.d |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹)) |
6 | 4, 5 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ) |
7 | 6 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℂ) |
8 | 7 | subidd 10380 |
. . . . 5
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) = 0) |
9 | | dvferm.u |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵)) |
10 | | ne0i 3921 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅) |
11 | | ndmioo 12202 |
. . . . . . . . . . . . . . 15
⊢ (¬
(𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → (𝐴(,)𝐵) = ∅) |
12 | 11 | necon1ai 2821 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
13 | 9, 10, 12 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
14 | 13 | simpld 475 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
15 | | eliooord 12233 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵)) |
16 | 9, 15 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵)) |
17 | 16 | simpld 475 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 < 𝑈) |
18 | | ioossre 12235 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴(,)𝐵) ⊆ ℝ |
19 | 18, 9 | sseldi 3601 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ∈ ℝ) |
20 | 19 | rexrd 10089 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ∈
ℝ*) |
21 | | xrltle 11982 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝑈 ∈
ℝ*) → (𝐴 < 𝑈 → 𝐴 ≤ 𝑈)) |
22 | 14, 20, 21 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 < 𝑈 → 𝐴 ≤ 𝑈)) |
23 | 17, 22 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ 𝑈) |
24 | | iooss1 12210 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑈) → (𝑈(,)𝐵) ⊆ (𝐴(,)𝐵)) |
25 | 14, 23, 24 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈(,)𝐵) ⊆ (𝐴(,)𝐵)) |
26 | | dvferm.s |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋) |
27 | 25, 26 | sstrd 3613 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑈(,)𝐵) ⊆ 𝑋) |
28 | | dvferm1.x |
. . . . . . . . . . . 12
⊢ 𝑆 = ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) |
29 | 13 | simprd 479 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
30 | | dvferm1.t |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
31 | 30 | rpred 11872 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ∈ ℝ) |
32 | 19, 31 | readdcld 10069 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 + 𝑇) ∈ ℝ) |
33 | 32 | rexrd 10089 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑈 + 𝑇) ∈
ℝ*) |
34 | 29, 33 | ifcld 4131 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈
ℝ*) |
35 | | mnfxr 10096 |
. . . . . . . . . . . . . . . . . 18
⊢ -∞
∈ ℝ* |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → -∞ ∈
ℝ*) |
37 | | mnflt 11957 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ ℝ → -∞
< 𝑈) |
38 | 19, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → -∞ < 𝑈) |
39 | 16 | simprd 479 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈 < 𝐵) |
40 | 36, 20, 29, 38, 39 | xrlttrd 11990 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -∞ < 𝐵) |
41 | | mnflt 11957 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 + 𝑇) ∈ ℝ → -∞ < (𝑈 + 𝑇)) |
42 | 32, 41 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -∞ < (𝑈 + 𝑇)) |
43 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (-∞ < 𝐵 ↔ -∞ < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) |
44 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 + 𝑇) = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (-∞ < (𝑈 + 𝑇) ↔ -∞ < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) |
45 | 43, 44 | ifboth 4124 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ < 𝐵
∧ -∞ < (𝑈 +
𝑇)) → -∞ <
if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) |
46 | 40, 42, 45 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → -∞ < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) |
47 | | xrmin2 12009 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ ℝ*
∧ (𝑈 + 𝑇) ∈ ℝ*)
→ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ (𝑈 + 𝑇)) |
48 | 29, 33, 47 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ (𝑈 + 𝑇)) |
49 | | xrre 12000 |
. . . . . . . . . . . . . . 15
⊢
(((if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ* ∧ (𝑈 + 𝑇) ∈ ℝ) ∧ (-∞ <
if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∧ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ (𝑈 + 𝑇))) → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ) |
50 | 34, 32, 46, 48, 49 | syl22anc 1327 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ) |
51 | 19, 50 | readdcld 10069 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) ∈ ℝ) |
52 | 51 | rehalfcld 11279 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) ∈ ℝ) |
53 | 28, 52 | syl5eqel 2705 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ℝ) |
54 | 19, 30 | ltaddrpd 11905 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 < (𝑈 + 𝑇)) |
55 | | breq2 4657 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (𝑈 < 𝐵 ↔ 𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) |
56 | | breq2 4657 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 + 𝑇) = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (𝑈 < (𝑈 + 𝑇) ↔ 𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) |
57 | 55, 56 | ifboth 4124 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 < 𝐵 ∧ 𝑈 < (𝑈 + 𝑇)) → 𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) |
58 | 39, 54, 57 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) |
59 | | avglt1 11270 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ ℝ ∧ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ) → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ 𝑈 < ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2))) |
60 | 19, 50, 59 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ 𝑈 < ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2))) |
61 | 58, 60 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 < ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2)) |
62 | 61, 28 | syl6breqr 4695 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 < 𝑆) |
63 | 53 | rexrd 10089 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
64 | | avglt2 11271 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ ℝ ∧ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ) → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) |
65 | 19, 50, 64 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))) |
66 | 58, 65 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) |
67 | 28, 66 | syl5eqbr 4688 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) |
68 | | xrmin1 12008 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ*
∧ (𝑈 + 𝑇) ∈ ℝ*)
→ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ 𝐵) |
69 | 29, 33, 68 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ 𝐵) |
70 | 63, 34, 29, 67, 69 | xrltletrd 11992 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 < 𝐵) |
71 | | elioo2 12216 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑆 ∈ (𝑈(,)𝐵) ↔ (𝑆 ∈ ℝ ∧ 𝑈 < 𝑆 ∧ 𝑆 < 𝐵))) |
72 | 20, 29, 71 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 ∈ (𝑈(,)𝐵) ↔ (𝑆 ∈ ℝ ∧ 𝑈 < 𝑆 ∧ 𝑆 < 𝐵))) |
73 | 53, 62, 70, 72 | mpbir3and 1245 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ (𝑈(,)𝐵)) |
74 | 27, 73 | sseldd 3604 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ 𝑋) |
75 | 19, 62 | gtned 10172 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ≠ 𝑈) |
76 | | eldifsn 4317 |
. . . . . . . . 9
⊢ (𝑆 ∈ (𝑋 ∖ {𝑈}) ↔ (𝑆 ∈ 𝑋 ∧ 𝑆 ≠ 𝑈)) |
77 | 74, 75, 76 | sylanbrc 698 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ (𝑋 ∖ {𝑈})) |
78 | | dvferm1.l |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) |
79 | 19, 53, 62 | ltled 10185 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ≤ 𝑆) |
80 | 19, 53, 79 | abssubge0d 14170 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) = (𝑆 − 𝑈)) |
81 | 53, 50, 32, 67, 48 | ltletrd 10197 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 < (𝑈 + 𝑇)) |
82 | 53, 19, 31 | ltsubadd2d 10625 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑆 − 𝑈) < 𝑇 ↔ 𝑆 < (𝑈 + 𝑇))) |
83 | 81, 82 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 − 𝑈) < 𝑇) |
84 | 80, 83 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) < 𝑇) |
85 | 75, 84 | jca 554 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇)) |
86 | | neeq1 2856 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → (𝑧 ≠ 𝑈 ↔ 𝑆 ≠ 𝑈)) |
87 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (𝑧 − 𝑈) = (𝑆 − 𝑈)) |
88 | 87 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → (abs‘(𝑧 − 𝑈)) = (abs‘(𝑆 − 𝑈))) |
89 | 88 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → ((abs‘(𝑧 − 𝑈)) < 𝑇 ↔ (abs‘(𝑆 − 𝑈)) < 𝑇)) |
90 | 86, 89 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑆 → ((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) ↔ (𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇))) |
91 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑆 → (𝐹‘𝑧) = (𝐹‘𝑆)) |
92 | 91 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑆 → ((𝐹‘𝑧) − (𝐹‘𝑈)) = ((𝐹‘𝑆) − (𝐹‘𝑈))) |
93 | 92, 87 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) = (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) |
94 | 93 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → ((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈)) = ((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) |
95 | 94 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) = (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈)))) |
96 | 95 | breq1d 4663 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑆 → ((abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈) ↔ (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))) |
97 | 90, 96 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑧 = 𝑆 → (((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)) ↔ ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))) |
98 | 97 | rspcv 3305 |
. . . . . . . 8
⊢ (𝑆 ∈ (𝑋 ∖ {𝑈}) → (∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)) → ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))) |
99 | 77, 78, 85, 98 | syl3c 66 |
. . . . . . 7
⊢ (𝜑 → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)) |
100 | 1, 74 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ) |
101 | 26, 9 | sseldd 3604 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ 𝑋) |
102 | 1, 101 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑈) ∈ ℝ) |
103 | 100, 102 | resubcld 10458 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ) |
104 | 53, 19 | resubcld 10458 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 − 𝑈) ∈ ℝ) |
105 | 19, 53 | posdifd 10614 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈 < 𝑆 ↔ 0 < (𝑆 − 𝑈))) |
106 | 62, 105 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (𝑆 − 𝑈)) |
107 | 104, 106 | elrpd 11869 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 − 𝑈) ∈
ℝ+) |
108 | 103, 107 | rerpdivcld 11903 |
. . . . . . . 8
⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∈ ℝ) |
109 | 108, 6, 6 | absdifltd 14172 |
. . . . . . 7
⊢ (𝜑 → ((abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈) ↔ ((((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + ((ℝ D 𝐹)‘𝑈))))) |
110 | 99, 109 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → ((((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + ((ℝ D 𝐹)‘𝑈)))) |
111 | 110 | simpld 475 |
. . . . 5
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) |
112 | 8, 111 | eqbrtrrd 4677 |
. . . 4
⊢ (𝜑 → 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))) |
113 | | gt0div 10889 |
. . . . 5
⊢ ((((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ ∧ (𝑆 − 𝑈) ∈ ℝ ∧ 0 < (𝑆 − 𝑈)) → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)))) |
114 | 103, 104,
106, 113 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)))) |
115 | 112, 114 | mpbird 247 |
. . 3
⊢ (𝜑 → 0 < ((𝐹‘𝑆) − (𝐹‘𝑈))) |
116 | 102, 100 | posdifd 10614 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑈) < (𝐹‘𝑆) ↔ 0 < ((𝐹‘𝑆) − (𝐹‘𝑈)))) |
117 | 115, 116 | mpbird 247 |
. 2
⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑆)) |
118 | | dvferm1.r |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈)) |
119 | | fveq2 6191 |
. . . . . 6
⊢ (𝑦 = 𝑆 → (𝐹‘𝑦) = (𝐹‘𝑆)) |
120 | 119 | breq1d 4663 |
. . . . 5
⊢ (𝑦 = 𝑆 → ((𝐹‘𝑦) ≤ (𝐹‘𝑈) ↔ (𝐹‘𝑆) ≤ (𝐹‘𝑈))) |
121 | 120 | rspcv 3305 |
. . . 4
⊢ (𝑆 ∈ (𝑈(,)𝐵) → (∀𝑦 ∈ (𝑈(,)𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑈) → (𝐹‘𝑆) ≤ (𝐹‘𝑈))) |
122 | 73, 118, 121 | sylc 65 |
. . 3
⊢ (𝜑 → (𝐹‘𝑆) ≤ (𝐹‘𝑈)) |
123 | 100, 102 | lenltd 10183 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑆) ≤ (𝐹‘𝑈) ↔ ¬ (𝐹‘𝑈) < (𝐹‘𝑆))) |
124 | 122, 123 | mpbid 222 |
. 2
⊢ (𝜑 → ¬ (𝐹‘𝑈) < (𝐹‘𝑆)) |
125 | 117, 124 | pm2.65i 185 |
1
⊢ ¬
𝜑 |