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 34690

Description: Lemma for unbdqndv2 34691. (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 4465	. . . . . 6 ⊢ ((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑈)
4	3	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑈)
5	2, 4	eqtrd 2778	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = 𝑈)
6		unbdqndv2lem2.u	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ 𝑋)
7	6	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ 𝑋)
8		simplr 766	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
9		fveq2 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑈 = 𝐴 → (𝐹‘𝑈) = (𝐹‘𝐴))
10	9	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ (𝑈 = 𝐴 → (𝐹‘𝐴) = (𝐹‘𝑈))
11	10	oveq2d 7291	. . . . . . . . . . . . 13 ⊢ (𝑈 = 𝐴 → ((𝐹‘𝑈) − (𝐹‘𝐴)) = ((𝐹‘𝑈) − (𝐹‘𝑈)))
12	11	fveq2d 6778	. . . . . . . . . . . 12 ⊢ (𝑈 = 𝐴 → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))))
13	12	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))))
14		unbdqndv2lem2.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
15	14, 6	ffvelrnd 6962	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑈) ∈ ℂ)
16	15	subidd 11320	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝑈) − (𝐹‘𝑈)) = 0)
17	16	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ (𝜑 → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = (abs‘0))
18	17	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = (abs‘0))
19		abs0 14997	. . . . . . . . . . . . 13 ⊢ (abs‘0) = 0
20	19	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘0) = 0)
21	18, 20	eqtrd 2778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = 0)
22	13, 21	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = 0)
23	22	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = 0)
24	8, 23	breqtrd 5100	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (𝐵 · (𝑉 − 𝑈)) ≤ 0)
25		unbdqndv2lem2.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ⁺)
26	25	rpred 12772	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ)
27		unbdqndv2lem2.x	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ⊆ ℝ)
28		unbdqndv2lem2.v	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ∈ 𝑋)
29	27, 28	sseldd 3922	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑉 ∈ ℝ)
30	27, 6	sseldd 3922	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ ℝ)
31	29, 30	resubcld 11403	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉 − 𝑈) ∈ ℝ)
32	25	rpgt0d 12775	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝐵)
33		unbdqndv2lem2.a	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
34	27, 33	sseldd 3922	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ)
35		unbdqndv2lem2.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ≤ 𝐴)
36		unbdqndv2lem2.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ≤ 𝑉)
37	30, 34, 29, 35, 36	letrd 11132	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ≤ 𝑉)
38		unbdqndv2lem2.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
39	38	necomd 2999	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ≠ 𝑈)
40	30, 29, 37, 39	leneltd 11129	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 < 𝑉)
41	30, 29	posdifd 11562	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑈 < 𝑉 ↔ 0 < (𝑉 − 𝑈)))
42	40, 41	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (𝑉 − 𝑈))
43	26, 31, 32, 42	mulgt0d 11130	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 · (𝑉 − 𝑈)))
44		0red 10978	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℝ)
45	26, 31	remulcld 11005	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 · (𝑉 − 𝑈)) ∈ ℝ)
46	44, 45	ltnled 11122	. . . . . . . . . . 11 ⊢ (𝜑 → (0 < (𝐵 · (𝑉 − 𝑈)) ↔ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0))
47	43, 46	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0)
48	47	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0)
49	48	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0)
50	24, 49	pm2.65da 814	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ 𝑈 = 𝐴)
51	50	neqned 2950	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ≠ 𝐴)
52	7, 51	jca 512	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴))
53		eldifsn 4720	. . . . 5 ⊢ (𝑈 ∈ (𝑋 ∖ {𝐴}) ↔ (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴))
54	52, 53	sylibr 233	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ (𝑋 ∖ {𝐴}))
55	5, 54	eqeltrd 2839	. . 3 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 ∈ (𝑋 ∖ {𝐴}))
56	5	oveq1d 7290	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 − 𝐴) = (𝑈 − 𝐴))
57	56	fveq2d 6778	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (abs‘(𝑈 − 𝐴)))
58	30, 34, 35	abssuble0d 15144	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝑈 − 𝐴)) = (𝐴 − 𝑈))
59	58	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑈 − 𝐴)) = (𝐴 − 𝑈))
60	57, 59	eqtrd 2778	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (𝐴 − 𝑈))
61	34, 30	resubcld 11403	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑈) ∈ ℝ)
62		unbdqndv2lem2.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℝ⁺)
63	62	rpred 12772	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℝ)
64	34, 29, 30, 36	lesub1dd 11591	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑈) ≤ (𝑉 − 𝑈))
65		unbdqndv2lem2.4	. . . . . . 7 ⊢ (𝜑 → (𝑉 − 𝑈) < 𝐷)
66	61, 31, 63, 64, 65	lelttrd 11133	. . . . . 6 ⊢ (𝜑 → (𝐴 − 𝑈) < 𝐷)
67	66	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) < 𝐷)
68	60, 67	eqbrtrd 5096	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) < 𝐷)
69	26, 61	remulcld 11005	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (𝐴 − 𝑈)) ∈ ℝ)
70	69	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ∈ ℝ)
71	45	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝑉 − 𝑈)) ∈ ℝ)
72	14, 33	ffvelrnd 6962	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ)
73	15, 72	subcld 11332	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑈) − (𝐹‘𝐴)) ∈ ℂ)
74	73	abscld 15148	. . . . . . . 8 ⊢ (𝜑 → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ∈ ℝ)
75	74	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ∈ ℝ)
76	44, 26, 32	ltled 11123	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝐵)
77	61, 31, 26, 76, 64	lemul2ad 11915	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (𝐴 − 𝑈)) ≤ (𝐵 · (𝑉 − 𝑈)))
78	77	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ≤ (𝐵 · (𝑉 − 𝑈)))
79		simpr 485	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
80	70, 71, 75, 78, 79	letrd 11132	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
81	26	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ∈ ℝ)
82	61	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) ∈ ℝ)
83	35	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ≤ 𝐴)
84	51	necomd 2999	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ≠ 𝑈)
85	83, 84	jca 512	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈))
86	30, 34	ltlend 11120	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈 < 𝐴 ↔ (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈)))
87	86	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 < 𝐴 ↔ (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈)))
88	85, 87	mpbird 256	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 < 𝐴)
89	30, 34	posdifd 11562	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 < 𝐴 ↔ 0 < (𝐴 − 𝑈)))
90	89	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 < 𝐴 ↔ 0 < (𝐴 − 𝑈)))
91	88, 90	mpbid 231	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 0 < (𝐴 − 𝑈))
92	82, 91	jca 512	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐴 − 𝑈) ∈ ℝ ∧ 0 < (𝐴 − 𝑈)))
93		elrp 12732	. . . . . . . 8 ⊢ ((𝐴 − 𝑈) ∈ ℝ⁺ ↔ ((𝐴 − 𝑈) ∈ ℝ ∧ 0 < (𝐴 − 𝑈)))
94	92, 93	sylibr 233	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) ∈ ℝ⁺)
95	81, 75, 94	lemuldivd 12821	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (𝐴 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ 𝐵 ≤ ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈))))
96	80, 95	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
97	5	fveq2d 6778	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (𝐺‘𝑈))
98		unbdqndv2lem2.g	. . . . . . . . . 10 ⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))
99		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑈 → (𝐹‘𝑧) = (𝐹‘𝑈))
100	99	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑈 → ((𝐹‘𝑧) − (𝐹‘𝐴)) = ((𝐹‘𝑈) − (𝐹‘𝐴)))
101		oveq1 7282	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑈 → (𝑧 − 𝐴) = (𝑈 − 𝐴))
102	100, 101	oveq12d 7293	. . . . . . . . . 10 ⊢ (𝑧 = 𝑈 → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)))
103		ovexd 7310	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)) ∈ V)
104	98, 102, 54, 103	fvmptd3 6898	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑈) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)))
105	97, 104	eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)))
106	105	fveq2d 6778	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))))
107	73	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐹‘𝑈) − (𝐹‘𝐴)) ∈ ℂ)
108	30	recnd 11003	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ ℂ)
109	34	recnd 11003	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
110	108, 109	subcld 11332	. . . . . . . . . 10 ⊢ (𝜑 → (𝑈 − 𝐴) ∈ ℂ)
111	110	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 − 𝐴) ∈ ℂ)
112	108	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ ℂ)
113	109	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ∈ ℂ)
114	112, 113, 51	subne0d 11341	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 − 𝐴) ≠ 0)
115	107, 111, 114	absdivd 15167	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (abs‘(𝑈 − 𝐴))))
116	59	oveq2d 7291	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (abs‘(𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
117	115, 116	eqtrd 2778	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
118	106, 117	eqtrd 2778	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
119	118	eqcomd 2744	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)) = (abs‘(𝐺‘𝑊)))
120	96, 119	breqtrd 5100	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ (abs‘(𝐺‘𝑊)))
121	68, 120	jca 512	. . 3 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))
122	55, 121	jca 512	. 2 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))
123	1	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉))
124		simpr 485	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
125	124	iffalsed 4470	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑉)
126	123, 125	eqtrd 2778	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = 𝑉)
127	28	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ 𝑋)
128	30, 29, 37	abssubge0d 15143	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝑉 − 𝑈)) = (𝑉 − 𝑈))
129	128	oveq2d 7291	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝑈))) = (𝐵 · (𝑉 − 𝑈)))
130	129	breq1d 5084	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
131	130	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
132	124, 131	mtbird 325	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
133	14, 28	ffvelrnd 6962	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝑉) ∈ ℂ)
134	31	recnd 11003	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉 − 𝑈) ∈ ℂ)
135	44, 42	gtned 11110	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉 − 𝑈) ≠ 0)
136		unbdqndv2lem2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 𝐵) ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))
137	133, 15	subcld 11332	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐹‘𝑉) − (𝐹‘𝑈)) ∈ ℂ)
138	137, 134, 135	absdivd 15167	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (abs‘(𝑉 − 𝑈))))
139	128	oveq2d 7291	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (abs‘(𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))
140	138, 139	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))
141	140	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)) = (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))))
142	136, 141	breqtrd 5100	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 𝐵) ≤ (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))))
143	133, 15, 72, 134, 25, 135, 142	unbdqndv2lem1 34689	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
144	143	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
145		orel2 888	. . . . . . . . . . 11 ⊢ (¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) → (((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴)))))
146	132, 144, 145	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))))
147	146	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))))
148		fveq2 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑉 = 𝐴 → (𝐹‘𝑉) = (𝐹‘𝐴))
149	148	oveq1d 7290	. . . . . . . . . . . . . 14 ⊢ (𝑉 = 𝐴 → ((𝐹‘𝑉) − (𝐹‘𝐴)) = ((𝐹‘𝐴) − (𝐹‘𝐴)))
150	149	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝑉) − (𝐹‘𝐴)) = ((𝐹‘𝐴) − (𝐹‘𝐴)))
151	72	subidd 11320	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝐴) − (𝐹‘𝐴)) = 0)
152	151	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝐴) − (𝐹‘𝐴)) = 0)
153	150, 152	eqtrd 2778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝑉) − (𝐹‘𝐴)) = 0)
154	153	fveq2d 6778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = (abs‘0))
155	19	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘0) = 0)
156	154, 155	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = 0)
157	156	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = 0)
158	147, 157	breqtrd 5100	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
159	129	breq1d 5084	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0 ↔ (𝐵 · (𝑉 − 𝑈)) ≤ 0))
160	47, 159	mtbird 325	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
161	160	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
162	161	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
163	158, 162	pm2.65da 814	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ 𝑉 = 𝐴)
164	163	neqned 2950	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ≠ 𝐴)
165	127, 164	jca 512	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴))
166		eldifsn 4720	. . . . 5 ⊢ (𝑉 ∈ (𝑋 ∖ {𝐴}) ↔ (𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴))
167	165, 166	sylibr 233	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ (𝑋 ∖ {𝐴}))
168	126, 167	eqeltrd 2839	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 ∈ (𝑋 ∖ {𝐴}))
169	126	oveq1d 7290	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 − 𝐴) = (𝑉 − 𝐴))
170	169	fveq2d 6778	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (abs‘(𝑉 − 𝐴)))
171	34, 29, 36	abssubge0d 15143	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) = (𝑉 − 𝐴))
172	171	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑉 − 𝐴)) = (𝑉 − 𝐴))
173	170, 172	eqtrd 2778	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (𝑉 − 𝐴))
174	29, 34	resubcld 11403	. . . . . . 7 ⊢ (𝜑 → (𝑉 − 𝐴) ∈ ℝ)
175	30, 34, 29, 35	lesub2dd 11592	. . . . . . 7 ⊢ (𝜑 → (𝑉 − 𝐴) ≤ (𝑉 − 𝑈))
176	174, 31, 63, 175, 65	lelttrd 11133	. . . . . 6 ⊢ (𝜑 → (𝑉 − 𝐴) < 𝐷)
177	176	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) < 𝐷)
178	173, 177	eqbrtrd 5096	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) < 𝐷)
179	171, 174	eqeltrd 2839	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) ∈ ℝ)
180	26, 179	remulcld 11005	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝐴))) ∈ ℝ)
181	180	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ∈ ℝ)
182	129, 45	eqeltrd 2839	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝑈))) ∈ ℝ)
183	182	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ∈ ℝ)
184	133, 72	subcld 11332	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑉) − (𝐹‘𝐴)) ∈ ℂ)
185	184	abscld 15148	. . . . . . . 8 ⊢ (𝜑 → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∈ ℝ)
186	185	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∈ ℝ)
187	128, 31	eqeltrd 2839	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(𝑉 − 𝑈)) ∈ ℝ)
188	175, 171, 128	3brtr4d 5106	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) ≤ (abs‘(𝑉 − 𝑈)))
189	179, 187, 26, 76, 188	lemul2ad 11915	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (𝐵 · (abs‘(𝑉 − 𝑈))))
190	189	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (𝐵 · (abs‘(𝑉 − 𝑈))))
191	181, 183, 186, 190, 146	letrd 11132	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))))
192	26	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ∈ ℝ)
193	174	recnd 11003	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 − 𝐴) ∈ ℂ)
194	193	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) ∈ ℂ)
195	29	recnd 11003	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℂ)
196	195	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ ℂ)
197	109	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ∈ ℂ)
198	196, 197, 164	subne0d 11341	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) ≠ 0)
199	194, 198	absrpcld 15160	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑉 − 𝐴)) ∈ ℝ⁺)
200	192, 186, 199	lemuldivd 12821	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ↔ 𝐵 ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴)))))
201	191, 200	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))))
202	126	fveq2d 6778	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (𝐺‘𝑉))
203		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑉 → (𝐹‘𝑧) = (𝐹‘𝑉))
204	203	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑉 → ((𝐹‘𝑧) − (𝐹‘𝐴)) = ((𝐹‘𝑉) − (𝐹‘𝐴)))
205		oveq1 7282	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑉 → (𝑧 − 𝐴) = (𝑉 − 𝐴))
206	204, 205	oveq12d 7293	. . . . . . . . . 10 ⊢ (𝑧 = 𝑉 → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)))
207		ovexd 7310	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)) ∈ V)
208	98, 206, 167, 207	fvmptd3 6898	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑉) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)))
209	202, 208	eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)))
210	209	fveq2d 6778	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = (abs‘(((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))))
211	184	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐹‘𝑉) − (𝐹‘𝐴)) ∈ ℂ)
212	211, 194, 198	absdivd 15167	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))))
213	210, 212	eqtrd 2778	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))))
214	213	eqcomd 2744	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))) = (abs‘(𝐺‘𝑊)))
215	201, 214	breqtrd 5100	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ (abs‘(𝐺‘𝑊)))
216	178, 215	jca 512	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))
217	168, 216	jca 512	. 2 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))
218	122, 217	pm2.61dan 810	1 ⊢ (𝜑 → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 Vcvv 3432 ∖ cdif 3884 ⊆ wss 3887 ifcif 4459 {csn 4561 class class class wbr 5074 ↦ cmpt 5157 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 ℂcc 10869 ℝcr 10870 0cc0 10871 · cmul 10876 < clt 11009 ≤ cle 11010 − cmin 11205 / cdiv 11632 2c2 12028 ℝ⁺crp 12730 abscabs 14945

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-sup 9201 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-z 12320 df-uz 12583 df-rp 12731 df-seq 13722 df-exp 13783 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947

This theorem is referenced by: unbdqndv2 34691

W3C validator