Proof of Theorem unbdqndv2lem2
Step | Hyp | Ref
| Expression |
1 | | unbdqndv2lem2.w |
. . . . . 6
⊢ 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) |
2 | 1 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉)) |
3 | | iftrue 4234 |
. . . . . 6
⊢ ((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑈) |
4 | 3 | adantl 473 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑈) |
5 | 2, 4 | eqtrd 2792 |
. . . 4
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = 𝑈) |
6 | | unbdqndv2lem2.u |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ 𝑋) |
7 | 6 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ 𝑋) |
8 | | simplr 809 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) |
9 | | fveq2 6350 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 = 𝐴 → (𝐹‘𝑈) = (𝐹‘𝐴)) |
10 | 9 | eqcomd 2764 |
. . . . . . . . . . . . . 14
⊢ (𝑈 = 𝐴 → (𝐹‘𝐴) = (𝐹‘𝑈)) |
11 | 10 | oveq2d 6827 |
. . . . . . . . . . . . 13
⊢ (𝑈 = 𝐴 → ((𝐹‘𝑈) − (𝐹‘𝐴)) = ((𝐹‘𝑈) − (𝐹‘𝑈))) |
12 | 11 | fveq2d 6354 |
. . . . . . . . . . . 12
⊢ (𝑈 = 𝐴 → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = (abs‘((𝐹‘𝑈) − (𝐹‘𝑈)))) |
13 | 12 | adantl 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = (abs‘((𝐹‘𝑈) − (𝐹‘𝑈)))) |
14 | | unbdqndv2lem2.f |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
15 | 14, 6 | ffvelrnd 6521 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘𝑈) ∈ ℂ) |
16 | 15 | subidd 10570 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐹‘𝑈) − (𝐹‘𝑈)) = 0) |
17 | 16 | fveq2d 6354 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = (abs‘0)) |
18 | 17 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = (abs‘0)) |
19 | | abs0 14222 |
. . . . . . . . . . . . 13
⊢
(abs‘0) = 0 |
20 | 19 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘0) = 0) |
21 | 18, 20 | eqtrd 2792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = 0) |
22 | 13, 21 | eqtrd 2792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = 0) |
23 | 22 | adantlr 753 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = 0) |
24 | 8, 23 | breqtrd 4828 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (𝐵 · (𝑉 − 𝑈)) ≤ 0) |
25 | | unbdqndv2lem2.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
26 | 25 | rpred 12063 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℝ) |
27 | | unbdqndv2lem2.x |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
28 | | unbdqndv2lem2.v |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑉 ∈ 𝑋) |
29 | 27, 28 | sseldd 3743 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑉 ∈ ℝ) |
30 | 27, 6 | sseldd 3743 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ ℝ) |
31 | 29, 30 | resubcld 10648 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑉 − 𝑈) ∈ ℝ) |
32 | 25 | rpgt0d 12066 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐵) |
33 | | unbdqndv2lem2.a |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
34 | 27, 33 | sseldd 3743 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
35 | | unbdqndv2lem2.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ≤ 𝐴) |
36 | | unbdqndv2lem2.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ≤ 𝑉) |
37 | 30, 34, 29, 35, 36 | letrd 10384 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ≤ 𝑉) |
38 | | unbdqndv2lem2.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ≠ 𝑉) |
39 | 38 | necomd 2985 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑉 ≠ 𝑈) |
40 | 30, 29, 37, 39 | leneltd 10381 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 < 𝑉) |
41 | 30, 29 | posdifd 10804 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 < 𝑉 ↔ 0 < (𝑉 − 𝑈))) |
42 | 40, 41 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝑉 − 𝑈)) |
43 | 26, 31, 32, 42 | mulgt0d 10382 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (𝐵 · (𝑉 − 𝑈))) |
44 | | 0red 10231 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℝ) |
45 | 26, 31 | remulcld 10260 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 · (𝑉 − 𝑈)) ∈ ℝ) |
46 | 44, 45 | ltnled 10374 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 < (𝐵 · (𝑉 − 𝑈)) ↔ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0)) |
47 | 43, 46 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0) |
48 | 47 | adantr 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0) |
49 | 48 | adantr 472 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0) |
50 | 24, 49 | pm2.65da 601 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ 𝑈 = 𝐴) |
51 | 50 | neqned 2937 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ≠ 𝐴) |
52 | 7, 51 | jca 555 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴)) |
53 | | eldifsn 4460 |
. . . . 5
⊢ (𝑈 ∈ (𝑋 ∖ {𝐴}) ↔ (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴)) |
54 | 52, 53 | sylibr 224 |
. . . 4
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ (𝑋 ∖ {𝐴})) |
55 | 5, 54 | eqeltrd 2837 |
. . 3
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 ∈ (𝑋 ∖ {𝐴})) |
56 | 5 | oveq1d 6826 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 − 𝐴) = (𝑈 − 𝐴)) |
57 | 56 | fveq2d 6354 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (abs‘(𝑈 − 𝐴))) |
58 | 30, 34, 35 | abssuble0d 14368 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝑈 − 𝐴)) = (𝐴 − 𝑈)) |
59 | 58 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑈 − 𝐴)) = (𝐴 − 𝑈)) |
60 | 57, 59 | eqtrd 2792 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (𝐴 − 𝑈)) |
61 | 34, 30 | resubcld 10648 |
. . . . . . 7
⊢ (𝜑 → (𝐴 − 𝑈) ∈ ℝ) |
62 | | unbdqndv2lem2.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈
ℝ+) |
63 | 62 | rpred 12063 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℝ) |
64 | 34, 29, 30, 36 | lesub1dd 10833 |
. . . . . . 7
⊢ (𝜑 → (𝐴 − 𝑈) ≤ (𝑉 − 𝑈)) |
65 | | unbdqndv2lem2.4 |
. . . . . . 7
⊢ (𝜑 → (𝑉 − 𝑈) < 𝐷) |
66 | 61, 31, 63, 64, 65 | lelttrd 10385 |
. . . . . 6
⊢ (𝜑 → (𝐴 − 𝑈) < 𝐷) |
67 | 66 | adantr 472 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) < 𝐷) |
68 | 60, 67 | eqbrtrd 4824 |
. . . 4
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) < 𝐷) |
69 | 26, 61 | remulcld 10260 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (𝐴 − 𝑈)) ∈ ℝ) |
70 | 69 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ∈ ℝ) |
71 | 45 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝑉 − 𝑈)) ∈ ℝ) |
72 | 14, 33 | ffvelrnd 6521 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ) |
73 | 15, 72 | subcld 10582 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑈) − (𝐹‘𝐴)) ∈ ℂ) |
74 | 73 | abscld 14372 |
. . . . . . . 8
⊢ (𝜑 → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ∈ ℝ) |
75 | 74 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ∈ ℝ) |
76 | 44, 26, 32 | ltled 10375 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐵) |
77 | 61, 31, 26, 76, 64 | lemul2ad 11154 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (𝐴 − 𝑈)) ≤ (𝐵 · (𝑉 − 𝑈))) |
78 | 77 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ≤ (𝐵 · (𝑉 − 𝑈))) |
79 | | simpr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) |
80 | 70, 71, 75, 78, 79 | letrd 10384 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) |
81 | 26 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ∈ ℝ) |
82 | 61 | adantr 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) ∈ ℝ) |
83 | 35 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ≤ 𝐴) |
84 | 51 | necomd 2985 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ≠ 𝑈) |
85 | 83, 84 | jca 555 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈)) |
86 | 30, 34 | ltlend 10372 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 < 𝐴 ↔ (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈))) |
87 | 86 | adantr 472 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 < 𝐴 ↔ (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈))) |
88 | 85, 87 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 < 𝐴) |
89 | 30, 34 | posdifd 10804 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈 < 𝐴 ↔ 0 < (𝐴 − 𝑈))) |
90 | 89 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 < 𝐴 ↔ 0 < (𝐴 − 𝑈))) |
91 | 88, 90 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 0 < (𝐴 − 𝑈)) |
92 | 82, 91 | jca 555 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐴 − 𝑈) ∈ ℝ ∧ 0 < (𝐴 − 𝑈))) |
93 | | elrp 12025 |
. . . . . . . 8
⊢ ((𝐴 − 𝑈) ∈ ℝ+ ↔ ((𝐴 − 𝑈) ∈ ℝ ∧ 0 < (𝐴 − 𝑈))) |
94 | 92, 93 | sylibr 224 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) ∈
ℝ+) |
95 | 81, 75, 94 | lemuldivd 12112 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (𝐴 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ 𝐵 ≤ ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))) |
96 | 80, 95 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈))) |
97 | 5 | fveq2d 6354 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (𝐺‘𝑈)) |
98 | | unbdqndv2lem2.g |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴))) |
99 | 98 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))) |
100 | | fveq2 6350 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑈 → (𝐹‘𝑧) = (𝐹‘𝑈)) |
101 | 100 | oveq1d 6826 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑈 → ((𝐹‘𝑧) − (𝐹‘𝐴)) = ((𝐹‘𝑈) − (𝐹‘𝐴))) |
102 | | oveq1 6818 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑈 → (𝑧 − 𝐴) = (𝑈 − 𝐴)) |
103 | 101, 102 | oveq12d 6829 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑈 → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) |
104 | 103 | adantl 473 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑧 = 𝑈) → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) |
105 | | ovexd 6841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)) ∈ V) |
106 | 99, 104, 54, 105 | fvmptd 6448 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑈) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) |
107 | 97, 106 | eqtrd 2792 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) |
108 | 107 | fveq2d 6354 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)))) |
109 | 73 | adantr 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐹‘𝑈) − (𝐹‘𝐴)) ∈ ℂ) |
110 | 30 | recnd 10258 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ ℂ) |
111 | 34 | recnd 10258 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
112 | 110, 111 | subcld 10582 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑈 − 𝐴) ∈ ℂ) |
113 | 112 | adantr 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 − 𝐴) ∈ ℂ) |
114 | 110 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ ℂ) |
115 | 111 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ∈ ℂ) |
116 | 114, 115,
51 | subne0d 10591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 − 𝐴) ≠ 0) |
117 | 109, 113,
116 | absdivd 14391 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (abs‘(𝑈 − 𝐴)))) |
118 | 59 | oveq2d 6827 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (abs‘(𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈))) |
119 | 117, 118 | eqtrd 2792 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈))) |
120 | 108, 119 | eqtrd 2792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈))) |
121 | 120 | eqcomd 2764 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)) = (abs‘(𝐺‘𝑊))) |
122 | 96, 121 | breqtrd 4828 |
. . . 4
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ (abs‘(𝐺‘𝑊))) |
123 | 68, 122 | jca 555 |
. . 3
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))) |
124 | 55, 123 | jca 555 |
. 2
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))) |
125 | 1 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉)) |
126 | | simpr 479 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) |
127 | 126 | iffalsed 4239 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑉) |
128 | 125, 127 | eqtrd 2792 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = 𝑉) |
129 | 28 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ 𝑋) |
130 | 30, 29, 37 | abssubge0d 14367 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (abs‘(𝑉 − 𝑈)) = (𝑉 − 𝑈)) |
131 | 130 | oveq2d 6827 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝑈))) = (𝐵 · (𝑉 − 𝑈))) |
132 | 131 | breq1d 4812 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))) |
133 | 132 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))) |
134 | 126, 133 | mtbird 314 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) |
135 | 14, 28 | ffvelrnd 6521 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝑉) ∈ ℂ) |
136 | 31 | recnd 10258 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑉 − 𝑈) ∈ ℂ) |
137 | 44, 42 | gtned 10362 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑉 − 𝑈) ≠ 0) |
138 | | unbdqndv2lem2.5 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · 𝐵) ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈))) |
139 | 135, 15 | subcld 10582 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐹‘𝑉) − (𝐹‘𝑈)) ∈ ℂ) |
140 | 139, 136,
137 | absdivd 14391 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (abs‘(𝑉 − 𝑈)))) |
141 | 130 | oveq2d 6827 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (abs‘(𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈))) |
142 | 140, 141 | eqtrd 2792 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈))) |
143 | 142 | eqcomd 2764 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)) = (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈)))) |
144 | 138, 143 | breqtrd 4828 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · 𝐵) ≤ (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈)))) |
145 | 135, 15, 72, 136, 25, 137, 144 | unbdqndv2lem1 32804 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))) |
146 | 145 | adantr 472 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))) |
147 | | orel2 397 |
. . . . . . . . . . 11
⊢ (¬
(𝐵 ·
(abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) → (((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))))) |
148 | 134, 146,
147 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴)))) |
149 | 148 | adantr 472 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴)))) |
150 | | fveq2 6350 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 = 𝐴 → (𝐹‘𝑉) = (𝐹‘𝐴)) |
151 | 150 | oveq1d 6826 |
. . . . . . . . . . . . . 14
⊢ (𝑉 = 𝐴 → ((𝐹‘𝑉) − (𝐹‘𝐴)) = ((𝐹‘𝐴) − (𝐹‘𝐴))) |
152 | 151 | adantl 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝑉) − (𝐹‘𝐴)) = ((𝐹‘𝐴) − (𝐹‘𝐴))) |
153 | 72 | subidd 10570 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐹‘𝐴) − (𝐹‘𝐴)) = 0) |
154 | 153 | adantr 472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝐴) − (𝐹‘𝐴)) = 0) |
155 | 152, 154 | eqtrd 2792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝑉) − (𝐹‘𝐴)) = 0) |
156 | 155 | fveq2d 6354 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = (abs‘0)) |
157 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘0) = 0) |
158 | 156, 157 | eqtrd 2792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = 0) |
159 | 158 | adantlr 753 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = 0) |
160 | 149, 159 | breqtrd 4828 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0) |
161 | 131 | breq1d 4812 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0 ↔ (𝐵 · (𝑉 − 𝑈)) ≤ 0)) |
162 | 47, 161 | mtbird 314 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0) |
163 | 162 | adantr 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0) |
164 | 163 | adantr 472 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0) |
165 | 160, 164 | pm2.65da 601 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ 𝑉 = 𝐴) |
166 | 165 | neqned 2937 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ≠ 𝐴) |
167 | 129, 166 | jca 555 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴)) |
168 | | eldifsn 4460 |
. . . . 5
⊢ (𝑉 ∈ (𝑋 ∖ {𝐴}) ↔ (𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴)) |
169 | 167, 168 | sylibr 224 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ (𝑋 ∖ {𝐴})) |
170 | 128, 169 | eqeltrd 2837 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 ∈ (𝑋 ∖ {𝐴})) |
171 | 128 | oveq1d 6826 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 − 𝐴) = (𝑉 − 𝐴)) |
172 | 171 | fveq2d 6354 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (abs‘(𝑉 − 𝐴))) |
173 | 34, 29, 36 | abssubge0d 14367 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) = (𝑉 − 𝐴)) |
174 | 173 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑉 − 𝐴)) = (𝑉 − 𝐴)) |
175 | 172, 174 | eqtrd 2792 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (𝑉 − 𝐴)) |
176 | 29, 34 | resubcld 10648 |
. . . . . . 7
⊢ (𝜑 → (𝑉 − 𝐴) ∈ ℝ) |
177 | 30, 34, 29, 35 | lesub2dd 10834 |
. . . . . . 7
⊢ (𝜑 → (𝑉 − 𝐴) ≤ (𝑉 − 𝑈)) |
178 | 176, 31, 63, 177, 65 | lelttrd 10385 |
. . . . . 6
⊢ (𝜑 → (𝑉 − 𝐴) < 𝐷) |
179 | 178 | adantr 472 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) < 𝐷) |
180 | 175, 179 | eqbrtrd 4824 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) < 𝐷) |
181 | 173, 176 | eqeltrd 2837 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) ∈ ℝ) |
182 | 26, 181 | remulcld 10260 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝐴))) ∈ ℝ) |
183 | 182 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ∈ ℝ) |
184 | 131, 45 | eqeltrd 2837 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝑈))) ∈ ℝ) |
185 | 184 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ∈ ℝ) |
186 | 135, 72 | subcld 10582 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑉) − (𝐹‘𝐴)) ∈ ℂ) |
187 | 186 | abscld 14372 |
. . . . . . . 8
⊢ (𝜑 → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∈ ℝ) |
188 | 187 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∈ ℝ) |
189 | 130, 31 | eqeltrd 2837 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑉 − 𝑈)) ∈ ℝ) |
190 | 177, 173,
130 | 3brtr4d 4834 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) ≤ (abs‘(𝑉 − 𝑈))) |
191 | 181, 189,
26, 76, 190 | lemul2ad 11154 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (𝐵 · (abs‘(𝑉 − 𝑈)))) |
192 | 191 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (𝐵 · (abs‘(𝑉 − 𝑈)))) |
193 | 183, 185,
188, 192, 148 | letrd 10384 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴)))) |
194 | 26 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ∈ ℝ) |
195 | 176 | recnd 10258 |
. . . . . . . . 9
⊢ (𝜑 → (𝑉 − 𝐴) ∈ ℂ) |
196 | 195 | adantr 472 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) ∈ ℂ) |
197 | 29 | recnd 10258 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ ℂ) |
198 | 197 | adantr 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ ℂ) |
199 | 111 | adantr 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ∈ ℂ) |
200 | 198, 199,
166 | subne0d 10591 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) ≠ 0) |
201 | 196, 200 | absrpcld 14384 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑉 − 𝐴)) ∈
ℝ+) |
202 | 194, 188,
201 | lemuldivd 12112 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ↔ 𝐵 ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))))) |
203 | 193, 202 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴)))) |
204 | 128 | fveq2d 6354 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (𝐺‘𝑉)) |
205 | 98 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))) |
206 | | fveq2 6350 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑉 → (𝐹‘𝑧) = (𝐹‘𝑉)) |
207 | 206 | oveq1d 6826 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑉 → ((𝐹‘𝑧) − (𝐹‘𝐴)) = ((𝐹‘𝑉) − (𝐹‘𝐴))) |
208 | | oveq1 6818 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑉 → (𝑧 − 𝐴) = (𝑉 − 𝐴)) |
209 | 207, 208 | oveq12d 6829 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑉 → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) |
210 | 209 | adantl 473 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑧 = 𝑉) → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) |
211 | | ovexd 6841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)) ∈ V) |
212 | 205, 210,
169, 211 | fvmptd 6448 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑉) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) |
213 | 204, 212 | eqtrd 2792 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) |
214 | 213 | fveq2d 6354 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = (abs‘(((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)))) |
215 | 186 | adantr 472 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐹‘𝑉) − (𝐹‘𝐴)) ∈ ℂ) |
216 | 215, 196,
200 | absdivd 14391 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴)))) |
217 | 214, 216 | eqtrd 2792 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴)))) |
218 | 217 | eqcomd 2764 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))) = (abs‘(𝐺‘𝑊))) |
219 | 203, 218 | breqtrd 4828 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ (abs‘(𝐺‘𝑊))) |
220 | 180, 219 | jca 555 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))) |
221 | 170, 220 | jca 555 |
. 2
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))) |
222 | 124, 221 | pm2.61dan 867 |
1
⊢ (𝜑 → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))) |