Step | Hyp | Ref
| Expression |
1 | | aalioulem2.d |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | 1re 9918 |
. . . . 5
⊢ 1 ∈
ℝ |
3 | | resubcl 10224 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐴 −
1) ∈ ℝ) |
4 | 1, 2, 3 | sylancl 693 |
. . . 4
⊢ (𝜑 → (𝐴 − 1) ∈ ℝ) |
5 | | peano2re 10088 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈
ℝ) |
6 | 1, 5 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐴 + 1) ∈ ℝ) |
7 | | reelprrecn 9907 |
. . . . 5
⊢ ℝ
∈ {ℝ, ℂ} |
8 | | ssid 3587 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
9 | | fncpn 23502 |
. . . . . . . . 9
⊢ (ℂ
⊆ ℂ → (Cn‘ℂ) Fn
ℕ0) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢
(Cn‘ℂ) Fn
ℕ0 |
11 | | 1nn0 11185 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
12 | | fnfvelrn 6264 |
. . . . . . . 8
⊢
(((Cn‘ℂ) Fn ℕ0 ∧ 1
∈ ℕ0) →
((Cn‘ℂ)‘1) ∈ ran
(Cn‘ℂ)) |
13 | 10, 11, 12 | mp2an 704 |
. . . . . . 7
⊢
((Cn‘ℂ)‘1) ∈ ran
(Cn‘ℂ) |
14 | | intss1 4427 |
. . . . . . 7
⊢
(((Cn‘ℂ)‘1) ∈ ran
(Cn‘ℂ) → ∩ ran
(Cn‘ℂ) ⊆
((Cn‘ℂ)‘1)) |
15 | 13, 14 | ax-mp 5 |
. . . . . 6
⊢ ∩ ran (Cn‘ℂ) ⊆
((Cn‘ℂ)‘1) |
16 | | aalioulem2.b |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℤ)) |
17 | | plycpn 23848 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℤ)
→ 𝐹 ∈ ∩ ran
(Cn‘ℂ)) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ ∩ ran
(Cn‘ℂ)) |
19 | 15, 18 | sseldi 3566 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈
((Cn‘ℂ)‘1)) |
20 | | cpnres 23506 |
. . . . 5
⊢ ((ℝ
∈ {ℝ, ℂ} ∧ 𝐹 ∈
((Cn‘ℂ)‘1)) → (𝐹 ↾ ℝ) ∈
((Cn‘ℝ)‘1)) |
21 | 7, 19, 20 | sylancr 694 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ ℝ) ∈
((Cn‘ℝ)‘1)) |
22 | | df-ima 5051 |
. . . . 5
⊢ (𝐹 “ ℝ) = ran (𝐹 ↾
ℝ) |
23 | | zssre 11261 |
. . . . . . . . 9
⊢ ℤ
⊆ ℝ |
24 | | ax-resscn 9872 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
25 | | plyss 23759 |
. . . . . . . . 9
⊢ ((ℤ
⊆ ℝ ∧ ℝ ⊆ ℂ) → (Poly‘ℤ)
⊆ (Poly‘ℝ)) |
26 | 23, 24, 25 | mp2an 704 |
. . . . . . . 8
⊢
(Poly‘ℤ) ⊆ (Poly‘ℝ) |
27 | 26, 16 | sseldi 3566 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℝ)) |
28 | | plyreres 23842 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹 ↾
ℝ):ℝ⟶ℝ) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾
ℝ):ℝ⟶ℝ) |
30 | | frn 5966 |
. . . . . 6
⊢ ((𝐹 ↾
ℝ):ℝ⟶ℝ → ran (𝐹 ↾ ℝ) ⊆
ℝ) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ↾ ℝ) ⊆
ℝ) |
32 | 22, 31 | syl5eqss 3612 |
. . . 4
⊢ (𝜑 → (𝐹 “ ℝ) ⊆
ℝ) |
33 | | iccssre 12126 |
. . . . . . 7
⊢ (((𝐴 − 1) ∈ ℝ ∧
(𝐴 + 1) ∈ ℝ)
→ ((𝐴 −
1)[,](𝐴 + 1)) ⊆
ℝ) |
34 | 4, 6, 33 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ ℝ) |
35 | 34, 24 | syl6ss 3580 |
. . . . 5
⊢ (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ ℂ) |
36 | | plyf 23758 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℤ)
→ 𝐹:ℂ⟶ℂ) |
37 | 16, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
38 | | fdm 5964 |
. . . . . 6
⊢ (𝐹:ℂ⟶ℂ →
dom 𝐹 =
ℂ) |
39 | 37, 38 | syl 17 |
. . . . 5
⊢ (𝜑 → dom 𝐹 = ℂ) |
40 | 35, 39 | sseqtr4d 3605 |
. . . 4
⊢ (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ dom 𝐹) |
41 | 4, 6, 21, 32, 40 | c1lip3 23566 |
. . 3
⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏)))) |
42 | | simp2 1055 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝑟 ∈ ℝ) |
43 | 42 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝑟 ∈ ℂ) |
44 | 1 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐴 ∈ ℝ) |
45 | 44 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐴 ∈ ℝ) |
46 | 45 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐴 ∈ ℂ) |
47 | 43, 46 | abssubd 14040 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘(𝑟 − 𝐴)) = (abs‘(𝐴 − 𝑟))) |
48 | | simp3 1056 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘(𝐴 − 𝑟)) ≤ 1) |
49 | 47, 48 | eqbrtrd 4605 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘(𝑟 − 𝐴)) ≤ 1) |
50 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 1 ∈
ℝ) |
51 | | elicc4abs 13907 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝑟 ∈
ℝ) → (𝑟 ∈
((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝑟 − 𝐴)) ≤ 1)) |
52 | 45, 50, 42, 51 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝑟 − 𝐴)) ≤ 1)) |
53 | 49, 52 | mpbird 246 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1))) |
54 | 1 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℂ) |
55 | 54 | subidd 10259 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 − 𝐴) = 0) |
56 | 55 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘(𝐴 − 𝐴)) = (abs‘0)) |
57 | | abs0 13873 |
. . . . . . . . . . . . . . 15
⊢
(abs‘0) = 0 |
58 | | 0le1 10430 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
1 |
59 | 57, 58 | eqbrtri 4604 |
. . . . . . . . . . . . . 14
⊢
(abs‘0) ≤ 1 |
60 | 56, 59 | syl6eqbr 4622 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘(𝐴 − 𝐴)) ≤ 1) |
61 | | 1red 9934 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ) |
62 | | elicc4abs 13907 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝐴 ∈
ℝ) → (𝐴 ∈
((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝐴 − 𝐴)) ≤ 1)) |
63 | 1, 61, 1, 62 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝐴 − 𝐴)) ≤ 1)) |
64 | 60, 63 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) |
65 | 64 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) |
66 | 65 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) |
67 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑟 → (𝐹‘𝑏) = (𝐹‘𝑟)) |
68 | 67 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑟 → ((𝐹‘𝑐) − (𝐹‘𝑏)) = ((𝐹‘𝑐) − (𝐹‘𝑟))) |
69 | 68 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑟 → (abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) = (abs‘((𝐹‘𝑐) − (𝐹‘𝑟)))) |
70 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑟 → (𝑐 − 𝑏) = (𝑐 − 𝑟)) |
71 | 70 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑟 → (abs‘(𝑐 − 𝑏)) = (abs‘(𝑐 − 𝑟))) |
72 | 71 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑟 → (𝑎 · (abs‘(𝑐 − 𝑏))) = (𝑎 · (abs‘(𝑐 − 𝑟)))) |
73 | 69, 72 | breq12d 4596 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑟 → ((abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) ↔ (abs‘((𝐹‘𝑐) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝑐 − 𝑟))))) |
74 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝐴 → (𝐹‘𝑐) = (𝐹‘𝐴)) |
75 | 74 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝐴 → ((𝐹‘𝑐) − (𝐹‘𝑟)) = ((𝐹‘𝐴) − (𝐹‘𝑟))) |
76 | 75 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝐴 → (abs‘((𝐹‘𝑐) − (𝐹‘𝑟))) = (abs‘((𝐹‘𝐴) − (𝐹‘𝑟)))) |
77 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝐴 → (𝑐 − 𝑟) = (𝐴 − 𝑟)) |
78 | 77 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝐴 → (abs‘(𝑐 − 𝑟)) = (abs‘(𝐴 − 𝑟))) |
79 | 78 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝐴 → (𝑎 · (abs‘(𝑐 − 𝑟))) = (𝑎 · (abs‘(𝐴 − 𝑟)))) |
80 | 76, 79 | breq12d 4596 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝐴 → ((abs‘((𝐹‘𝑐) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝑐 − 𝑟))) ↔ (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
81 | 73, 80 | rspc2v 3293 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ∧ 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
82 | 53, 66, 81 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
83 | | simp1l 1078 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝜑) |
84 | | aalioulem3.e |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘𝐴) = 0) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝐹‘𝐴) = 0) |
86 | | 0cn 9911 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℂ |
87 | 85, 86 | syl6eqel 2696 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝐹‘𝐴) ∈ ℂ) |
88 | 37 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐹:ℂ⟶ℂ) |
89 | 88 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐹:ℂ⟶ℂ) |
90 | 89, 43 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝐹‘𝑟) ∈ ℂ) |
91 | 87, 90 | abssubd 14040 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) = (abs‘((𝐹‘𝑟) − (𝐹‘𝐴)))) |
92 | 85 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((𝐹‘𝑟) − (𝐹‘𝐴)) = ((𝐹‘𝑟) − 0)) |
93 | 90 | subid1d 10260 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((𝐹‘𝑟) − 0) = (𝐹‘𝑟)) |
94 | 92, 93 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((𝐹‘𝑟) − (𝐹‘𝐴)) = (𝐹‘𝑟)) |
95 | 94 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘((𝐹‘𝑟) − (𝐹‘𝐴))) = (abs‘(𝐹‘𝑟))) |
96 | 91, 95 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) = (abs‘(𝐹‘𝑟))) |
97 | 96 | breq1d 4593 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))) ↔ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
98 | 82, 97 | sylibd 228 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
99 | 98 | 3exp 1256 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑟 ∈ ℝ → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))))) |
100 | 99 | com34 89 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑟 ∈ ℝ → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))))) |
101 | 100 | com23 84 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (𝑟 ∈ ℝ → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))))) |
102 | 101 | ralrimdv 2951 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))))) |
103 | 102 | reximdva 3000 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ ℝ ∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → ∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))))) |
104 | 41, 103 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
105 | | 1rp 11712 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
106 | 105 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 = 0) → 1 ∈
ℝ+) |
107 | | recn 9905 |
. . . . . . . 8
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℂ) |
108 | 107 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℂ) |
109 | | df-ne 2782 |
. . . . . . . 8
⊢ (𝑎 ≠ 0 ↔ ¬ 𝑎 = 0) |
110 | 109 | biimpri 217 |
. . . . . . 7
⊢ (¬
𝑎 = 0 → 𝑎 ≠ 0) |
111 | | absrpcl 13876 |
. . . . . . 7
⊢ ((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) → (abs‘𝑎) ∈
ℝ+) |
112 | 108, 110,
111 | syl2an 493 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 𝑎 = 0) → (abs‘𝑎) ∈
ℝ+) |
113 | 112 | rpreccld 11758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 𝑎 = 0) → (1 /
(abs‘𝑎)) ∈
ℝ+) |
114 | 106, 113 | ifclda 4070 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → if(𝑎 = 0, 1, (1 / (abs‘𝑎))) ∈
ℝ+) |
115 | | eqid 2610 |
. . . . . . . . 9
⊢ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) |
116 | | eqif 4076 |
. . . . . . . . 9
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) ↔ ((𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1) ∨ (¬ 𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎))))) |
117 | 115, 116 | mpbi 219 |
. . . . . . . 8
⊢ ((𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1) ∨ (¬ 𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)))) |
118 | | simplrr 797 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) |
119 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 0 → (𝑎 · (abs‘(𝐴 − 𝑟))) = (0 · (abs‘(𝐴 − 𝑟)))) |
120 | 119 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝑎 · (abs‘(𝐴 − 𝑟))) = (0 · (abs‘(𝐴 − 𝑟)))) |
121 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝐴 ∈ ℝ) |
122 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑟 ∈ ℝ) |
123 | 121, 122 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝐴 − 𝑟) ∈ ℝ) |
124 | 123 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝐴 − 𝑟) ∈ ℂ) |
125 | 124 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐴 − 𝑟)) ∈ ℝ) |
126 | 125 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐴 − 𝑟)) ∈ ℂ) |
127 | 126 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐴 − 𝑟)) ∈ ℂ) |
128 | 127 | mul02d 10113 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (0 · (abs‘(𝐴 − 𝑟))) = 0) |
129 | 120, 128 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝑎 · (abs‘(𝐴 − 𝑟))) = 0) |
130 | 118, 129 | breqtrd 4609 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) ≤ 0) |
131 | 37 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝐹:ℂ⟶ℂ) |
132 | 122 | recnd 9947 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑟 ∈ ℂ) |
133 | 131, 132 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝐹‘𝑟) ∈ ℂ) |
134 | 133 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝐹‘𝑟) ∈ ℂ) |
135 | 134 | absge0d 14031 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → 0 ≤ (abs‘(𝐹‘𝑟))) |
136 | 133 | abscld 14023 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐹‘𝑟)) ∈ ℝ) |
137 | 136 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) ∈ ℝ) |
138 | | 0re 9919 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
139 | | letri3 10002 |
. . . . . . . . . . . . . . . 16
⊢
(((abs‘(𝐹‘𝑟)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((abs‘(𝐹‘𝑟)) = 0 ↔ ((abs‘(𝐹‘𝑟)) ≤ 0 ∧ 0 ≤ (abs‘(𝐹‘𝑟))))) |
140 | 137, 138,
139 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → ((abs‘(𝐹‘𝑟)) = 0 ↔ ((abs‘(𝐹‘𝑟)) ≤ 0 ∧ 0 ≤ (abs‘(𝐹‘𝑟))))) |
141 | 130, 135,
140 | mpbir2and 959 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) = 0) |
142 | 141 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹‘𝑟))) = (1 · 0)) |
143 | | ax-1cn 9873 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
144 | 143 | mul01i 10105 |
. . . . . . . . . . . . 13
⊢ (1
· 0) = 0 |
145 | 142, 144 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹‘𝑟))) = 0) |
146 | 124 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝐴 − 𝑟) ∈ ℂ) |
147 | 146 | absge0d 14031 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → 0 ≤ (abs‘(𝐴 − 𝑟))) |
148 | 145, 147 | eqbrtrd 4605 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) |
149 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) = (1 · (abs‘(𝐹‘𝑟)))) |
150 | 149 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → ((if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)) ↔ (1 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
151 | 148, 150 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
152 | 151 | expimpd 627 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → ((𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
153 | 136 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹‘𝑟)) ∈ ℝ) |
154 | 153 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹‘𝑟)) ∈ ℂ) |
155 | | simpllr 795 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → 𝑎 ∈ ℝ) |
156 | 155 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → 𝑎 ∈ ℂ) |
157 | 156, 111 | sylancom 698 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘𝑎) ∈
ℝ+) |
158 | 157 | rpcnne0d 11757 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘𝑎) ∈ ℂ ∧
(abs‘𝑎) ≠
0)) |
159 | | divrec2 10581 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘(𝐹‘𝑟)) ∈ ℂ ∧ (abs‘𝑎) ∈ ℂ ∧
(abs‘𝑎) ≠ 0)
→ ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) |
160 | 159 | 3expb 1258 |
. . . . . . . . . . . . . 14
⊢
(((abs‘(𝐹‘𝑟)) ∈ ℂ ∧ ((abs‘𝑎) ∈ ℂ ∧
(abs‘𝑎) ≠ 0))
→ ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) |
161 | 154, 158,
160 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) |
162 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑎 ∈ ℝ) |
163 | 162, 125 | remulcld 9949 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝑎 · (abs‘(𝐴 − 𝑟))) ∈ ℝ) |
164 | 162 | recnd 9947 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑎 ∈ ℂ) |
165 | 164 | abscld 14023 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘𝑎) ∈ ℝ) |
166 | 165, 125 | remulcld 9949 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → ((abs‘𝑎) · (abs‘(𝐴 − 𝑟))) ∈ ℝ) |
167 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) |
168 | 124 | absge0d 14031 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 0 ≤ (abs‘(𝐴 − 𝑟))) |
169 | | leabs 13887 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ ℝ → 𝑎 ≤ (abs‘𝑎)) |
170 | 169 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑎 ≤ (abs‘𝑎)) |
171 | 162, 165,
125, 168, 170 | lemul1ad 10842 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝑎 · (abs‘(𝐴 − 𝑟))) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟)))) |
172 | 136, 163,
166, 167, 171 | letrd 10073 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐹‘𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟)))) |
173 | 172 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹‘𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟)))) |
174 | 125 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐴 − 𝑟)) ∈ ℝ) |
175 | 153, 174,
157 | ledivmuld 11801 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) ≤ (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐹‘𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟))))) |
176 | 173, 175 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) ≤ (abs‘(𝐴 − 𝑟))) |
177 | 161, 176 | eqbrtrrd 4607 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) |
178 | 109, 177 | sylan2br 492 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ ¬ 𝑎 = 0) → ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) |
179 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) |
180 | 179 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → ((if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)) ↔ ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
181 | 178, 180 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ ¬ 𝑎 = 0) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
182 | 181 | expimpd 627 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → ((¬ 𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
183 | 152, 182 | jaod 394 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (((𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1) ∨ (¬ 𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
184 | 117, 183 | mpi 20 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) |
185 | 184 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ) → ((abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
186 | 185 | imim2d 55 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ) → (((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
187 | 186 | ralimdva 2945 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 →
(abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
188 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (𝑥 · (abs‘(𝐹‘𝑟))) = (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟)))) |
189 | 188 | breq1d 4593 |
. . . . . . 7
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → ((𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)) ↔ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
190 | 189 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (((abs‘(𝐴 − 𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) ↔ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
191 | 190 | ralbidv 2969 |
. . . . 5
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) ↔ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
192 | 191 | rspcev 3282 |
. . . 4
⊢
((if(𝑎 = 0, 1, (1 /
(abs‘𝑎))) ∈
ℝ+ ∧ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
193 | 114, 187,
192 | syl6an 566 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 →
(abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
194 | 193 | rexlimdva 3013 |
. 2
⊢ (𝜑 → (∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
195 | 104, 194 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |