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 36912

Description: Lemma for unbdqndv2 36913. (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 4485	. . . . . 6 ⊢ ((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑈)
4	3	adantl 485	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑈)
5	2, 4	eqtrd 2796	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = 𝑈)
6		unbdqndv2lem2.u	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ 𝑋)
7	6	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ 𝑋)
8		simplr 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
9		fveq2 6863	. . . . . . . . . . . . . . 15 ⊢ (𝑈 = 𝐴 → (𝐹‘𝑈) = (𝐹‘𝐴))
10	9	eqcomd 2767	. . . . . . . . . . . . . 14 ⊢ (𝑈 = 𝐴 → (𝐹‘𝐴) = (𝐹‘𝑈))
11	10	oveq2d 7408	. . . . . . . . . . . . 13 ⊢ (𝑈 = 𝐴 → ((𝐹‘𝑈) − (𝐹‘𝐴)) = ((𝐹‘𝑈) − (𝐹‘𝑈)))
12	11	fveq2d 6867	. . . . . . . . . . . 12 ⊢ (𝑈 = 𝐴 → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))))
13	12	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))))
14		unbdqndv2lem2.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
15	14, 6	ffvelcdmd 7062	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑈) ∈ ℂ)
16	15	subidd 11527	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝑈) − (𝐹‘𝑈)) = 0)
17	16	fveq2d 6867	. . . . . . . . . . . . 13 ⊢ (𝜑 → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = (abs‘0))
18	17	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = (abs‘0))
19		abs0 15295	. . . . . . . . . . . . 13 ⊢ (abs‘0) = 0
20	19	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘0) = 0)
21	18, 20	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = 0)
22	13, 21	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = 0)
23	22	adantlr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = 0)
24	8, 23	breqtrd 5125	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (𝐵 · (𝑉 − 𝑈)) ≤ 0)
25		unbdqndv2lem2.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ⁺)
26	25	rpred 13034	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ)
27		unbdqndv2lem2.x	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ⊆ ℝ)
28		unbdqndv2lem2.v	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ∈ 𝑋)
29	27, 28	sseldd 3937	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑉 ∈ ℝ)
30	27, 6	sseldd 3937	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ ℝ)
31	29, 30	resubcld 11612	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉 − 𝑈) ∈ ℝ)
32	25	rpgt0d 13037	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝐵)
33		unbdqndv2lem2.a	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
34	27, 33	sseldd 3937	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ)
35		unbdqndv2lem2.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ≤ 𝐴)
36		unbdqndv2lem2.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ≤ 𝑉)
37	30, 34, 29, 35, 36	letrd 11337	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ≤ 𝑉)
38		unbdqndv2lem2.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
39	38	necomd 3011	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ≠ 𝑈)
40	30, 29, 37, 39	leneltd 11334	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 < 𝑉)
41	30, 29	posdifd 11771	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑈 < 𝑉 ↔ 0 < (𝑉 − 𝑈)))
42	40, 41	mpbid 234	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (𝑉 − 𝑈))
43	26, 31, 32, 42	mulgt0d 11335	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝐵 · (𝑉 − 𝑈)))
44		0red 11181	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℝ)
45	26, 31	remulcld 11209	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 · (𝑉 − 𝑈)) ∈ ℝ)
46	44, 45	ltnled 11327	. . . . . . . . . . 11 ⊢ (𝜑 → (0 < (𝐵 · (𝑉 − 𝑈)) ↔ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0))
47	43, 46	mpbid 234	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0)
48	47	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0)
49	48	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0)
50	24, 49	pm2.65da 826	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ 𝑈 = 𝐴)
51	50	neqned 2963	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ≠ 𝐴)
52	7, 51	jca 519	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴))
53		eldifsn 4745	. . . . 5 ⊢ (𝑈 ∈ (𝑋 ∖ {𝐴}) ↔ (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴))
54	52, 53	sylibr 236	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ (𝑋 ∖ {𝐴}))
55	5, 54	eqeltrd 2861	. . 3 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 ∈ (𝑋 ∖ {𝐴}))
56	5	oveq1d 7407	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 − 𝐴) = (𝑈 − 𝐴))
57	56	fveq2d 6867	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (abs‘(𝑈 − 𝐴)))
58	30, 34, 35	abssuble0d 15445	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝑈 − 𝐴)) = (𝐴 − 𝑈))
59	58	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑈 − 𝐴)) = (𝐴 − 𝑈))
60	57, 59	eqtrd 2796	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (𝐴 − 𝑈))
61	34, 30	resubcld 11612	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑈) ∈ ℝ)
62		unbdqndv2lem2.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℝ⁺)
63	62	rpred 13034	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℝ)
64	34, 29, 30, 36	lesub1dd 11800	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑈) ≤ (𝑉 − 𝑈))
65		unbdqndv2lem2.4	. . . . . . 7 ⊢ (𝜑 → (𝑉 − 𝑈) < 𝐷)
66	61, 31, 63, 64, 65	lelttrd 11338	. . . . . 6 ⊢ (𝜑 → (𝐴 − 𝑈) < 𝐷)
67	66	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) < 𝐷)
68	60, 67	eqbrtrd 5121	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) < 𝐷)
69	26, 61	remulcld 11209	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (𝐴 − 𝑈)) ∈ ℝ)
70	69	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ∈ ℝ)
71	45	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝑉 − 𝑈)) ∈ ℝ)
72	14, 33	ffvelcdmd 7062	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ)
73	15, 72	subcld 11539	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑈) − (𝐹‘𝐴)) ∈ ℂ)
74	73	abscld 15449	. . . . . . . 8 ⊢ (𝜑 → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ∈ ℝ)
75	74	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ∈ ℝ)
76	44, 26, 32	ltled 11328	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝐵)
77	61, 31, 26, 76, 64	lemul2ad 12129	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (𝐴 − 𝑈)) ≤ (𝐵 · (𝑉 − 𝑈)))
78	77	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ≤ (𝐵 · (𝑉 − 𝑈)))
79		simpr 488	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
80	70, 71, 75, 78, 79	letrd 11337	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
81	26	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ∈ ℝ)
82	61	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) ∈ ℝ)
83	35	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ≤ 𝐴)
84	51	necomd 3011	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ≠ 𝑈)
85	83, 84	jca 519	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈))
86	30, 34	ltlend 11325	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈 < 𝐴 ↔ (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈)))
87	86	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 < 𝐴 ↔ (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈)))
88	85, 87	mpbird 259	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 < 𝐴)
89	30, 34	posdifd 11771	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 < 𝐴 ↔ 0 < (𝐴 − 𝑈)))
90	89	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 < 𝐴 ↔ 0 < (𝐴 − 𝑈)))
91	88, 90	mpbid 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 0 < (𝐴 − 𝑈))
92	82, 91	jca 519	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐴 − 𝑈) ∈ ℝ ∧ 0 < (𝐴 − 𝑈)))
93		elrp 12992	. . . . . . . 8 ⊢ ((𝐴 − 𝑈) ∈ ℝ⁺ ↔ ((𝐴 − 𝑈) ∈ ℝ ∧ 0 < (𝐴 − 𝑈)))
94	92, 93	sylibr 236	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) ∈ ℝ⁺)
95	81, 75, 94	lemuldivd 13083	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (𝐴 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ 𝐵 ≤ ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈))))
96	80, 95	mpbid 234	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
97	5	fveq2d 6867	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (𝐺‘𝑈))
98		unbdqndv2lem2.g	. . . . . . . . . 10 ⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))
99		fveq2 6863	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑈 → (𝐹‘𝑧) = (𝐹‘𝑈))
100	99	oveq1d 7407	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑈 → ((𝐹‘𝑧) − (𝐹‘𝐴)) = ((𝐹‘𝑈) − (𝐹‘𝐴)))
101		oveq1 7399	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑈 → (𝑧 − 𝐴) = (𝑈 − 𝐴))
102	100, 101	oveq12d 7410	. . . . . . . . . 10 ⊢ (𝑧 = 𝑈 → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)))
103		ovexd 7427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)) ∈ V)
104	98, 102, 54, 103	fvmptd3 6995	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑈) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)))
105	97, 104	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)))
106	105	fveq2d 6867	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))))
107	73	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐹‘𝑈) − (𝐹‘𝐴)) ∈ ℂ)
108	30	recnd 11207	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ ℂ)
109	34	recnd 11207	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
110	108, 109	subcld 11539	. . . . . . . . . 10 ⊢ (𝜑 → (𝑈 − 𝐴) ∈ ℂ)
111	110	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 − 𝐴) ∈ ℂ)
112	108	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ ℂ)
113	109	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ∈ ℂ)
114	112, 113, 51	subne0d 11548	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 − 𝐴) ≠ 0)
115	107, 111, 114	absdivd 15468	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (abs‘(𝑈 − 𝐴))))
116	59	oveq2d 7408	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (abs‘(𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
117	115, 116	eqtrd 2796	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
118	106, 117	eqtrd 2796	. . . . . 6 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))
119	118	eqcomd 2767	. . . . 5 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)) = (abs‘(𝐺‘𝑊)))
120	96, 119	breqtrd 5125	. . . 4 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ (abs‘(𝐺‘𝑊)))
121	68, 120	jca 519	. . 3 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))
122	55, 121	jca 519	. 2 ⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))
123	1	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉))
124		simpr 488	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
125	124	iffalsed 4490	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑉)
126	123, 125	eqtrd 2796	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = 𝑉)
127	28	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ 𝑋)
128	30, 29, 37	abssubge0d 15444	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝑉 − 𝑈)) = (𝑉 − 𝑈))
129	128	oveq2d 7408	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝑈))) = (𝐵 · (𝑉 − 𝑈)))
130	129	breq1d 5109	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
131	130	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
132	124, 131	mtbird 327	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))
133	14, 28	ffvelcdmd 7062	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝑉) ∈ ℂ)
134	31	recnd 11207	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉 − 𝑈) ∈ ℂ)
135	44, 42	gtned 11315	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉 − 𝑈) ≠ 0)
136		unbdqndv2lem2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 𝐵) ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))
137	133, 15	subcld 11539	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐹‘𝑉) − (𝐹‘𝑈)) ∈ ℂ)
138	137, 134, 135	absdivd 15468	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (abs‘(𝑉 − 𝑈))))
139	128	oveq2d 7408	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (abs‘(𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))
140	138, 139	eqtrd 2796	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)))
141	140	eqcomd 2767	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)) = (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))))
142	136, 141	breqtrd 5125	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 𝐵) ≤ (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))))
143	133, 15, 72, 134, 25, 135, 142	unbdqndv2lem1 36911	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
144	143	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))))
145		orel2 901	. . . . . . . . . . 11 ⊢ (¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) → (((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴)))))
146	132, 144, 145	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))))
147	146	adantr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))))
148		fveq2 6863	. . . . . . . . . . . . . . 15 ⊢ (𝑉 = 𝐴 → (𝐹‘𝑉) = (𝐹‘𝐴))
149	148	oveq1d 7407	. . . . . . . . . . . . . 14 ⊢ (𝑉 = 𝐴 → ((𝐹‘𝑉) − (𝐹‘𝐴)) = ((𝐹‘𝐴) − (𝐹‘𝐴)))
150	149	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝑉) − (𝐹‘𝐴)) = ((𝐹‘𝐴) − (𝐹‘𝐴)))
151	72	subidd 11527	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝐴) − (𝐹‘𝐴)) = 0)
152	151	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝐴) − (𝐹‘𝐴)) = 0)
153	150, 152	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝑉) − (𝐹‘𝐴)) = 0)
154	153	fveq2d 6867	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = (abs‘0))
155	19	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘0) = 0)
156	154, 155	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = 0)
157	156	adantlr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = 0)
158	147, 157	breqtrd 5125	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
159	129	breq1d 5109	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0 ↔ (𝐵 · (𝑉 − 𝑈)) ≤ 0))
160	47, 159	mtbird 327	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
161	160	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
162	161	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0)
163	158, 162	pm2.65da 826	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ 𝑉 = 𝐴)
164	163	neqned 2963	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ≠ 𝐴)
165	127, 164	jca 519	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴))
166		eldifsn 4745	. . . . 5 ⊢ (𝑉 ∈ (𝑋 ∖ {𝐴}) ↔ (𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴))
167	165, 166	sylibr 236	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ (𝑋 ∖ {𝐴}))
168	126, 167	eqeltrd 2861	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 ∈ (𝑋 ∖ {𝐴}))
169	126	oveq1d 7407	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 − 𝐴) = (𝑉 − 𝐴))
170	169	fveq2d 6867	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (abs‘(𝑉 − 𝐴)))
171	34, 29, 36	abssubge0d 15444	. . . . . . 7 ⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) = (𝑉 − 𝐴))
172	171	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑉 − 𝐴)) = (𝑉 − 𝐴))
173	170, 172	eqtrd 2796	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (𝑉 − 𝐴))
174	29, 34	resubcld 11612	. . . . . . 7 ⊢ (𝜑 → (𝑉 − 𝐴) ∈ ℝ)
175	30, 34, 29, 35	lesub2dd 11801	. . . . . . 7 ⊢ (𝜑 → (𝑉 − 𝐴) ≤ (𝑉 − 𝑈))
176	174, 31, 63, 175, 65	lelttrd 11338	. . . . . 6 ⊢ (𝜑 → (𝑉 − 𝐴) < 𝐷)
177	176	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) < 𝐷)
178	173, 177	eqbrtrd 5121	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) < 𝐷)
179	171, 174	eqeltrd 2861	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) ∈ ℝ)
180	26, 179	remulcld 11209	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝐴))) ∈ ℝ)
181	180	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ∈ ℝ)
182	129, 45	eqeltrd 2861	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝑈))) ∈ ℝ)
183	182	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ∈ ℝ)
184	133, 72	subcld 11539	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑉) − (𝐹‘𝐴)) ∈ ℂ)
185	184	abscld 15449	. . . . . . . 8 ⊢ (𝜑 → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∈ ℝ)
186	185	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∈ ℝ)
187	128, 31	eqeltrd 2861	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(𝑉 − 𝑈)) ∈ ℝ)
188	175, 171, 128	3brtr4d 5131	. . . . . . . . 9 ⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) ≤ (abs‘(𝑉 − 𝑈)))
189	179, 187, 26, 76, 188	lemul2ad 12129	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (𝐵 · (abs‘(𝑉 − 𝑈))))
190	189	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (𝐵 · (abs‘(𝑉 − 𝑈))))
191	181, 183, 186, 190, 146	letrd 11337	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))))
192	26	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ∈ ℝ)
193	174	recnd 11207	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 − 𝐴) ∈ ℂ)
194	193	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) ∈ ℂ)
195	29	recnd 11207	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℂ)
196	195	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ ℂ)
197	109	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ∈ ℂ)
198	196, 197, 164	subne0d 11548	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) ≠ 0)
199	194, 198	absrpcld 15461	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑉 − 𝐴)) ∈ ℝ⁺)
200	192, 186, 199	lemuldivd 13083	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ↔ 𝐵 ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴)))))
201	191, 200	mpbid 234	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))))
202	126	fveq2d 6867	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (𝐺‘𝑉))
203		fveq2 6863	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑉 → (𝐹‘𝑧) = (𝐹‘𝑉))
204	203	oveq1d 7407	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑉 → ((𝐹‘𝑧) − (𝐹‘𝐴)) = ((𝐹‘𝑉) − (𝐹‘𝐴)))
205		oveq1 7399	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑉 → (𝑧 − 𝐴) = (𝑉 − 𝐴))
206	204, 205	oveq12d 7410	. . . . . . . . . 10 ⊢ (𝑧 = 𝑉 → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)))
207		ovexd 7427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)) ∈ V)
208	98, 206, 167, 207	fvmptd3 6995	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑉) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)))
209	202, 208	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)))
210	209	fveq2d 6867	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = (abs‘(((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))))
211	184	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐹‘𝑉) − (𝐹‘𝐴)) ∈ ℂ)
212	211, 194, 198	absdivd 15468	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))))
213	210, 212	eqtrd 2796	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))))
214	213	eqcomd 2767	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))) = (abs‘(𝐺‘𝑊)))
215	201, 214	breqtrd 5125	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ (abs‘(𝐺‘𝑊)))
216	178, 215	jca 519	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))
217	168, 216	jca 519	. 2 ⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))
218	122, 217	pm2.61dan 822	1 ⊢ (𝜑 → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 Vcvv 3453 ∖ cdif 3901 ⊆ wss 3904 ifcif 4479 {csn 4581 class class class wbr 5099 ↦ cmpt 5180 ⟶wf 6513 ‘cfv 6517 (class class class)co 7392 ℂcc 11068 ℝcr 11069 0cc0 11070 · cmul 11075 < clt 11213 ≤ cle 11214 − cmin 11411 / cdiv 11841 2c2 12269 ℝ⁺crp 12990 abscabs 15244

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147 ax-pre-sup 11148

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-iun 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-om 7843 df-2nd 7967 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-er 8673 df-en 8924 df-dom 8925 df-sdom 8926 df-sup 9385 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-div 11842 df-nn 12208 df-2 12277 df-3 12278 df-n0 12479 df-z 12566 df-uz 12837 df-rp 12991 df-seq 14012 df-exp 14072 df-cj 15109 df-re 15110 df-im 15111 df-sqrt 15245 df-abs 15246

This theorem is referenced by: unbdqndv2 36913

W3C validator