unbdqndv2lem2 - Mathbox for Asger C. Ipsen

	Mathbox for Asger C. Ipsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > unbdqndv2lem2		Structured version Visualization version GIF version

Theorem unbdqndv2lem2 37140

Description: Lemma for unbdqndv2 37141. (Contributed by Asger C. Ipsen, 12-May-2021.)

**Hypotheses**
Ref	Expression
unbdqndv2lem2.g	⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))
unbdqndv2lem2.w	⊢ 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉)
unbdqndv2lem2.x	⊢ (𝜑 → 𝑋 ⊆ ℝ)
unbdqndv2lem2.f	⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
unbdqndv2lem2.a	⊢ (𝜑 → 𝐴 ∈ 𝑋)
unbdqndv2lem2.b	⊢ (𝜑 → 𝐵 ∈ ℝ⁺)
unbdqndv2lem2.d	⊢ (𝜑 → 𝐷 ∈ ℝ⁺)
unbdqndv2lem2.u	⊢ (𝜑 → 𝑈 ∈ 𝑋)
unbdqndv2lem2.v	⊢ (𝜑 → 𝑉 ∈ 𝑋)
unbdqndv2lem2.1	⊢ (𝜑 → 𝑈 ≠ 𝑉)
unbdqndv2lem2.2	⊢ (𝜑 → 𝑈 ≤ 𝐴)
unbdqndv2lem2.3	⊢ (𝜑 → 𝐴 ≤ 𝑉)
unbdqndv2lem2.4	⊢ (𝜑 → (𝑉 − 𝑈) < 𝐷)
unbdqndv2lem2.5	⊢ (𝜑 → (2 · 𝐵) ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))

**Assertion**
Ref	Expression
unbdqndv2lem2	⊢ (𝜑 → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))

Distinct variable groups: 𝑧,𝐴 𝑧,𝐵 𝑧,𝐹 𝑧,𝑈 𝑧,𝑉 𝑧,𝑋 𝜑,𝑧 Allowed substitution hints: 𝐷(𝑧) 𝐺(𝑧) 𝑊(𝑧)

**Proof of Theorem unbdqndv2lem2**
Step	Hyp	Ref	Expression
1		unbdqndv2lem2.w	. . . . . 6 ⊢ 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉)
2	1	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉))
3		iftrue 4498	. . . . . 6 ⊢ ((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑈)
4	3	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑈)
5	2, 4	eqtrd 2801	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = 𝑈)
6		unbdqndv2lem2.u	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ 𝑋)
7	6	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ 𝑋)
8		simplr 781	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
9		fveq2 6888	. . . . . . . . . . . . . . 15 ⊢ (𝑈 = 𝐴 → (𝐹‘𝑈) = (𝐹‘𝐴))
10	9	eqcomd 2772	. . . . . . . . . . . . . 14 ⊢ (𝑈 = 𝐴 → (𝐹‘𝐴) = (𝐹‘𝑈))
11	10	oveq2d 7439	. . . . . . . . . . . . 13 ⊢ (𝑈 = 𝐴 → ((𝐹‘𝑈) − (𝐹‘𝐴)) = ((𝐹‘𝑈) − (𝐹‘𝑈)))
12	11	fveq2d 6892	. . . . . . . . . . . 12 ⊢ (𝑈 = 𝐴 → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))))
13	12	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))))
14		unbdqndv2lem2.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
15	14, 6	ffvelcdmd 7087	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑈) ∈ ℂ)
16	15	subidd 11575	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝑈) − (𝐹‘𝑈)) = 0)
17	16	fveq2d 6892	. . . . . . . . . . . . 13 ⊢ (𝜑 → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = (abs‘0))
18	17	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = (abs‘0))
19		abs0 15362	. . . . . . . . . . . . 13 ⊢ (abs‘0) = 0
20	19	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘0) = 0)
21	18, 20	eqtrd 2801	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = 0)
22	13, 21	eqtrd 2801	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = 0)
23	22	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = 0)
24	8, 23	breqtrd 5142	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (𝐵 · (𝑉 − 𝑈)) ≤ 0)
25		unbdqndv2lem2.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ⁺)
26	25	rpred 13078	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ)
27		unbdqndv2lem2.x	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ⊆ ℝ)
28		unbdqndv2lem2.v	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ∈ 𝑋)
29	27, 28	sseldd 3941	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑉 ∈ ℝ)
30	27, 6	sseldd 3941	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ ℝ)
31	29, 30	resubcld 11660	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉 − 𝑈) ∈ ℝ)
32	25	rpgt0d 13081	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝐵)
33		unbdqndv2lem2.a	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
34	27, 33	sseldd 3941	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ)
35		unbdqndv2lem2.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ≤ 𝐴)
36		unbdqndv2lem2.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ≤ 𝑉)
37	30, 34, 29, 35, 36	letrd 11385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ≤ 𝑉)
38		unbdqndv2lem2.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
39	38	necomd 3016	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ≠ 𝑈)
40	30, 29, 37, 39	leneltd 11382	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 < 𝑉)
41	30, 29	posdifd 11819	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑈 < 𝑉 ↔ 0 < (𝑉 − 𝑈)))
42	40, 41	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (𝑉 − 𝑈))
43	26, 31, 32, 42	mulgt0d 11383	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 · (𝑉 − 𝑈)))
44		0red 11229	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℝ)
45	26, 31	remulcld 11257	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 · (𝑉 − 𝑈)) ∈ ℝ)
46	44, 45	ltnled 11375	. . . . . . . . . . 11 ⊢ (𝜑 → (0 < (𝐵 · (𝑉 − 𝑈)) ↔ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0))
47	43, 46	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0)
48	47	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0)
49	48	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0)
50	24, 49	pm2.65da 829	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ 𝑈 = 𝐴)
51	50	neqned 2968	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ≠ 𝐴)
52	7, 51	jca 521	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴))
53		eldifsn 4758	. . . . 5 ⊢ (𝑈 ∈ (𝑋 ∖ {𝐴}) ↔ (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴))
54	52, 53	sylibr 237	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ (𝑋 ∖ {𝐴}))
55	5, 54	eqeltrd 2866	. . 3 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 ∈ (𝑋 ∖ {𝐴}))
56	5	oveq1d 7438	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 − 𝐴) = (𝑈 − 𝐴))
57	56	fveq2d 6892	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (abs‘(𝑈 − 𝐴)))
58	30, 34, 35	abssuble0d 15512	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝑈 − 𝐴)) = (𝐴 − 𝑈))
59	58	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑈 − 𝐴)) = (𝐴 − 𝑈))
60	57, 59	eqtrd 2801	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (𝐴 − 𝑈))
61	34, 30	resubcld 11660	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑈) ∈ ℝ)
62		unbdqndv2lem2.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℝ⁺)
63	62	rpred 13078	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℝ)
64	34, 29, 30, 36	lesub1dd 11848	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑈) ≤ (𝑉 − 𝑈))
65		unbdqndv2lem2.4	. . . . . . 7 ⊢ (𝜑 → (𝑉 − 𝑈) < 𝐷)
66	61, 31, 63, 64, 65	lelttrd 11386	. . . . . 6 ⊢ (𝜑 → (𝐴 − 𝑈) < 𝐷)
67	66	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) < 𝐷)
68	60, 67	eqbrtrd 5138	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) < 𝐷)
69	26, 61	remulcld 11257	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (𝐴 − 𝑈)) ∈ ℝ)
70	69	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ∈ ℝ)
71	45	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝑉 − 𝑈)) ∈ ℝ)
72	14, 33	ffvelcdmd 7087	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ)
73	15, 72	subcld 11587	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑈) − (𝐹‘𝐴)) ∈ ℂ)
74	73	abscld 15516	. . . . . . . 8 ⊢ (𝜑 → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ∈ ℝ)
75	74	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ∈ ℝ)
76	44, 26, 32	ltled 11376	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝐵)
77	61, 31, 26, 76, 64	lemul2ad 12173	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (𝐴 − 𝑈)) ≤ (𝐵 · (𝑉 − 𝑈)))
78	77	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ≤ (𝐵 · (𝑉 − 𝑈)))
79		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
80	70, 71, 75, 78, 79	letrd 11385	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
81	26	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ∈ ℝ)
82	61	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) ∈ ℝ)
83	35	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ≤ 𝐴)
84	51	necomd 3016	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ≠ 𝑈)
85	83, 84	jca 521	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈))
86	30, 34	ltlend 11373	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈 < 𝐴 ↔ (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈)))
87	86	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 < 𝐴 ↔ (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈)))
88	85, 87	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 < 𝐴)
89	30, 34	posdifd 11819	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 < 𝐴 ↔ 0 < (𝐴 − 𝑈)))
90	89	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 < 𝐴 ↔ 0 < (𝐴 − 𝑈)))
91	88, 90	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 0 < (𝐴 − 𝑈))
92	82, 91	jca 521	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐴 − 𝑈) ∈ ℝ ∧ 0 < (𝐴 − 𝑈)))
93		elrp 13036	. . . . . . . 8 ⊢ ((𝐴 − 𝑈) ∈ ℝ⁺ ↔ ((𝐴 − 𝑈) ∈ ℝ ∧ 0 < (𝐴 − 𝑈)))
94	92, 93	sylibr 237	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) ∈ ℝ⁺)
95	81, 75, 94	lemuldivd 13127	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (𝐴 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ 𝐵 ≤ ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈))))
96	80, 95	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
97	5	fveq2d 6892	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (𝐺‘𝑈))
98		unbdqndv2lem2.g	. . . . . . . . . 10 ⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))
99		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑈 → (𝐹‘𝑧) = (𝐹‘𝑈))
100	99	oveq1d 7438	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑈 → ((𝐹‘𝑧) − (𝐹‘𝐴)) = ((𝐹‘𝑈) − (𝐹‘𝐴)))
101		oveq1 7430	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑈 → (𝑧 − 𝐴) = (𝑈 − 𝐴))
102	100, 101	oveq12d 7441	. . . . . . . . . 10 ⊢ (𝑧 = 𝑈 → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)))
103		ovexd 7458	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)) ∈ V)
104	98, 102, 54, 103	fvmptd3 7020	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑈) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)))
105	97, 104	eqtrd 2801	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)))
106	105	fveq2d 6892	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))))
107	73	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐹‘𝑈) − (𝐹‘𝐴)) ∈ ℂ)
108	30	recnd 11255	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ ℂ)
109	34	recnd 11255	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
110	108, 109	subcld 11587	. . . . . . . . . 10 ⊢ (𝜑 → (𝑈 − 𝐴) ∈ ℂ)
111	110	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 − 𝐴) ∈ ℂ)
112	108	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ ℂ)
113	109	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ∈ ℂ)
114	112, 113, 51	subne0d 11596	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 − 𝐴) ≠ 0)
115	107, 111, 114	absdivd 15535	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (abs‘(𝑈 − 𝐴))))
116	59	oveq2d 7439	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (abs‘(𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
117	115, 116	eqtrd 2801	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
118	106, 117	eqtrd 2801	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
119	118	eqcomd 2772	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)) = (abs‘(𝐺‘𝑊)))
120	96, 119	breqtrd 5142	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ (abs‘(𝐺‘𝑊)))
121	68, 120	jca 521	. . 3 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))
122	55, 121	jca 521	. 2 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))
123	1	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉))
124		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
125	124	iffalsed 4503	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑉)
126	123, 125	eqtrd 2801	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = 𝑉)
127	28	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ 𝑋)
128	30, 29, 37	abssubge0d 15511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝑉 − 𝑈)) = (𝑉 − 𝑈))
129	128	oveq2d 7439	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝑈))) = (𝐵 · (𝑉 − 𝑈)))
130	129	breq1d 5124	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
131	130	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
132	124, 131	mtbird 328	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
133	14, 28	ffvelcdmd 7087	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝑉) ∈ ℂ)
134	31	recnd 11255	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉 − 𝑈) ∈ ℂ)
135	44, 42	gtned 11363	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉 − 𝑈) ≠ 0)
136		unbdqndv2lem2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 𝐵) ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))
137	133, 15	subcld 11587	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐹‘𝑉) − (𝐹‘𝑈)) ∈ ℂ)
138	137, 134, 135	absdivd 15535	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (abs‘(𝑉 − 𝑈))))
139	128	oveq2d 7439	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (abs‘(𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))
140	138, 139	eqtrd 2801	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))
141	140	eqcomd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)) = (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))))
142	136, 141	breqtrd 5142	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 𝐵) ≤ (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))))
143	133, 15, 72, 134, 25, 135, 142	unbdqndv2lem1 37139	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
144	143	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
145		orel2 904	. . . . . . . . . . 11 ⊢ (¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) → (((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴)))))
146	132, 144, 145	sylc 66	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))))
147	146	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))))
148		fveq2 6888	. . . . . . . . . . . . . . 15 ⊢ (𝑉 = 𝐴 → (𝐹‘𝑉) = (𝐹‘𝐴))
149	148	oveq1d 7438	. . . . . . . . . . . . . 14 ⊢ (𝑉 = 𝐴 → ((𝐹‘𝑉) − (𝐹‘𝐴)) = ((𝐹‘𝐴) − (𝐹‘𝐴)))
150	149	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝑉) − (𝐹‘𝐴)) = ((𝐹‘𝐴) − (𝐹‘𝐴)))
151	72	subidd 11575	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝐴) − (𝐹‘𝐴)) = 0)
152	151	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝐴) − (𝐹‘𝐴)) = 0)
153	150, 152	eqtrd 2801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝑉) − (𝐹‘𝐴)) = 0)
154	153	fveq2d 6892	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = (abs‘0))
155	19	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘0) = 0)
156	154, 155	eqtrd 2801	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = 0)
157	156	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = 0)
158	147, 157	breqtrd 5142	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
159	129	breq1d 5124	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0 ↔ (𝐵 · (𝑉 − 𝑈)) ≤ 0))
160	47, 159	mtbird 328	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
161	160	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
162	161	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
163	158, 162	pm2.65da 829	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ 𝑉 = 𝐴)
164	163	neqned 2968	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ≠ 𝐴)
165	127, 164	jca 521	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴))
166		eldifsn 4758	. . . . 5 ⊢ (𝑉 ∈ (𝑋 ∖ {𝐴}) ↔ (𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴))
167	165, 166	sylibr 237	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ (𝑋 ∖ {𝐴}))
168	126, 167	eqeltrd 2866	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 ∈ (𝑋 ∖ {𝐴}))
169	126	oveq1d 7438	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 − 𝐴) = (𝑉 − 𝐴))
170	169	fveq2d 6892	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (abs‘(𝑉 − 𝐴)))
171	34, 29, 36	abssubge0d 15511	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) = (𝑉 − 𝐴))
172	171	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑉 − 𝐴)) = (𝑉 − 𝐴))
173	170, 172	eqtrd 2801	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (𝑉 − 𝐴))
174	29, 34	resubcld 11660	. . . . . . 7 ⊢ (𝜑 → (𝑉 − 𝐴) ∈ ℝ)
175	30, 34, 29, 35	lesub2dd 11849	. . . . . . 7 ⊢ (𝜑 → (𝑉 − 𝐴) ≤ (𝑉 − 𝑈))
176	174, 31, 63, 175, 65	lelttrd 11386	. . . . . 6 ⊢ (𝜑 → (𝑉 − 𝐴) < 𝐷)
177	176	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) < 𝐷)
178	173, 177	eqbrtrd 5138	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) < 𝐷)
179	171, 174	eqeltrd 2866	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) ∈ ℝ)
180	26, 179	remulcld 11257	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝐴))) ∈ ℝ)
181	180	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ∈ ℝ)
182	129, 45	eqeltrd 2866	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝑈))) ∈ ℝ)
183	182	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ∈ ℝ)
184	133, 72	subcld 11587	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑉) − (𝐹‘𝐴)) ∈ ℂ)
185	184	abscld 15516	. . . . . . . 8 ⊢ (𝜑 → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∈ ℝ)
186	185	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∈ ℝ)
187	128, 31	eqeltrd 2866	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(𝑉 − 𝑈)) ∈ ℝ)
188	175, 171, 128	3brtr4d 5148	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) ≤ (abs‘(𝑉 − 𝑈)))
189	179, 187, 26, 76, 188	lemul2ad 12173	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (𝐵 · (abs‘(𝑉 − 𝑈))))
190	189	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (𝐵 · (abs‘(𝑉 − 𝑈))))
191	181, 183, 186, 190, 146	letrd 11385	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))))
192	26	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ∈ ℝ)
193	174	recnd 11255	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 − 𝐴) ∈ ℂ)
194	193	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) ∈ ℂ)
195	29	recnd 11255	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℂ)
196	195	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ ℂ)
197	109	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ∈ ℂ)
198	196, 197, 164	subne0d 11596	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) ≠ 0)
199	194, 198	absrpcld 15528	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑉 − 𝐴)) ∈ ℝ⁺)
200	192, 186, 199	lemuldivd 13127	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ↔ 𝐵 ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴)))))
201	191, 200	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))))
202	126	fveq2d 6892	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (𝐺‘𝑉))
203		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑉 → (𝐹‘𝑧) = (𝐹‘𝑉))
204	203	oveq1d 7438	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑉 → ((𝐹‘𝑧) − (𝐹‘𝐴)) = ((𝐹‘𝑉) − (𝐹‘𝐴)))
205		oveq1 7430	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑉 → (𝑧 − 𝐴) = (𝑉 − 𝐴))
206	204, 205	oveq12d 7441	. . . . . . . . . 10 ⊢ (𝑧 = 𝑉 → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)))
207		ovexd 7458	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)) ∈ V)
208	98, 206, 167, 207	fvmptd3 7020	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑉) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)))
209	202, 208	eqtrd 2801	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)))
210	209	fveq2d 6892	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = (abs‘(((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))))
211	184	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐹‘𝑉) − (𝐹‘𝐴)) ∈ ℂ)
212	211, 194, 198	absdivd 15535	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))))
213	210, 212	eqtrd 2801	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))))
214	213	eqcomd 2772	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))) = (abs‘(𝐺‘𝑊)))
215	201, 214	breqtrd 5142	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ (abs‘(𝐺‘𝑊)))
216	178, 215	jca 521	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))
217	168, 216	jca 521	. 2 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))
218	122, 217	pm2.61dan 825	1 ⊢ (𝜑 → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2146 ≠ wne 2961 Vcvv 3458 ∖ cdif 3905 ⊆ wss 3908 ifcif 4492 {csn 4594 class class class wbr 5114 ↦ cmpt 5197 ⟶wf 6539 ‘cfv 6543 (class class class)co 7423 ℂcc 11116 ℝcr 11117 0cc0 11118 · cmul 11123 < clt 11261 ≤ cle 11262 − cmin 11459 / cdiv 11889 2c2 12313 ℝ⁺crp 13034 abscabs 15311

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-sup 9412 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-n0 12523 df-z 12610 df-uz 12881 df-rp 13035 df-seq 14058 df-exp 14118 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313

This theorem is used by: unbdqndv2 37141

W3C validator