dvferm2lem - Metamath Proof Explorer

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

Theorem dvferm2lem 25738

Description: Lemma for dvferm 25740. (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**
Step	Hyp	Ref	Expression
1		dvferm2.x	. . . . . . . . . . . 12 ⊢ 𝑆 = ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2)
2		mnfxr 11275	. . . . . . . . . . . . . . . 16 ⊢ -∞ ∈ ℝ^*
3	2	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -∞ ∈ ℝ^*)
4		ioossre 13389	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴(,)𝐵) ⊆ ℝ
5		dvferm.u	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑈 ∈ (𝐴(,)𝐵))
6	4, 5	sselid 3979	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 ∈ ℝ)
7		dvferm2.t	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
8	7	rpred 13020	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ∈ ℝ)
9	6, 8	resubcld 11646	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑈 − 𝑇) ∈ ℝ)
10	9	rexrd 11268	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑈 − 𝑇) ∈ ℝ^*)
11		ne0i 4333	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
12		ndmioo 13355	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴(,)𝐵) = ∅)
13	12	necon1ai 2966	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
14	5, 11, 13	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
15	14	simpld 493	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
16	10, 15	ifcld 4573	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ^*)
17	6	rexrd 11268	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ∈ ℝ^*)
18	9	mnfltd 13108	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -∞ < (𝑈 − 𝑇))
19		xrmax2 13159	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ^* ∧ (𝑈 − 𝑇) ∈ ℝ^*) → (𝑈 − 𝑇) ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴))
20	15, 10, 19	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑈 − 𝑇) ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴))
21	3, 10, 16, 18, 20	xrltletrd 13144	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -∞ < if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴))
22	6, 7	ltsubrpd 13052	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑈 − 𝑇) < 𝑈)
23		eliooord 13387	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵))
24	5, 23	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 < 𝑈 ∧ 𝑈 < 𝐵))
25	24	simpld 493	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 < 𝑈)
26		breq1 5150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 − 𝑇) = if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) → ((𝑈 − 𝑇) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈))
27		breq1 5150	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 = if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) → (𝐴 < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈))
28	26, 27	ifboth 4566	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 − 𝑇) < 𝑈 ∧ 𝐴 < 𝑈) → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)
29	22, 25, 28	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)
30		xrre2 13153	. . . . . . . . . . . . . . 15 ⊢ (((-∞ ∈ ℝ^* ∧ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ^* ∧ 𝑈 ∈ ℝ^*) ∧ (-∞ < if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∧ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈)) → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ)
31	3, 16, 17, 21, 29, 30	syl32anc 1376	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ)
32	31, 6	readdcld 11247	. . . . . . . . . . . . 13 ⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) ∈ ℝ)
33	32	rehalfcld 12463	. . . . . . . . . . . 12 ⊢ (𝜑 → ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) ∈ ℝ)
34	1, 33	eqeltrid 2835	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ ℝ)
35		avglt2 12455	. . . . . . . . . . . . . 14 ⊢ ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ ∧ 𝑈 ∈ ℝ) → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈))
36	31, 6, 35	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈))
37	29, 36	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2) < 𝑈)
38	1, 37	eqbrtrid 5182	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 < 𝑈)
39	34, 38	ltned 11354	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ≠ 𝑈)
40	34, 6, 38	ltled 11366	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ≤ 𝑈)
41	34, 6, 40	abssuble0d 15383	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) = (𝑈 − 𝑆))
42		avglt1 12454	. . . . . . . . . . . . . . . 16 ⊢ ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) ∈ ℝ ∧ 𝑈 ∈ ℝ) → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2)))
43	31, 6, 42	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑈 ↔ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2)))
44	29, 43	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < ((if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) + 𝑈) / 2))
45	44, 1	breqtrrdi 5189	. . . . . . . . . . . . 13 ⊢ (𝜑 → if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴) < 𝑆)
46	9, 31, 34, 20, 45	lelttrd 11376	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈 − 𝑇) < 𝑆)
47	6, 8, 34, 46	ltsub23d 11823	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 − 𝑆) < 𝑇)
48	41, 47	eqbrtrd 5169	. . . . . . . . . 10 ⊢ (𝜑 → (abs‘(𝑆 − 𝑈)) < 𝑇)
49		neeq1 3001	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑆 → (𝑧 ≠ 𝑈 ↔ 𝑆 ≠ 𝑈))
50		fvoveq1 7434	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑆 → (abs‘(𝑧 − 𝑈)) = (abs‘(𝑆 − 𝑈)))
51	50	breq1d 5157	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑆 → ((abs‘(𝑧 − 𝑈)) < 𝑇 ↔ (abs‘(𝑆 − 𝑈)) < 𝑇))
52	49, 51	anbi12d 629	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑆 → ((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) ↔ (𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇)))
53		fveq2 6890	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑆 → (𝐹‘𝑧) = (𝐹‘𝑆))
54	53	oveq1d 7426	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑆 → ((𝐹‘𝑧) − (𝐹‘𝑈)) = ((𝐹‘𝑆) − (𝐹‘𝑈)))
55		oveq1 7418	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑆 → (𝑧 − 𝑈) = (𝑆 − 𝑈))
56	54, 55	oveq12d 7429	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑆 → (((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) = (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)))
57	56	fvoveq1d 7433	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑆 → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) = (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))))
58	57	breq1d 5157	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑆 → ((abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈) ↔ (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))
59	52, 58	imbi12d 343	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑆 → (((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)) ↔ ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))))
60		dvferm2.l	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑧 ∈ (𝑋 ∖ {𝑈})((𝑧 ≠ 𝑈 ∧ (abs‘(𝑧 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑧) − (𝐹‘𝑈)) / (𝑧 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))
61	14	simprd 494	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
62	24	simprd 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 < 𝐵)
63	17, 61, 62	xrltled 13133	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ≤ 𝐵)
64		iooss2 13364	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝑈 ≤ 𝐵) → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵))
65	61, 63, 64	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(,)𝑈) ⊆ (𝐴(,)𝐵))
66		dvferm.s	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝑋)
67	65, 66	sstrd 3991	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴(,)𝑈) ⊆ 𝑋)
68	34	rexrd 11268	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ ℝ^*)
69		xrmax1 13158	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ^* ∧ (𝑈 − 𝑇) ∈ ℝ^*) → 𝐴 ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴))
70	15, 10, 69	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ≤ if(𝐴 ≤ (𝑈 − 𝑇), (𝑈 − 𝑇), 𝐴))
71	15, 16, 68, 70, 45	xrlelttrd 13143	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 < 𝑆)
72		elioo2 13369	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑈 ∈ ℝ^*) → (𝑆 ∈ (𝐴(,)𝑈) ↔ (𝑆 ∈ ℝ ∧ 𝐴 < 𝑆 ∧ 𝑆 < 𝑈)))
73	15, 17, 72	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆 ∈ (𝐴(,)𝑈) ↔ (𝑆 ∈ ℝ ∧ 𝐴 < 𝑆 ∧ 𝑆 < 𝑈)))
74	34, 71, 38, 73	mpbir3and 1340	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ (𝐴(,)𝑈))
75	67, 74	sseldd 3982	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ 𝑋)
76		eldifsn 4789	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (𝑋 ∖ {𝑈}) ↔ (𝑆 ∈ 𝑋 ∧ 𝑆 ≠ 𝑈))
77	75, 39, 76	sylanbrc 581	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ (𝑋 ∖ {𝑈}))
78	59, 60, 77	rspcdva 3612	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆 ≠ 𝑈 ∧ (abs‘(𝑆 − 𝑈)) < 𝑇) → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈)))
79	39, 48, 78	mp2and 695	. . . . . . . . 9 ⊢ (𝜑 → (abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈))
80		dvferm.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝑋⟶ℝ)
81	80, 75	ffvelcdmd 7086	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ)
82	66, 5	sseldd 3982	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ 𝑋)
83	80, 82	ffvelcdmd 7086	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘𝑈) ∈ ℝ)
84	81, 83	resubcld 11646	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ)
85	34, 6	resubcld 11646	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 − 𝑈) ∈ ℝ)
86	34	recnd 11246	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ ℂ)
87	6	recnd 11246	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ ℂ)
88	86, 87, 39	subne0d 11584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 − 𝑈) ≠ 0)
89	84, 85, 88	redivcld 12046	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∈ ℝ)
90		dvferm.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ⊆ ℝ)
91		dvfre 25703	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑋⟶ℝ ∧ 𝑋 ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
92	80, 90, 91	syl2anc 582	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
93		dvferm.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ dom (ℝ D 𝐹))
94	92, 93	ffvelcdmd 7086	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℝ)
95	94	renegcld 11645	. . . . . . . . . 10 ⊢ (𝜑 → -((ℝ D 𝐹)‘𝑈) ∈ ℝ)
96	89, 94, 95	absdifltd 15384	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) − ((ℝ D 𝐹)‘𝑈))) < -((ℝ D 𝐹)‘𝑈) ↔ ((((ℝ D 𝐹)‘𝑈) − -((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)))))
97	79, 96	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → ((((ℝ D 𝐹)‘𝑈) − -((ℝ D 𝐹)‘𝑈)) < (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) ∧ (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈))))
98	97	simprd 494	. . . . . . 7 ⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)))
99	94	recnd 11246	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D 𝐹)‘𝑈) ∈ ℂ)
100	99	negidd 11565	. . . . . . 7 ⊢ (𝜑 → (((ℝ D 𝐹)‘𝑈) + -((ℝ D 𝐹)‘𝑈)) = 0)
101	98, 100	breqtrd 5173	. . . . . 6 ⊢ (𝜑 → (((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < 0)
102	89	lt0neg1d 11787	. . . . . 6 ⊢ (𝜑 → ((((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) < 0 ↔ 0 < -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈))))
103	101, 102	mpbid 231	. . . . 5 ⊢ (𝜑 → 0 < -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)))
104	84	recnd 11246	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℂ)
105	85	recnd 11246	. . . . . 6 ⊢ (𝜑 → (𝑆 − 𝑈) ∈ ℂ)
106	104, 105, 88	divneg2d 12008	. . . . 5 ⊢ (𝜑 → -(((𝐹‘𝑆) − (𝐹‘𝑈)) / (𝑆 − 𝑈)) = (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈)))
107	103, 106	breqtrd 5173	. . . 4 ⊢ (𝜑 → 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈)))
108	85	renegcld 11645	. . . . 5 ⊢ (𝜑 → -(𝑆 − 𝑈) ∈ ℝ)
109	34, 6	posdifd 11805	. . . . . . 7 ⊢ (𝜑 → (𝑆 < 𝑈 ↔ 0 < (𝑈 − 𝑆)))
110	38, 109	mpbid 231	. . . . . 6 ⊢ (𝜑 → 0 < (𝑈 − 𝑆))
111	86, 87	negsubdi2d 11591	. . . . . 6 ⊢ (𝜑 → -(𝑆 − 𝑈) = (𝑈 − 𝑆))
112	110, 111	breqtrrd 5175	. . . . 5 ⊢ (𝜑 → 0 < -(𝑆 − 𝑈))
113		gt0div 12084	. . . . 5 ⊢ ((((𝐹‘𝑆) − (𝐹‘𝑈)) ∈ ℝ ∧ -(𝑆 − 𝑈) ∈ ℝ ∧ 0 < -(𝑆 − 𝑈)) → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈))))
114	84, 108, 112, 113	syl3anc 1369	. . . 4 ⊢ (𝜑 → (0 < ((𝐹‘𝑆) − (𝐹‘𝑈)) ↔ 0 < (((𝐹‘𝑆) − (𝐹‘𝑈)) / -(𝑆 − 𝑈))))
115	107, 114	mpbird 256	. . 3 ⊢ (𝜑 → 0 < ((𝐹‘𝑆) − (𝐹‘𝑈)))
116	83, 81	posdifd 11805	. . 3 ⊢ (𝜑 → ((𝐹‘𝑈) < (𝐹‘𝑆) ↔ 0 < ((𝐹‘𝑆) − (𝐹‘𝑈))))
117	115, 116	mpbird 256	. 2 ⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑆))
118		fveq2 6890	. . . . 5 ⊢ (𝑦 = 𝑆 → (𝐹‘𝑦) = (𝐹‘𝑆))
119	118	breq1d 5157	. . . 4 ⊢ (𝑦 = 𝑆 → ((𝐹‘𝑦) ≤ (𝐹‘𝑈) ↔ (𝐹‘𝑆) ≤ (𝐹‘𝑈)))
120		dvferm2.r	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝑈)(𝐹‘𝑦) ≤ (𝐹‘𝑈))
121	119, 120, 74	rspcdva 3612	. . 3 ⊢ (𝜑 → (𝐹‘𝑆) ≤ (𝐹‘𝑈))
122	81, 83, 121	lensymd 11369	. 2 ⊢ (𝜑 → ¬ (𝐹‘𝑈) < (𝐹‘𝑆))
123	117, 122	pm2.65i 193	1 ⊢ ¬ 𝜑

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 ∀wral 3059 ∖ cdif 3944 ⊆ wss 3947 ∅c0 4321 ifcif 4527 {csn 4627 class class class wbr 5147 dom cdm 5675 ⟶wf 6538 ‘cfv 6542 (class class class)co 7411 ℝcr 11111 0cc0 11112 + caddc 11115 -∞cmnf 11250 ℝ^*cxr 11251 < clt 11252 ≤ cle 11253 − cmin 11448 -cneg 11449 / cdiv 11875 2c2 12271 ℝ⁺crp 12978 (,)cioo 13328 abscabs 15185 D cdv 25612

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-map 8824 df-pm 8825 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fi 9408 df-sup 9439 df-inf 9440 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-z 12563 df-dec 12682 df-uz 12827 df-q 12937 df-rp 12979 df-xneg 13096 df-xadd 13097 df-xmul 13098 df-ioo 13332 df-icc 13335 df-fz 13489 df-seq 13971 df-exp 14032 df-cj 15050 df-re 15051 df-im 15052 df-sqrt 15186 df-abs 15187 df-struct 17084 df-slot 17119 df-ndx 17131 df-base 17149 df-plusg 17214 df-mulr 17215 df-starv 17216 df-tset 17220 df-ple 17221 df-ds 17223 df-unif 17224 df-rest 17372 df-topn 17373 df-topgen 17393 df-psmet 21136 df-xmet 21137 df-met 21138 df-bl 21139 df-mopn 21140 df-fbas 21141 df-fg 21142 df-cnfld 21145 df-top 22616 df-topon 22633 df-topsp 22655 df-bases 22669 df-cld 22743 df-ntr 22744 df-cls 22745 df-nei 22822 df-lp 22860 df-perf 22861 df-cn 22951 df-cnp 22952 df-haus 23039 df-fil 23570 df-fm 23662 df-flim 23663 df-flf 23664 df-xms 24046 df-ms 24047 df-cncf 24618 df-limc 25615 df-dv 25616

This theorem is referenced by: dvferm2 25739

W3C validator