Proof of Theorem unbdqndv2lem2
Step | Hyp | Ref
| Expression |
1 | | unbdqndv2lem2.w |
. . . . . 6
⊢ 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) |
2 | 1 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉)) |
3 | | iftrue 4042 |
. . . . . 6
⊢ ((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑈) |
4 | 3 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑈) |
5 | 2, 4 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = 𝑈) |
6 | | unbdqndv2lem2.u |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ 𝑋) |
7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ 𝑋) |
8 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) |
9 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 = 𝐴 → (𝐹‘𝑈) = (𝐹‘𝐴)) |
10 | 9 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝑈 = 𝐴 → (𝐹‘𝐴) = (𝐹‘𝑈)) |
11 | 10 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑈 = 𝐴 → ((𝐹‘𝑈) − (𝐹‘𝐴)) = ((𝐹‘𝑈) − (𝐹‘𝑈))) |
12 | 11 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑈 = 𝐴 → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = (abs‘((𝐹‘𝑈) − (𝐹‘𝑈)))) |
13 | 12 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = (abs‘((𝐹‘𝑈) − (𝐹‘𝑈)))) |
14 | | unbdqndv2lem2.f |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
15 | 14, 6 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘𝑈) ∈ ℂ) |
16 | 15 | subidd 10259 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐹‘𝑈) − (𝐹‘𝑈)) = 0) |
17 | 16 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = (abs‘0)) |
18 | 17 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = (abs‘0)) |
19 | | abs0 13873 |
. . . . . . . . . . . . 13
⊢
(abs‘0) = 0 |
20 | 19 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘0) = 0) |
21 | 18, 20 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝑈))) = 0) |
22 | 13, 21 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = 0) |
23 | 22 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) = 0) |
24 | 8, 23 | breqtrd 4609 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → (𝐵 · (𝑉 − 𝑈)) ≤ 0) |
25 | | unbdqndv2lem2.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
26 | 25 | rpred 11748 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℝ) |
27 | | unbdqndv2lem2.x |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
28 | | unbdqndv2lem2.v |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑉 ∈ 𝑋) |
29 | 27, 28 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑉 ∈ ℝ) |
30 | 27, 6 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ ℝ) |
31 | 29, 30 | resubcld 10337 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑉 − 𝑈) ∈ ℝ) |
32 | 25 | rpgt0d 11751 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐵) |
33 | | unbdqndv2lem2.a |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
34 | 27, 33 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
35 | | unbdqndv2lem2.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ≤ 𝐴) |
36 | | unbdqndv2lem2.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ≤ 𝑉) |
37 | 30, 34, 29, 35, 36 | letrd 10073 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ≤ 𝑉) |
38 | | unbdqndv2lem2.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ≠ 𝑉) |
39 | 38 | necomd 2837 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑉 ≠ 𝑈) |
40 | 30, 29, 37, 39 | leneltd 10070 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 < 𝑉) |
41 | 30, 29 | posdifd 10493 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 < 𝑉 ↔ 0 < (𝑉 − 𝑈))) |
42 | 40, 41 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝑉 − 𝑈)) |
43 | 26, 31, 32, 42 | mulgt0d 10071 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (𝐵 · (𝑉 − 𝑈))) |
44 | | 0red 9920 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℝ) |
45 | 26, 31 | remulcld 9949 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 · (𝑉 − 𝑈)) ∈ ℝ) |
46 | 44, 45 | ltnled 10063 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 < (𝐵 · (𝑉 − 𝑈)) ↔ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0)) |
47 | 43, 46 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0) |
48 | 47 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0) |
49 | 48 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑈 = 𝐴) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ 0) |
50 | 24, 49 | pm2.65da 598 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ 𝑈 = 𝐴) |
51 | 50 | neqned 2789 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ≠ 𝐴) |
52 | 7, 51 | jca 553 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴)) |
53 | | eldifsn 4260 |
. . . . 5
⊢ (𝑈 ∈ (𝑋 ∖ {𝐴}) ↔ (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝐴)) |
54 | 52, 53 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ (𝑋 ∖ {𝐴})) |
55 | 5, 54 | eqeltrd 2688 |
. . 3
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 ∈ (𝑋 ∖ {𝐴})) |
56 | 5 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 − 𝐴) = (𝑈 − 𝐴)) |
57 | 56 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (abs‘(𝑈 − 𝐴))) |
58 | 30, 34, 35 | abssuble0d 14019 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝑈 − 𝐴)) = (𝐴 − 𝑈)) |
59 | 58 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑈 − 𝐴)) = (𝐴 − 𝑈)) |
60 | 57, 59 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (𝐴 − 𝑈)) |
61 | 34, 30 | resubcld 10337 |
. . . . . . 7
⊢ (𝜑 → (𝐴 − 𝑈) ∈ ℝ) |
62 | | unbdqndv2lem2.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈
ℝ+) |
63 | 62 | rpred 11748 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℝ) |
64 | 34, 29, 30, 36 | lesub1dd 10522 |
. . . . . . 7
⊢ (𝜑 → (𝐴 − 𝑈) ≤ (𝑉 − 𝑈)) |
65 | | unbdqndv2lem2.4 |
. . . . . . 7
⊢ (𝜑 → (𝑉 − 𝑈) < 𝐷) |
66 | 61, 31, 63, 64, 65 | lelttrd 10074 |
. . . . . 6
⊢ (𝜑 → (𝐴 − 𝑈) < 𝐷) |
67 | 66 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) < 𝐷) |
68 | 60, 67 | eqbrtrd 4605 |
. . . 4
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) < 𝐷) |
69 | 26, 61 | remulcld 9949 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (𝐴 − 𝑈)) ∈ ℝ) |
70 | 69 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ∈ ℝ) |
71 | 45 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝑉 − 𝑈)) ∈ ℝ) |
72 | 14, 33 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ) |
73 | 15, 72 | subcld 10271 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑈) − (𝐹‘𝐴)) ∈ ℂ) |
74 | 73 | abscld 14023 |
. . . . . . . 8
⊢ (𝜑 → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ∈ ℝ) |
75 | 74 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ∈ ℝ) |
76 | 44, 26, 32 | ltled 10064 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐵) |
77 | 61, 31, 26, 76, 64 | lemul2ad 10843 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (𝐴 − 𝑈)) ≤ (𝐵 · (𝑉 − 𝑈))) |
78 | 77 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ≤ (𝐵 · (𝑉 − 𝑈))) |
79 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) |
80 | 70, 71, 75, 78, 79 | letrd 10073 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (𝐴 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) |
81 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ∈ ℝ) |
82 | 61 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) ∈ ℝ) |
83 | 35 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ≤ 𝐴) |
84 | 51 | necomd 2837 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ≠ 𝑈) |
85 | 83, 84 | jca 553 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈)) |
86 | 30, 34 | ltlend 10061 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 < 𝐴 ↔ (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈))) |
87 | 86 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 < 𝐴 ↔ (𝑈 ≤ 𝐴 ∧ 𝐴 ≠ 𝑈))) |
88 | 85, 87 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 < 𝐴) |
89 | 30, 34 | posdifd 10493 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈 < 𝐴 ↔ 0 < (𝐴 − 𝑈))) |
90 | 89 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 < 𝐴 ↔ 0 < (𝐴 − 𝑈))) |
91 | 88, 90 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 0 < (𝐴 − 𝑈)) |
92 | 82, 91 | jca 553 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐴 − 𝑈) ∈ ℝ ∧ 0 < (𝐴 − 𝑈))) |
93 | | elrp 11710 |
. . . . . . . 8
⊢ ((𝐴 − 𝑈) ∈ ℝ+ ↔ ((𝐴 − 𝑈) ∈ ℝ ∧ 0 < (𝐴 − 𝑈))) |
94 | 92, 93 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐴 − 𝑈) ∈
ℝ+) |
95 | 81, 75, 94 | lemuldivd 11797 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (𝐴 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ 𝐵 ≤ ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)))) |
96 | 80, 95 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈))) |
97 | 5 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (𝐺‘𝑈)) |
98 | | unbdqndv2lem2.g |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴))) |
99 | 98 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))) |
100 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑈 → (𝐹‘𝑧) = (𝐹‘𝑈)) |
101 | 100 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑈 → ((𝐹‘𝑧) − (𝐹‘𝐴)) = ((𝐹‘𝑈) − (𝐹‘𝐴))) |
102 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑈 → (𝑧 − 𝐴) = (𝑈 − 𝐴)) |
103 | 101, 102 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑈 → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) |
104 | 103 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑧 = 𝑈) → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) |
105 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)) ∈ V |
106 | 105 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)) ∈ V) |
107 | 99, 104, 54, 106 | fvmptd 6197 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑈) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) |
108 | 97, 107 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) |
109 | 108 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴)))) |
110 | 73 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐹‘𝑈) − (𝐹‘𝐴)) ∈ ℂ) |
111 | 30 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ ℂ) |
112 | 34 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
113 | 111, 112 | subcld 10271 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑈 − 𝐴) ∈ ℂ) |
114 | 113 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 − 𝐴) ∈ ℂ) |
115 | 111 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑈 ∈ ℂ) |
116 | 112 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ∈ ℂ) |
117 | 115, 116,
51 | subne0d 10280 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑈 − 𝐴) ≠ 0) |
118 | 110, 114,
117 | absdivd 14042 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (abs‘(𝑈 − 𝐴)))) |
119 | 59 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (abs‘(𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈))) |
120 | 118, 119 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑈) − (𝐹‘𝐴)) / (𝑈 − 𝐴))) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈))) |
121 | 109, 120 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈))) |
122 | 121 | eqcomd 2616 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) / (𝐴 − 𝑈)) = (abs‘(𝐺‘𝑊))) |
123 | 96, 122 | breqtrd 4609 |
. . . 4
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ (abs‘(𝐺‘𝑊))) |
124 | 68, 123 | jca 553 |
. . 3
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))) |
125 | 55, 124 | jca 553 |
. 2
⊢ ((𝜑 ∧ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))) |
126 | 1 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉)) |
127 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) |
128 | 127 | iffalsed 4047 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → if((𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))), 𝑈, 𝑉) = 𝑉) |
129 | 126, 128 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 = 𝑉) |
130 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ 𝑋) |
131 | 30, 29, 37 | abssubge0d 14018 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (abs‘(𝑉 − 𝑈)) = (𝑉 − 𝑈)) |
132 | 131 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝑈))) = (𝐵 · (𝑉 − 𝑈))) |
133 | 132 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))) |
134 | 133 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) ↔ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))) |
135 | 127, 134 | mtbird 314 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) |
136 | 14, 28 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝑉) ∈ ℂ) |
137 | 31 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑉 − 𝑈) ∈ ℂ) |
138 | 44, 42 | gtned 10051 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑉 − 𝑈) ≠ 0) |
139 | | unbdqndv2lem2.5 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · 𝐵) ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈))) |
140 | 136, 15 | subcld 10271 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐹‘𝑉) − (𝐹‘𝑈)) ∈ ℂ) |
141 | 140, 137,
138 | absdivd 14042 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (abs‘(𝑉 − 𝑈)))) |
142 | 131 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (abs‘(𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈))) |
143 | 141, 142 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈))) |
144 | 143 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((abs‘((𝐹‘𝑉) − (𝐹‘𝑈))) / (𝑉 − 𝑈)) = (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈)))) |
145 | 139, 144 | breqtrd 4609 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · 𝐵) ≤ (abs‘(((𝐹‘𝑉) − (𝐹‘𝑈)) / (𝑉 − 𝑈)))) |
146 | 136, 15, 72, 137, 25, 138, 145 | unbdqndv2lem1 31670 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))) |
147 | 146 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))))) |
148 | | orel2 397 |
. . . . . . . . . . 11
⊢ (¬
(𝐵 ·
(abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴))) → (((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∨ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))))) |
149 | 135, 147,
148 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴)))) |
150 | 149 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴)))) |
151 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 = 𝐴 → (𝐹‘𝑉) = (𝐹‘𝐴)) |
152 | 151 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑉 = 𝐴 → ((𝐹‘𝑉) − (𝐹‘𝐴)) = ((𝐹‘𝐴) − (𝐹‘𝐴))) |
153 | 152 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝑉) − (𝐹‘𝐴)) = ((𝐹‘𝐴) − (𝐹‘𝐴))) |
154 | 72 | subidd 10259 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐹‘𝐴) − (𝐹‘𝐴)) = 0) |
155 | 154 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝐴) − (𝐹‘𝐴)) = 0) |
156 | 153, 155 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → ((𝐹‘𝑉) − (𝐹‘𝐴)) = 0) |
157 | 156 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = (abs‘0)) |
158 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘0) = 0) |
159 | 157, 158 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = 0) |
160 | 159 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) = 0) |
161 | 150, 160 | breqtrd 4609 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0) |
162 | 132 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0 ↔ (𝐵 · (𝑉 − 𝑈)) ≤ 0)) |
163 | 47, 162 | mtbird 314 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0) |
164 | 163 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0) |
165 | 164 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑉 = 𝐴) → ¬ (𝐵 · (abs‘(𝑉 − 𝑈))) ≤ 0) |
166 | 161, 165 | pm2.65da 598 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ¬ 𝑉 = 𝐴) |
167 | 166 | neqned 2789 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ≠ 𝐴) |
168 | 130, 167 | jca 553 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴)) |
169 | | eldifsn 4260 |
. . . . 5
⊢ (𝑉 ∈ (𝑋 ∖ {𝐴}) ↔ (𝑉 ∈ 𝑋 ∧ 𝑉 ≠ 𝐴)) |
170 | 168, 169 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ (𝑋 ∖ {𝐴})) |
171 | 129, 170 | eqeltrd 2688 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑊 ∈ (𝑋 ∖ {𝐴})) |
172 | 129 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 − 𝐴) = (𝑉 − 𝐴)) |
173 | 172 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (abs‘(𝑉 − 𝐴))) |
174 | 34, 29, 36 | abssubge0d 14018 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) = (𝑉 − 𝐴)) |
175 | 174 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑉 − 𝐴)) = (𝑉 − 𝐴)) |
176 | 173, 175 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) = (𝑉 − 𝐴)) |
177 | 29, 34 | resubcld 10337 |
. . . . . . 7
⊢ (𝜑 → (𝑉 − 𝐴) ∈ ℝ) |
178 | 30, 34, 29, 35 | lesub2dd 10523 |
. . . . . . 7
⊢ (𝜑 → (𝑉 − 𝐴) ≤ (𝑉 − 𝑈)) |
179 | 177, 31, 63, 178, 65 | lelttrd 10074 |
. . . . . 6
⊢ (𝜑 → (𝑉 − 𝐴) < 𝐷) |
180 | 179 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) < 𝐷) |
181 | 176, 180 | eqbrtrd 4605 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑊 − 𝐴)) < 𝐷) |
182 | 174, 177 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) ∈ ℝ) |
183 | 26, 182 | remulcld 9949 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝐴))) ∈ ℝ) |
184 | 183 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ∈ ℝ) |
185 | 132, 45 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝑈))) ∈ ℝ) |
186 | 185 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝑈))) ∈ ℝ) |
187 | 136, 72 | subcld 10271 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑉) − (𝐹‘𝐴)) ∈ ℂ) |
188 | 187 | abscld 14023 |
. . . . . . . 8
⊢ (𝜑 → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∈ ℝ) |
189 | 188 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ∈ ℝ) |
190 | 131, 31 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑉 − 𝑈)) ∈ ℝ) |
191 | 178, 174,
131 | 3brtr4d 4615 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑉 − 𝐴)) ≤ (abs‘(𝑉 − 𝑈))) |
192 | 182, 190,
26, 76, 191 | lemul2ad 10843 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (𝐵 · (abs‘(𝑉 − 𝑈)))) |
193 | 192 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (𝐵 · (abs‘(𝑉 − 𝑈)))) |
194 | 184, 186,
189, 193, 149 | letrd 10073 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴)))) |
195 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ∈ ℝ) |
196 | 177 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → (𝑉 − 𝐴) ∈ ℂ) |
197 | 196 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) ∈ ℂ) |
198 | 29 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ ℂ) |
199 | 198 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝑉 ∈ ℂ) |
200 | 112 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐴 ∈ ℂ) |
201 | 199, 200,
167 | subne0d 10280 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑉 − 𝐴) ≠ 0) |
202 | 197, 201 | absrpcld 14035 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝑉 − 𝐴)) ∈
ℝ+) |
203 | 195, 189,
202 | lemuldivd 11797 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐵 · (abs‘(𝑉 − 𝐴))) ≤ (abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) ↔ 𝐵 ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))))) |
204 | 194, 203 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴)))) |
205 | 129 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (𝐺‘𝑉)) |
206 | 98 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐺 = (𝑧 ∈ (𝑋 ∖ {𝐴}) ↦ (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)))) |
207 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑉 → (𝐹‘𝑧) = (𝐹‘𝑉)) |
208 | 207 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑉 → ((𝐹‘𝑧) − (𝐹‘𝐴)) = ((𝐹‘𝑉) − (𝐹‘𝐴))) |
209 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑉 → (𝑧 − 𝐴) = (𝑉 − 𝐴)) |
210 | 208, 209 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑉 → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) |
211 | 210 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) ∧ 𝑧 = 𝑉) → (((𝐹‘𝑧) − (𝐹‘𝐴)) / (𝑧 − 𝐴)) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) |
212 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)) ∈ V |
213 | 212 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)) ∈ V) |
214 | 206, 211,
170, 213 | fvmptd 6197 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑉) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) |
215 | 205, 214 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝐺‘𝑊) = (((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) |
216 | 215 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = (abs‘(((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴)))) |
217 | 187 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((𝐹‘𝑉) − (𝐹‘𝐴)) ∈ ℂ) |
218 | 217, 197,
201 | absdivd 14042 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(((𝐹‘𝑉) − (𝐹‘𝐴)) / (𝑉 − 𝐴))) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴)))) |
219 | 216, 218 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (abs‘(𝐺‘𝑊)) = ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴)))) |
220 | 219 | eqcomd 2616 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘((𝐹‘𝑉) − (𝐹‘𝐴))) / (abs‘(𝑉 − 𝐴))) = (abs‘(𝐺‘𝑊))) |
221 | 204, 220 | breqtrd 4609 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → 𝐵 ≤ (abs‘(𝐺‘𝑊))) |
222 | 181, 221 | jca 553 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊)))) |
223 | 171, 222 | jca 553 |
. 2
⊢ ((𝜑 ∧ ¬ (𝐵 · (𝑉 − 𝑈)) ≤ (abs‘((𝐹‘𝑈) − (𝐹‘𝐴)))) → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))) |
224 | 125, 223 | pm2.61dan 828 |
1
⊢ (𝜑 → (𝑊 ∈ (𝑋 ∖ {𝐴}) ∧ ((abs‘(𝑊 − 𝐴)) < 𝐷 ∧ 𝐵 ≤ (abs‘(𝐺‘𝑊))))) |