MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvferm2lem Structured version   Visualization version   GIF version

Theorem dvferm2lem 24498
Description: Lemma for dvferm 24500. (Contributed by Mario Carneiro, 24-Feb-2015.)
Hypotheses
Ref Expression
dvferm.a (𝜑𝐹:𝑋⟶ℝ)
dvferm.b (𝜑𝑋 ⊆ ℝ)
dvferm.u (𝜑𝑈 ∈ (𝐴(,)𝐵))
dvferm.s (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)
dvferm.d (𝜑𝑈 ∈ dom (ℝ D 𝐹))
dvferm2.r (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹𝑦) ≤ (𝐹𝑈))
dvferm2.z (𝜑 → ((ℝ D 𝐹)‘𝑈) < 0)
dvferm2.t (𝜑𝑇 ∈ ℝ+)
dvferm2.l (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑇) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))
dvferm2.x 𝑆 = ((if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) + 𝑈) / 2)
Assertion
Ref Expression
dvferm2lem ¬ 𝜑
Distinct variable groups:   𝑦,𝑧,𝐴   𝑦,𝐵,𝑧   𝑦,𝐹,𝑧   𝑦,𝑈,𝑧   𝑦,𝑋,𝑧   𝜑,𝑦   𝑦,𝑆,𝑧   𝑧,𝑇
Allowed substitution hints:   𝜑(𝑧)   𝑇(𝑦)

Proof of Theorem dvferm2lem
StepHypRef Expression
1 dvferm2.x . . . . . . . . . . . 12 𝑆 = ((if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) + 𝑈) / 2)
2 mnfxr 10687 . . . . . . . . . . . . . . . 16 -∞ ∈ ℝ*
32a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → -∞ ∈ ℝ*)
4 ioossre 12788 . . . . . . . . . . . . . . . . . . 19 (𝐴(,)𝐵) ⊆ ℝ
5 dvferm.u . . . . . . . . . . . . . . . . . . 19 (𝜑𝑈 ∈ (𝐴(,)𝐵))
64, 5sseldi 3969 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ∈ ℝ)
7 dvferm2.t . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ ℝ+)
87rpred 12421 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ ℝ)
96, 8resubcld 11057 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈𝑇) ∈ ℝ)
109rexrd 10680 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑈𝑇) ∈ ℝ*)
11 ne0i 4304 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
12 ndmioo 12755 . . . . . . . . . . . . . . . . . . 19 (¬ (𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = ∅)
1312necon1ai 3048 . . . . . . . . . . . . . . . . . 18 ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
145, 11, 133syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
1514simpld 495 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℝ*)
1610, 15ifcld 4515 . . . . . . . . . . . . . . 15 (𝜑 → if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) ∈ ℝ*)
176rexrd 10680 . . . . . . . . . . . . . . 15 (𝜑𝑈 ∈ ℝ*)
189mnfltd 12509 . . . . . . . . . . . . . . . 16 (𝜑 → -∞ < (𝑈𝑇))
19 xrmax2 12559 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℝ* ∧ (𝑈𝑇) ∈ ℝ*) → (𝑈𝑇) ≤ if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴))
2015, 10, 19syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑈𝑇) ≤ if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴))
213, 10, 16, 18, 20xrltletrd 12544 . . . . . . . . . . . . . . 15 (𝜑 → -∞ < if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴))
226, 7ltsubrpd 12453 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑈𝑇) < 𝑈)
23 eliooord 12786 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑈𝑈 < 𝐵))
245, 23syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 < 𝑈𝑈 < 𝐵))
2524simpld 495 . . . . . . . . . . . . . . . 16 (𝜑𝐴 < 𝑈)
26 breq1 5066 . . . . . . . . . . . . . . . . 17 ((𝑈𝑇) = if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) → ((𝑈𝑇) < 𝑈 ↔ if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < 𝑈))
27 breq1 5066 . . . . . . . . . . . . . . . . 17 (𝐴 = if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) → (𝐴 < 𝑈 ↔ if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < 𝑈))
2826, 27ifboth 4508 . . . . . . . . . . . . . . . 16 (((𝑈𝑇) < 𝑈𝐴 < 𝑈) → if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < 𝑈)
2922, 25, 28syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < 𝑈)
30 xrre2 12553 . . . . . . . . . . . . . . 15 (((-∞ ∈ ℝ* ∧ if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) ∈ ℝ*𝑈 ∈ ℝ*) ∧ (-∞ < if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) ∧ if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < 𝑈)) → if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) ∈ ℝ)
313, 16, 17, 21, 29, 30syl32anc 1372 . . . . . . . . . . . . . 14 (𝜑 → if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) ∈ ℝ)
3231, 6readdcld 10659 . . . . . . . . . . . . 13 (𝜑 → (if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) + 𝑈) ∈ ℝ)
3332rehalfcld 11873 . . . . . . . . . . . 12 (𝜑 → ((if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) + 𝑈) / 2) ∈ ℝ)
341, 33eqeltrid 2922 . . . . . . . . . . 11 (𝜑𝑆 ∈ ℝ)
35 avglt2 11865 . . . . . . . . . . . . . 14 ((if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) ∈ ℝ ∧ 𝑈 ∈ ℝ) → (if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < 𝑈 ↔ ((if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) + 𝑈) / 2) < 𝑈))
3631, 6, 35syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < 𝑈 ↔ ((if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) + 𝑈) / 2) < 𝑈))
3729, 36mpbid 233 . . . . . . . . . . . 12 (𝜑 → ((if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) + 𝑈) / 2) < 𝑈)
381, 37eqbrtrid 5098 . . . . . . . . . . 11 (𝜑𝑆 < 𝑈)
3934, 38ltned 10765 . . . . . . . . . 10 (𝜑𝑆𝑈)
4034, 6, 38ltled 10777 . . . . . . . . . . . 12 (𝜑𝑆𝑈)
4134, 6, 40abssuble0d 14782 . . . . . . . . . . 11 (𝜑 → (abs‘(𝑆𝑈)) = (𝑈𝑆))
42 avglt1 11864 . . . . . . . . . . . . . . . 16 ((if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) ∈ ℝ ∧ 𝑈 ∈ ℝ) → (if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < 𝑈 ↔ if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) + 𝑈) / 2)))
4331, 6, 42syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < 𝑈 ↔ if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) + 𝑈) / 2)))
4429, 43mpbid 233 . . . . . . . . . . . . . 14 (𝜑 → if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) + 𝑈) / 2))
4544, 1breqtrrdi 5105 . . . . . . . . . . . . 13 (𝜑 → if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴) < 𝑆)
469, 31, 34, 20, 45lelttrd 10787 . . . . . . . . . . . 12 (𝜑 → (𝑈𝑇) < 𝑆)
476, 8, 34, 46ltsub23d 11234 . . . . . . . . . . 11 (𝜑 → (𝑈𝑆) < 𝑇)
4841, 47eqbrtrd 5085 . . . . . . . . . 10 (𝜑 → (abs‘(𝑆𝑈)) < 𝑇)
49 neeq1 3083 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → (𝑧𝑈𝑆𝑈))
50 fvoveq1 7171 . . . . . . . . . . . . . 14 (𝑧 = 𝑆 → (abs‘(𝑧𝑈)) = (abs‘(𝑆𝑈)))
5150breq1d 5073 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → ((abs‘(𝑧𝑈)) < 𝑇 ↔ (abs‘(𝑆𝑈)) < 𝑇))
5249, 51anbi12d 630 . . . . . . . . . . . 12 (𝑧 = 𝑆 → ((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑇) ↔ (𝑆𝑈 ∧ (abs‘(𝑆𝑈)) < 𝑇)))
53 fveq2 6667 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑆 → (𝐹𝑧) = (𝐹𝑆))
5453oveq1d 7163 . . . . . . . . . . . . . . 15 (𝑧 = 𝑆 → ((𝐹𝑧) − (𝐹𝑈)) = ((𝐹𝑆) − (𝐹𝑈)))
55 oveq1 7155 . . . . . . . . . . . . . . 15 (𝑧 = 𝑆 → (𝑧𝑈) = (𝑆𝑈))
5654, 55oveq12d 7166 . . . . . . . . . . . . . 14 (𝑧 = 𝑆 → (((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) = (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)))
5756fvoveq1d 7170 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) = (abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))))
5857breq1d 5073 . . . . . . . . . . . 12 (𝑧 = 𝑆 → ((abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈) ↔ (abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))
5952, 58imbi12d 346 . . . . . . . . . . 11 (𝑧 = 𝑆 → (((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑇) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)) ↔ ((𝑆𝑈 ∧ (abs‘(𝑆𝑈)) < 𝑇) → (abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))))
60 dvferm2.l . . . . . . . . . . 11 (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑇) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))
6114simprd 496 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℝ*)
6224simprd 496 . . . . . . . . . . . . . . . 16 (𝜑𝑈 < 𝐵)
6317, 61, 62xrltled 12533 . . . . . . . . . . . . . . 15 (𝜑𝑈𝐵)
64 iooss2 12764 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℝ*𝑈𝐵) → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵))
6561, 63, 64syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵))
66 dvferm.s . . . . . . . . . . . . . 14 (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)
6765, 66sstrd 3981 . . . . . . . . . . . . 13 (𝜑 → (𝐴(,)𝑈) ⊆ 𝑋)
6834rexrd 10680 . . . . . . . . . . . . . . 15 (𝜑𝑆 ∈ ℝ*)
69 xrmax1 12558 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ* ∧ (𝑈𝑇) ∈ ℝ*) → 𝐴 ≤ if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴))
7015, 10, 69syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑𝐴 ≤ if(𝐴 ≤ (𝑈𝑇), (𝑈𝑇), 𝐴))
7115, 16, 68, 70, 45xrlelttrd 12543 . . . . . . . . . . . . . 14 (𝜑𝐴 < 𝑆)
72 elioo2 12769 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ*𝑈 ∈ ℝ*) → (𝑆 ∈ (𝐴(,)𝑈) ↔ (𝑆 ∈ ℝ ∧ 𝐴 < 𝑆𝑆 < 𝑈)))
7315, 17, 72syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑆 ∈ (𝐴(,)𝑈) ↔ (𝑆 ∈ ℝ ∧ 𝐴 < 𝑆𝑆 < 𝑈)))
7434, 71, 38, 73mpbir3and 1336 . . . . . . . . . . . . 13 (𝜑𝑆 ∈ (𝐴(,)𝑈))
7567, 74sseldd 3972 . . . . . . . . . . . 12 (𝜑𝑆𝑋)
76 eldifsn 4718 . . . . . . . . . . . 12 (𝑆 ∈ (𝑋 ∖ {𝑈}) ↔ (𝑆𝑋𝑆𝑈))
7775, 39, 76sylanbrc 583 . . . . . . . . . . 11 (𝜑𝑆 ∈ (𝑋 ∖ {𝑈}))
7859, 60, 77rspcdva 3629 . . . . . . . . . 10 (𝜑 → ((𝑆𝑈 ∧ (abs‘(𝑆𝑈)) < 𝑇) → (abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))
7939, 48, 78mp2and 695 . . . . . . . . 9 (𝜑 → (abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))
80 dvferm.a . . . . . . . . . . . . 13 (𝜑𝐹:𝑋⟶ℝ)
8180, 75ffvelrnd 6848 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑆) ∈ ℝ)
8266, 5sseldd 3972 . . . . . . . . . . . . 13 (𝜑𝑈𝑋)
8380, 82ffvelrnd 6848 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑈) ∈ ℝ)
8481, 83resubcld 11057 . . . . . . . . . . 11 (𝜑 → ((𝐹𝑆) − (𝐹𝑈)) ∈ ℝ)
8534, 6resubcld 11057 . . . . . . . . . . 11 (𝜑 → (𝑆𝑈) ∈ ℝ)
8634recnd 10658 . . . . . . . . . . . 12 (𝜑𝑆 ∈ ℂ)
876recnd 10658 . . . . . . . . . . . 12 (𝜑𝑈 ∈ ℂ)
8886, 87, 39subne0d 10995 . . . . . . . . . . 11 (𝜑 → (𝑆𝑈) ≠ 0)
8984, 85, 88redivcld 11457 . . . . . . . . . 10 (𝜑 → (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) ∈ ℝ)
90 dvferm.b . . . . . . . . . . . 12 (𝜑𝑋 ⊆ ℝ)
91 dvfre 24463 . . . . . . . . . . . 12 ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
9280, 90, 91syl2anc 584 . . . . . . . . . . 11 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
93 dvferm.d . . . . . . . . . . 11 (𝜑𝑈 ∈ dom (ℝ D 𝐹))
9492, 93ffvelrnd 6848 . . . . . . . . . 10 (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ)
9594renegcld 11056 . . . . . . . . . 10 (𝜑 → -((ℝ D 𝐹)‘𝑈) ∈ ℝ)
9689, 94, 95absdifltd 14783 . . . . . . . . 9 (𝜑 → ((abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈) ↔ ((((ℝ D 𝐹)‘𝑈) − -((ℝ D 𝐹)‘𝑈)) < (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) ∧ (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)))))
9779, 96mpbid 233 . . . . . . . 8 (𝜑 → ((((ℝ D 𝐹)‘𝑈) − -((ℝ D 𝐹)‘𝑈)) < (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) ∧ (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈))))
9897simprd 496 . . . . . . 7 (𝜑 → (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)))
9994recnd 10658 . . . . . . . 8 (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℂ)
10099negidd 10976 . . . . . . 7 (𝜑 → (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)) = 0)
10198, 100breqtrd 5089 . . . . . 6 (𝜑 → (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) < 0)
10289lt0neg1d 11198 . . . . . 6 (𝜑 → ((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) < 0 ↔ 0 < -(((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈))))
103101, 102mpbid 233 . . . . 5 (𝜑 → 0 < -(((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)))
10484recnd 10658 . . . . . 6 (𝜑 → ((𝐹𝑆) − (𝐹𝑈)) ∈ ℂ)
10585recnd 10658 . . . . . 6 (𝜑 → (𝑆𝑈) ∈ ℂ)
106104, 105, 88divneg2d 11419 . . . . 5 (𝜑 → -(((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) = (((𝐹𝑆) − (𝐹𝑈)) / -(𝑆𝑈)))
107103, 106breqtrd 5089 . . . 4 (𝜑 → 0 < (((𝐹𝑆) − (𝐹𝑈)) / -(𝑆𝑈)))
10885renegcld 11056 . . . . 5 (𝜑 → -(𝑆𝑈) ∈ ℝ)
10934, 6posdifd 11216 . . . . . . 7 (𝜑 → (𝑆 < 𝑈 ↔ 0 < (𝑈𝑆)))
11038, 109mpbid 233 . . . . . 6 (𝜑 → 0 < (𝑈𝑆))
11186, 87negsubdi2d 11002 . . . . . 6 (𝜑 → -(𝑆𝑈) = (𝑈𝑆))
112110, 111breqtrrd 5091 . . . . 5 (𝜑 → 0 < -(𝑆𝑈))
113 gt0div 11495 . . . . 5 ((((𝐹𝑆) − (𝐹𝑈)) ∈ ℝ ∧ -(𝑆𝑈) ∈ ℝ ∧ 0 < -(𝑆𝑈)) → (0 < ((𝐹𝑆) − (𝐹𝑈)) ↔ 0 < (((𝐹𝑆) − (𝐹𝑈)) / -(𝑆𝑈))))
11484, 108, 112, 113syl3anc 1365 . . . 4 (𝜑 → (0 < ((𝐹𝑆) − (𝐹𝑈)) ↔ 0 < (((𝐹𝑆) − (𝐹𝑈)) / -(𝑆𝑈))))
115107, 114mpbird 258 . . 3 (𝜑 → 0 < ((𝐹𝑆) − (𝐹𝑈)))
11683, 81posdifd 11216 . . 3 (𝜑 → ((𝐹𝑈) < (𝐹𝑆) ↔ 0 < ((𝐹𝑆) − (𝐹𝑈))))
117115, 116mpbird 258 . 2 (𝜑 → (𝐹𝑈) < (𝐹𝑆))
118 fveq2 6667 . . . . 5 (𝑦 = 𝑆 → (𝐹𝑦) = (𝐹𝑆))
119118breq1d 5073 . . . 4 (𝑦 = 𝑆 → ((𝐹𝑦) ≤ (𝐹𝑈) ↔ (𝐹𝑆) ≤ (𝐹𝑈)))
120 dvferm2.r . . . 4 (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹𝑦) ≤ (𝐹𝑈))
121119, 120, 74rspcdva 3629 . . 3 (𝜑 → (𝐹𝑆) ≤ (𝐹𝑈))
12281, 83, 121lensymd 10780 . 2 (𝜑 → ¬ (𝐹𝑈) < (𝐹𝑆))
123117, 122pm2.65i 195 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  wne 3021  wral 3143  cdif 3937  wss 3940  c0 4295  ifcif 4470  {csn 4564   class class class wbr 5063  dom cdm 5554  wf 6348  cfv 6352  (class class class)co 7148  cr 10525  0cc0 10526   + caddc 10529  -∞cmnf 10662  *cxr 10663   < clt 10664  cle 10665  cmin 10859  -cneg 10860   / cdiv 11286  2c2 11681  +crp 12379  (,)cioo 12728  abscabs 14583   D cdv 24376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-oadd 8097  df-er 8279  df-map 8398  df-pm 8399  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-fi 8864  df-sup 8895  df-inf 8896  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-z 11971  df-dec 12088  df-uz 12233  df-q 12338  df-rp 12380  df-xneg 12497  df-xadd 12498  df-xmul 12499  df-ioo 12732  df-icc 12735  df-fz 12883  df-seq 13360  df-exp 13420  df-cj 14448  df-re 14449  df-im 14450  df-sqrt 14584  df-abs 14585  df-struct 16475  df-ndx 16476  df-slot 16477  df-base 16479  df-plusg 16568  df-mulr 16569  df-starv 16570  df-tset 16574  df-ple 16575  df-ds 16577  df-unif 16578  df-rest 16686  df-topn 16687  df-topgen 16707  df-psmet 20453  df-xmet 20454  df-met 20455  df-bl 20456  df-mopn 20457  df-fbas 20458  df-fg 20459  df-cnfld 20462  df-top 21418  df-topon 21435  df-topsp 21457  df-bases 21470  df-cld 21543  df-ntr 21544  df-cls 21545  df-nei 21622  df-lp 21660  df-perf 21661  df-cn 21751  df-cnp 21752  df-haus 21839  df-fil 22370  df-fm 22462  df-flim 22463  df-flf 22464  df-xms 22845  df-ms 22846  df-cncf 23401  df-limc 24379  df-dv 24380
This theorem is referenced by:  dvferm2  24499
  Copyright terms: Public domain W3C validator