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

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

Proof of Theorem dvferm1lem
StepHypRef Expression
1 dvferm.a . . . . . . . . 9 (𝜑𝐹:𝑋⟶ℝ)
2 dvferm.b . . . . . . . . 9 (𝜑𝑋 ⊆ ℝ)
3 dvfre 23396 . . . . . . . . 9 ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
41, 2, 3syl2anc 690 . . . . . . . 8 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
5 dvferm.d . . . . . . . 8 (𝜑𝑈 ∈ dom (ℝ D 𝐹))
64, 5ffvelrnd 6151 . . . . . . 7 (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ)
76recnd 9822 . . . . . 6 (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℂ)
87subidd 10130 . . . . 5 (𝜑 → (((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) = 0)
9 dvferm.u . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ (𝐴(,)𝐵))
10 ne0i 3783 . . . . . . . . . . . . . 14 (𝑈 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
11 ndmioo 11941 . . . . . . . . . . . . . . 15 (¬ (𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = ∅)
1211necon1ai 2713 . . . . . . . . . . . . . 14 ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
139, 10, 123syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
1413simpld 473 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ*)
15 eliooord 11972 . . . . . . . . . . . . . . 15 (𝑈 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑈𝑈 < 𝐵))
169, 15syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 < 𝑈𝑈 < 𝐵))
1716simpld 473 . . . . . . . . . . . . 13 (𝜑𝐴 < 𝑈)
18 ioossre 11974 . . . . . . . . . . . . . . . 16 (𝐴(,)𝐵) ⊆ ℝ
1918, 9sseldi 3470 . . . . . . . . . . . . . . 15 (𝜑𝑈 ∈ ℝ)
2019rexrd 9843 . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ ℝ*)
21 xrltle 11726 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝑈 ∈ ℝ*) → (𝐴 < 𝑈𝐴𝑈))
2214, 20, 21syl2anc 690 . . . . . . . . . . . . 13 (𝜑 → (𝐴 < 𝑈𝐴𝑈))
2317, 22mpd 15 . . . . . . . . . . . 12 (𝜑𝐴𝑈)
24 iooss1 11949 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ*𝐴𝑈) → (𝑈(,)𝐵) ⊆ (𝐴(,)𝐵))
2514, 23, 24syl2anc 690 . . . . . . . . . . 11 (𝜑 → (𝑈(,)𝐵) ⊆ (𝐴(,)𝐵))
26 dvferm.s . . . . . . . . . . 11 (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)
2725, 26sstrd 3482 . . . . . . . . . 10 (𝜑 → (𝑈(,)𝐵) ⊆ 𝑋)
28 dvferm1.x . . . . . . . . . . . 12 𝑆 = ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2)
2913simprd 477 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℝ*)
30 dvferm1.t . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ ℝ+)
3130rpred 11613 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ ℝ)
3219, 31readdcld 9823 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈 + 𝑇) ∈ ℝ)
3332rexrd 9843 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑈 + 𝑇) ∈ ℝ*)
3429, 33ifcld 3984 . . . . . . . . . . . . . . 15 (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ*)
35 mnfxr 11692 . . . . . . . . . . . . . . . . . 18 -∞ ∈ ℝ*
3635a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → -∞ ∈ ℝ*)
37 mnflt 11703 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ ℝ → -∞ < 𝑈)
3819, 37syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → -∞ < 𝑈)
3916simprd 477 . . . . . . . . . . . . . . . . 17 (𝜑𝑈 < 𝐵)
4036, 20, 29, 38, 39xrlttrd 11734 . . . . . . . . . . . . . . . 16 (𝜑 → -∞ < 𝐵)
41 mnflt 11703 . . . . . . . . . . . . . . . . 17 ((𝑈 + 𝑇) ∈ ℝ → -∞ < (𝑈 + 𝑇))
4232, 41syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → -∞ < (𝑈 + 𝑇))
43 breq2 4485 . . . . . . . . . . . . . . . . 17 (𝐵 = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (-∞ < 𝐵 ↔ -∞ < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))))
44 breq2 4485 . . . . . . . . . . . . . . . . 17 ((𝑈 + 𝑇) = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (-∞ < (𝑈 + 𝑇) ↔ -∞ < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))))
4543, 44ifboth 3977 . . . . . . . . . . . . . . . 16 ((-∞ < 𝐵 ∧ -∞ < (𝑈 + 𝑇)) → -∞ < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))
4640, 42, 45syl2anc 690 . . . . . . . . . . . . . . 15 (𝜑 → -∞ < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))
47 xrmin2 11751 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ ℝ* ∧ (𝑈 + 𝑇) ∈ ℝ*) → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ (𝑈 + 𝑇))
4829, 33, 47syl2anc 690 . . . . . . . . . . . . . . 15 (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ (𝑈 + 𝑇))
49 xrre 11742 . . . . . . . . . . . . . . 15 (((if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ* ∧ (𝑈 + 𝑇) ∈ ℝ) ∧ (-∞ < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∧ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ (𝑈 + 𝑇))) → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ)
5034, 32, 46, 48, 49syl22anc 1318 . . . . . . . . . . . . . 14 (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ)
5119, 50readdcld 9823 . . . . . . . . . . . . 13 (𝜑 → (𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) ∈ ℝ)
5251rehalfcld 11033 . . . . . . . . . . . 12 (𝜑 → ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) ∈ ℝ)
5328, 52syl5eqel 2596 . . . . . . . . . . 11 (𝜑𝑆 ∈ ℝ)
5419, 30ltaddrpd 11646 . . . . . . . . . . . . . 14 (𝜑𝑈 < (𝑈 + 𝑇))
55 breq2 4485 . . . . . . . . . . . . . . 15 (𝐵 = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (𝑈 < 𝐵𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))))
56 breq2 4485 . . . . . . . . . . . . . . 15 ((𝑈 + 𝑇) = if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) → (𝑈 < (𝑈 + 𝑇) ↔ 𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))))
5755, 56ifboth 3977 . . . . . . . . . . . . . 14 ((𝑈 < 𝐵𝑈 < (𝑈 + 𝑇)) → 𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))
5839, 54, 57syl2anc 690 . . . . . . . . . . . . 13 (𝜑𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))
59 avglt1 11024 . . . . . . . . . . . . . 14 ((𝑈 ∈ ℝ ∧ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ) → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ 𝑈 < ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2)))
6019, 50, 59syl2anc 690 . . . . . . . . . . . . 13 (𝜑 → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ 𝑈 < ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2)))
6158, 60mpbid 220 . . . . . . . . . . . 12 (𝜑𝑈 < ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2))
6261, 28syl6breqr 4523 . . . . . . . . . . 11 (𝜑𝑈 < 𝑆)
6353rexrd 9843 . . . . . . . . . . . 12 (𝜑𝑆 ∈ ℝ*)
64 avglt2 11025 . . . . . . . . . . . . . . 15 ((𝑈 ∈ ℝ ∧ if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ∈ ℝ) → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))))
6519, 50, 64syl2anc 690 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ↔ ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))))
6658, 65mpbid 220 . . . . . . . . . . . . 13 (𝜑 → ((𝑈 + if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇))) / 2) < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))
6728, 66syl5eqbr 4516 . . . . . . . . . . . 12 (𝜑𝑆 < if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)))
68 xrmin1 11750 . . . . . . . . . . . . 13 ((𝐵 ∈ ℝ* ∧ (𝑈 + 𝑇) ∈ ℝ*) → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ 𝐵)
6929, 33, 68syl2anc 690 . . . . . . . . . . . 12 (𝜑 → if(𝐵 ≤ (𝑈 + 𝑇), 𝐵, (𝑈 + 𝑇)) ≤ 𝐵)
7063, 34, 29, 67, 69xrltletrd 11736 . . . . . . . . . . 11 (𝜑𝑆 < 𝐵)
71 elioo2 11955 . . . . . . . . . . . 12 ((𝑈 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑆 ∈ (𝑈(,)𝐵) ↔ (𝑆 ∈ ℝ ∧ 𝑈 < 𝑆𝑆 < 𝐵)))
7220, 29, 71syl2anc 690 . . . . . . . . . . 11 (𝜑 → (𝑆 ∈ (𝑈(,)𝐵) ↔ (𝑆 ∈ ℝ ∧ 𝑈 < 𝑆𝑆 < 𝐵)))
7353, 62, 70, 72mpbir3and 1237 . . . . . . . . . 10 (𝜑𝑆 ∈ (𝑈(,)𝐵))
7427, 73sseldd 3473 . . . . . . . . 9 (𝜑𝑆𝑋)
7519, 62gtned 9922 . . . . . . . . 9 (𝜑𝑆𝑈)
76 eldifsn 4163 . . . . . . . . 9 (𝑆 ∈ (𝑋 ∖ {𝑈}) ↔ (𝑆𝑋𝑆𝑈))
7774, 75, 76sylanbrc 694 . . . . . . . 8 (𝜑𝑆 ∈ (𝑋 ∖ {𝑈}))
78 dvferm1.l . . . . . . . 8 (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑇) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))
7919, 53, 62ltled 9935 . . . . . . . . . . 11 (𝜑𝑈𝑆)
8019, 53, 79abssubge0d 13875 . . . . . . . . . 10 (𝜑 → (abs‘(𝑆𝑈)) = (𝑆𝑈))
8153, 50, 32, 67, 48ltletrd 9947 . . . . . . . . . . 11 (𝜑𝑆 < (𝑈 + 𝑇))
8253, 19, 31ltsubadd2d 10373 . . . . . . . . . . 11 (𝜑 → ((𝑆𝑈) < 𝑇𝑆 < (𝑈 + 𝑇)))
8381, 82mpbird 245 . . . . . . . . . 10 (𝜑 → (𝑆𝑈) < 𝑇)
8480, 83eqbrtrd 4503 . . . . . . . . 9 (𝜑 → (abs‘(𝑆𝑈)) < 𝑇)
8575, 84jca 552 . . . . . . . 8 (𝜑 → (𝑆𝑈 ∧ (abs‘(𝑆𝑈)) < 𝑇))
86 neeq1 2748 . . . . . . . . . . 11 (𝑧 = 𝑆 → (𝑧𝑈𝑆𝑈))
87 oveq1 6432 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → (𝑧𝑈) = (𝑆𝑈))
8887fveq2d 5990 . . . . . . . . . . . 12 (𝑧 = 𝑆 → (abs‘(𝑧𝑈)) = (abs‘(𝑆𝑈)))
8988breq1d 4491 . . . . . . . . . . 11 (𝑧 = 𝑆 → ((abs‘(𝑧𝑈)) < 𝑇 ↔ (abs‘(𝑆𝑈)) < 𝑇))
9086, 89anbi12d 742 . . . . . . . . . 10 (𝑧 = 𝑆 → ((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑇) ↔ (𝑆𝑈 ∧ (abs‘(𝑆𝑈)) < 𝑇)))
91 fveq2 5986 . . . . . . . . . . . . . . 15 (𝑧 = 𝑆 → (𝐹𝑧) = (𝐹𝑆))
9291oveq1d 6440 . . . . . . . . . . . . . 14 (𝑧 = 𝑆 → ((𝐹𝑧) − (𝐹𝑈)) = ((𝐹𝑆) − (𝐹𝑈)))
9392, 87oveq12d 6443 . . . . . . . . . . . . 13 (𝑧 = 𝑆 → (((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) = (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)))
9493oveq1d 6440 . . . . . . . . . . . 12 (𝑧 = 𝑆 → ((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈)) = ((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈)))
9594fveq2d 5990 . . . . . . . . . . 11 (𝑧 = 𝑆 → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) = (abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))))
9695breq1d 4491 . . . . . . . . . 10 (𝑧 = 𝑆 → ((abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈) ↔ (abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)))
9790, 96imbi12d 332 . . . . . . . . 9 (𝑧 = 𝑆 → (((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑇) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)) ↔ ((𝑆𝑈 ∧ (abs‘(𝑆𝑈)) < 𝑇) → (abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))))
9897rspcv 3182 . . . . . . . 8 (𝑆 ∈ (𝑋 ∖ {𝑈}) → (∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧𝑈 ∧ (abs‘(𝑧𝑈)) < 𝑇) → (abs‘((((𝐹𝑧) − (𝐹𝑈)) / (𝑧𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈)) → ((𝑆𝑈 ∧ (abs‘(𝑆𝑈)) < 𝑇) → (abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))))
9977, 78, 85, 98syl3c 63 . . . . . . 7 (𝜑 → (abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈))
1001, 74ffvelrnd 6151 . . . . . . . . . 10 (𝜑 → (𝐹𝑆) ∈ ℝ)
10126, 9sseldd 3473 . . . . . . . . . . 11 (𝜑𝑈𝑋)
1021, 101ffvelrnd 6151 . . . . . . . . . 10 (𝜑 → (𝐹𝑈) ∈ ℝ)
103100, 102resubcld 10208 . . . . . . . . 9 (𝜑 → ((𝐹𝑆) − (𝐹𝑈)) ∈ ℝ)
10453, 19resubcld 10208 . . . . . . . . . 10 (𝜑 → (𝑆𝑈) ∈ ℝ)
10519, 53posdifd 10362 . . . . . . . . . . 11 (𝜑 → (𝑈 < 𝑆 ↔ 0 < (𝑆𝑈)))
10662, 105mpbid 220 . . . . . . . . . 10 (𝜑 → 0 < (𝑆𝑈))
107104, 106elrpd 11610 . . . . . . . . 9 (𝜑 → (𝑆𝑈) ∈ ℝ+)
108103, 107rerpdivcld 11644 . . . . . . . 8 (𝜑 → (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) ∈ ℝ)
109108, 6, 6absdifltd 13877 . . . . . . 7 (𝜑 → ((abs‘((((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) − ((ℝ D 𝐹)‘𝑈))) < ((ℝ D 𝐹)‘𝑈) ↔ ((((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) < (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) ∧ (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) < (((ℝ D 𝐹)‘𝑈) + ((ℝ D 𝐹)‘𝑈)))))
11099, 109mpbid 220 . . . . . 6 (𝜑 → ((((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) < (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) ∧ (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)) < (((ℝ D 𝐹)‘𝑈) + ((ℝ D 𝐹)‘𝑈))))
111110simpld 473 . . . . 5 (𝜑 → (((ℝ D 𝐹)‘𝑈) − ((ℝ D 𝐹)‘𝑈)) < (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)))
1128, 111eqbrtrrd 4505 . . . 4 (𝜑 → 0 < (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈)))
113 gt0div 10637 . . . . 5 ((((𝐹𝑆) − (𝐹𝑈)) ∈ ℝ ∧ (𝑆𝑈) ∈ ℝ ∧ 0 < (𝑆𝑈)) → (0 < ((𝐹𝑆) − (𝐹𝑈)) ↔ 0 < (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈))))
114103, 104, 106, 113syl3anc 1317 . . . 4 (𝜑 → (0 < ((𝐹𝑆) − (𝐹𝑈)) ↔ 0 < (((𝐹𝑆) − (𝐹𝑈)) / (𝑆𝑈))))
115112, 114mpbird 245 . . 3 (𝜑 → 0 < ((𝐹𝑆) − (𝐹𝑈)))
116102, 100posdifd 10362 . . 3 (𝜑 → ((𝐹𝑈) < (𝐹𝑆) ↔ 0 < ((𝐹𝑆) − (𝐹𝑈))))
117115, 116mpbird 245 . 2 (𝜑 → (𝐹𝑈) < (𝐹𝑆))
118 dvferm1.r . . . 4 (𝜑 → ∀𝑦 ∈ (𝑈(,)𝐵)(𝐹𝑦) ≤ (𝐹𝑈))
119 fveq2 5986 . . . . . 6 (𝑦 = 𝑆 → (𝐹𝑦) = (𝐹𝑆))
120119breq1d 4491 . . . . 5 (𝑦 = 𝑆 → ((𝐹𝑦) ≤ (𝐹𝑈) ↔ (𝐹𝑆) ≤ (𝐹𝑈)))
121120rspcv 3182 . . . 4 (𝑆 ∈ (𝑈(,)𝐵) → (∀𝑦 ∈ (𝑈(,)𝐵)(𝐹𝑦) ≤ (𝐹𝑈) → (𝐹𝑆) ≤ (𝐹𝑈)))
12273, 118, 121sylc 62 . . 3 (𝜑 → (𝐹𝑆) ≤ (𝐹𝑈))
123100, 102lenltd 9933 . . 3 (𝜑 → ((𝐹𝑆) ≤ (𝐹𝑈) ↔ ¬ (𝐹𝑈) < (𝐹𝑆)))
124122, 123mpbid 220 . 2 (𝜑 → ¬ (𝐹𝑈) < (𝐹𝑆))
125117, 124pm2.65i 183 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1938  wne 2684  wral 2800  cdif 3441  wss 3444  c0 3777  ifcif 3939  {csn 4028   class class class wbr 4481  dom cdm 4932  wf 5685  cfv 5689  (class class class)co 6425  cr 9689  0cc0 9690   + caddc 9693  -∞cmnf 9826  *cxr 9827   < clt 9828  cle 9829  cmin 10016   / cdiv 10432  2c2 10824  +crp 11573  (,)cioo 11914  abscabs 13679   D cdv 23309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6722  ax-cnex 9746  ax-resscn 9747  ax-1cn 9748  ax-icn 9749  ax-addcl 9750  ax-addrcl 9751  ax-mulcl 9752  ax-mulrcl 9753  ax-mulcom 9754  ax-addass 9755  ax-mulass 9756  ax-distr 9757  ax-i2m1 9758  ax-1ne0 9759  ax-1rid 9760  ax-rnegex 9761  ax-rrecex 9762  ax-cnre 9763  ax-pre-lttri 9764  ax-pre-lttrn 9765  ax-pre-ltadd 9766  ax-pre-mulgt0 9767  ax-pre-sup 9768
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-iin 4356  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-riota 6387  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-om 6833  df-1st 6933  df-2nd 6934  df-wrecs 7168  df-recs 7230  df-rdg 7268  df-1o 7322  df-oadd 7326  df-er 7504  df-map 7621  df-pm 7622  df-en 7717  df-dom 7718  df-sdom 7719  df-fin 7720  df-fi 8075  df-sup 8106  df-inf 8107  df-pnf 9830  df-mnf 9831  df-xr 9832  df-ltxr 9833  df-le 9834  df-sub 10018  df-neg 10019  df-div 10433  df-nn 10775  df-2 10833  df-3 10834  df-4 10835  df-5 10836  df-6 10837  df-7 10838  df-8 10839  df-9 10840  df-n0 11047  df-z 11118  df-dec 11233  df-uz 11427  df-q 11530  df-rp 11574  df-xneg 11687  df-xadd 11688  df-xmul 11689  df-ioo 11918  df-icc 11921  df-fz 12065  df-seq 12531  df-exp 12590  df-cj 13544  df-re 13545  df-im 13546  df-sqrt 13680  df-abs 13681  df-struct 15579  df-ndx 15580  df-slot 15581  df-base 15582  df-plusg 15663  df-mulr 15664  df-starv 15665  df-tset 15669  df-ple 15670  df-ds 15673  df-unif 15674  df-rest 15788  df-topn 15789  df-topgen 15809  df-psmet 19461  df-xmet 19462  df-met 19463  df-bl 19464  df-mopn 19465  df-fbas 19466  df-fg 19467  df-cnfld 19470  df-top 20422  df-bases 20423  df-topon 20424  df-topsp 20425  df-cld 20534  df-ntr 20535  df-cls 20536  df-nei 20613  df-lp 20651  df-perf 20652  df-cn 20742  df-cnp 20743  df-haus 20830  df-fil 21361  df-fm 21453  df-flim 21454  df-flf 21455  df-xms 21835  df-ms 21836  df-cncf 22410  df-limc 23312  df-dv 23313
This theorem is referenced by:  dvferm1  23428
  Copyright terms: Public domain W3C validator