Step | Hyp | Ref
| Expression |
1 | | aalioulem2.d |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | 1re 10641 |
. . . . 5
⊢ 1 ∈
ℝ |
3 | | resubcl 10950 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐴 −
1) ∈ ℝ) |
4 | 1, 2, 3 | sylancl 588 |
. . . 4
⊢ (𝜑 → (𝐴 − 1) ∈ ℝ) |
5 | | peano2re 10813 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈
ℝ) |
6 | 1, 5 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐴 + 1) ∈ ℝ) |
7 | | reelprrecn 10629 |
. . . . 5
⊢ ℝ
∈ {ℝ, ℂ} |
8 | | ssid 3989 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
9 | | fncpn 24530 |
. . . . . . . . 9
⊢ (ℂ
⊆ ℂ → (𝓑C𝑛‘ℂ) Fn
ℕ0) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
⊢
(𝓑C𝑛‘ℂ) Fn
ℕ0 |
11 | | 1nn0 11914 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
12 | | fnfvelrn 6848 |
. . . . . . . 8
⊢
(((𝓑C𝑛‘ℂ) Fn ℕ0
∧ 1 ∈ ℕ0) →
((𝓑C𝑛‘ℂ)‘1) ∈ ran
(𝓑C𝑛‘ℂ)) |
13 | 10, 11, 12 | mp2an 690 |
. . . . . . 7
⊢
((𝓑C𝑛‘ℂ)‘1) ∈ ran
(𝓑C𝑛‘ℂ) |
14 | | intss1 4891 |
. . . . . . 7
⊢
(((𝓑C𝑛‘ℂ)‘1) ∈ ran
(𝓑C𝑛‘ℂ) → ∩ ran (𝓑C𝑛‘ℂ)
⊆
((𝓑C𝑛‘ℂ)‘1)) |
15 | 13, 14 | ax-mp 5 |
. . . . . 6
⊢ ∩ ran (𝓑C𝑛‘ℂ)
⊆
((𝓑C𝑛‘ℂ)‘1) |
16 | | aalioulem2.b |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℤ)) |
17 | | plycpn 24878 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℤ)
→ 𝐹 ∈ ∩ ran
(𝓑C𝑛‘ℂ)) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ ∩ ran
(𝓑C𝑛‘ℂ)) |
19 | 15, 18 | sseldi 3965 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈
((𝓑C𝑛‘ℂ)‘1)) |
20 | | cpnres 24534 |
. . . . 5
⊢ ((ℝ
∈ {ℝ, ℂ} ∧ 𝐹 ∈
((𝓑C𝑛‘ℂ)‘1)) → (𝐹 ↾ ℝ) ∈
((𝓑C𝑛‘ℝ)‘1)) |
21 | 7, 19, 20 | sylancr 589 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ ℝ) ∈
((𝓑C𝑛‘ℝ)‘1)) |
22 | | df-ima 5568 |
. . . . 5
⊢ (𝐹 “ ℝ) = ran (𝐹 ↾
ℝ) |
23 | | zssre 11989 |
. . . . . . . . 9
⊢ ℤ
⊆ ℝ |
24 | | ax-resscn 10594 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
25 | | plyss 24789 |
. . . . . . . . 9
⊢ ((ℤ
⊆ ℝ ∧ ℝ ⊆ ℂ) → (Poly‘ℤ)
⊆ (Poly‘ℝ)) |
26 | 23, 24, 25 | mp2an 690 |
. . . . . . . 8
⊢
(Poly‘ℤ) ⊆ (Poly‘ℝ) |
27 | 26, 16 | sseldi 3965 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℝ)) |
28 | | plyreres 24872 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹 ↾
ℝ):ℝ⟶ℝ) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾
ℝ):ℝ⟶ℝ) |
30 | 29 | frnd 6521 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ↾ ℝ) ⊆
ℝ) |
31 | 22, 30 | eqsstrid 4015 |
. . . 4
⊢ (𝜑 → (𝐹 “ ℝ) ⊆
ℝ) |
32 | | iccssre 12819 |
. . . . . . 7
⊢ (((𝐴 − 1) ∈ ℝ ∧
(𝐴 + 1) ∈ ℝ)
→ ((𝐴 −
1)[,](𝐴 + 1)) ⊆
ℝ) |
33 | 4, 6, 32 | syl2anc 586 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ ℝ) |
34 | 33, 24 | sstrdi 3979 |
. . . . 5
⊢ (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ ℂ) |
35 | | plyf 24788 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘ℤ)
→ 𝐹:ℂ⟶ℂ) |
36 | 16, 35 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
37 | 36 | fdmd 6523 |
. . . . 5
⊢ (𝜑 → dom 𝐹 = ℂ) |
38 | 34, 37 | sseqtrrd 4008 |
. . . 4
⊢ (𝜑 → ((𝐴 − 1)[,](𝐴 + 1)) ⊆ dom 𝐹) |
39 | 4, 6, 21, 31, 38 | c1lip3 24596 |
. . 3
⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏)))) |
40 | | simp2 1133 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝑟 ∈ ℝ) |
41 | 40 | recnd 10669 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝑟 ∈ ℂ) |
42 | 1 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐴 ∈ ℝ) |
43 | 42 | 3ad2ant1 1129 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐴 ∈ ℝ) |
44 | 43 | recnd 10669 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐴 ∈ ℂ) |
45 | 41, 44 | abssubd 14813 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘(𝑟 − 𝐴)) = (abs‘(𝐴 − 𝑟))) |
46 | | simp3 1134 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘(𝐴 − 𝑟)) ≤ 1) |
47 | 45, 46 | eqbrtrd 5088 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘(𝑟 − 𝐴)) ≤ 1) |
48 | | 1red 10642 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 1 ∈
ℝ) |
49 | | elicc4abs 14679 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝑟 ∈
ℝ) → (𝑟 ∈
((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝑟 − 𝐴)) ≤ 1)) |
50 | 43, 48, 40, 49 | syl3anc 1367 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝑟 − 𝐴)) ≤ 1)) |
51 | 47, 50 | mpbird 259 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1))) |
52 | 1 | recnd 10669 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℂ) |
53 | 52 | subidd 10985 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 − 𝐴) = 0) |
54 | 53 | fveq2d 6674 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘(𝐴 − 𝐴)) = (abs‘0)) |
55 | | abs0 14645 |
. . . . . . . . . . . . . . 15
⊢
(abs‘0) = 0 |
56 | | 0le1 11163 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
1 |
57 | 55, 56 | eqbrtri 5087 |
. . . . . . . . . . . . . 14
⊢
(abs‘0) ≤ 1 |
58 | 54, 57 | eqbrtrdi 5105 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘(𝐴 − 𝐴)) ≤ 1) |
59 | | 1red 10642 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ) |
60 | | elicc4abs 14679 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝐴 ∈
ℝ) → (𝐴 ∈
((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝐴 − 𝐴)) ≤ 1)) |
61 | 1, 59, 1, 60 | syl3anc 1367 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ↔ (abs‘(𝐴 − 𝐴)) ≤ 1)) |
62 | 58, 61 | mpbird 259 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) |
63 | 62 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) |
64 | 63 | 3ad2ant1 1129 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) |
65 | | fveq2 6670 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑟 → (𝐹‘𝑏) = (𝐹‘𝑟)) |
66 | 65 | oveq2d 7172 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑟 → ((𝐹‘𝑐) − (𝐹‘𝑏)) = ((𝐹‘𝑐) − (𝐹‘𝑟))) |
67 | 66 | fveq2d 6674 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑟 → (abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) = (abs‘((𝐹‘𝑐) − (𝐹‘𝑟)))) |
68 | | oveq2 7164 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑟 → (𝑐 − 𝑏) = (𝑐 − 𝑟)) |
69 | 68 | fveq2d 6674 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑟 → (abs‘(𝑐 − 𝑏)) = (abs‘(𝑐 − 𝑟))) |
70 | 69 | oveq2d 7172 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑟 → (𝑎 · (abs‘(𝑐 − 𝑏))) = (𝑎 · (abs‘(𝑐 − 𝑟)))) |
71 | 67, 70 | breq12d 5079 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑟 → ((abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) ↔ (abs‘((𝐹‘𝑐) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝑐 − 𝑟))))) |
72 | | fveq2 6670 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝐴 → (𝐹‘𝑐) = (𝐹‘𝐴)) |
73 | 72 | fvoveq1d 7178 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝐴 → (abs‘((𝐹‘𝑐) − (𝐹‘𝑟))) = (abs‘((𝐹‘𝐴) − (𝐹‘𝑟)))) |
74 | | fvoveq1 7179 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝐴 → (abs‘(𝑐 − 𝑟)) = (abs‘(𝐴 − 𝑟))) |
75 | 74 | oveq2d 7172 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝐴 → (𝑎 · (abs‘(𝑐 − 𝑟))) = (𝑎 · (abs‘(𝐴 − 𝑟)))) |
76 | 73, 75 | breq12d 5079 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝐴 → ((abs‘((𝐹‘𝑐) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝑐 − 𝑟))) ↔ (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
77 | 71, 76 | rspc2v 3633 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ ((𝐴 − 1)[,](𝐴 + 1)) ∧ 𝐴 ∈ ((𝐴 − 1)[,](𝐴 + 1))) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
78 | 51, 64, 77 | syl2anc 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
79 | | simp1l 1193 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝜑) |
80 | | aalioulem3.e |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘𝐴) = 0) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝐹‘𝐴) = 0) |
82 | | 0cn 10633 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℂ |
83 | 81, 82 | eqeltrdi 2921 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝐹‘𝐴) ∈ ℂ) |
84 | 36 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐹:ℂ⟶ℂ) |
85 | 84 | 3ad2ant1 1129 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → 𝐹:ℂ⟶ℂ) |
86 | 85, 41 | ffvelrnd 6852 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (𝐹‘𝑟) ∈ ℂ) |
87 | 83, 86 | abssubd 14813 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) = (abs‘((𝐹‘𝑟) − (𝐹‘𝐴)))) |
88 | 81 | oveq2d 7172 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((𝐹‘𝑟) − (𝐹‘𝐴)) = ((𝐹‘𝑟) − 0)) |
89 | 86 | subid1d 10986 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((𝐹‘𝑟) − 0) = (𝐹‘𝑟)) |
90 | 88, 89 | eqtrd 2856 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((𝐹‘𝑟) − (𝐹‘𝐴)) = (𝐹‘𝑟)) |
91 | 90 | fveq2d 6674 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘((𝐹‘𝑟) − (𝐹‘𝐴))) = (abs‘(𝐹‘𝑟))) |
92 | 87, 91 | eqtrd 2856 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) = (abs‘(𝐹‘𝑟))) |
93 | 92 | breq1d 5076 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → ((abs‘((𝐹‘𝐴) − (𝐹‘𝑟))) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))) ↔ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
94 | 78, 93 | sylibd 241 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ ∧ (abs‘(𝐴 − 𝑟)) ≤ 1) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
95 | 94 | 3exp 1115 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑟 ∈ ℝ → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))))) |
96 | 95 | com34 91 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑟 ∈ ℝ → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))))) |
97 | 96 | com23 86 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → (𝑟 ∈ ℝ → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))))) |
98 | 97 | ralrimdv 3188 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))))) |
99 | 98 | reximdva 3274 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ ℝ ∀𝑏 ∈ ((𝐴 − 1)[,](𝐴 + 1))∀𝑐 ∈ ((𝐴 − 1)[,](𝐴 + 1))(abs‘((𝐹‘𝑐) − (𝐹‘𝑏))) ≤ (𝑎 · (abs‘(𝑐 − 𝑏))) → ∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))))) |
100 | 39, 99 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) |
101 | | 1rp 12394 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
102 | 101 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑎 = 0) → 1 ∈
ℝ+) |
103 | | recn 10627 |
. . . . . . . 8
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℂ) |
104 | 103 | adantl 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℂ) |
105 | | neqne 3024 |
. . . . . . 7
⊢ (¬
𝑎 = 0 → 𝑎 ≠ 0) |
106 | | absrpcl 14648 |
. . . . . . 7
⊢ ((𝑎 ∈ ℂ ∧ 𝑎 ≠ 0) → (abs‘𝑎) ∈
ℝ+) |
107 | 104, 105,
106 | syl2an 597 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 𝑎 = 0) → (abs‘𝑎) ∈
ℝ+) |
108 | 107 | rpreccld 12442 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ¬ 𝑎 = 0) → (1 /
(abs‘𝑎)) ∈
ℝ+) |
109 | 102, 108 | ifclda 4501 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → if(𝑎 = 0, 1, (1 / (abs‘𝑎))) ∈
ℝ+) |
110 | | eqid 2821 |
. . . . . . . . 9
⊢ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) |
111 | | eqif 4507 |
. . . . . . . . 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‘𝑎))))) |
112 | 110, 111 | mpbi 232 |
. . . . . . . 8
⊢ ((𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1) ∨ (¬ 𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)))) |
113 | | simplrr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) |
114 | | oveq1 7163 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 0 → (𝑎 · (abs‘(𝐴 − 𝑟))) = (0 · (abs‘(𝐴 − 𝑟)))) |
115 | 114 | adantl 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝑎 · (abs‘(𝐴 − 𝑟))) = (0 · (abs‘(𝐴 − 𝑟)))) |
116 | 1 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝐴 ∈ ℝ) |
117 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑟 ∈ ℝ) |
118 | 116, 117 | resubcld 11068 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝐴 − 𝑟) ∈ ℝ) |
119 | 118 | recnd 10669 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝐴 − 𝑟) ∈ ℂ) |
120 | 119 | abscld 14796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐴 − 𝑟)) ∈ ℝ) |
121 | 120 | recnd 10669 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐴 − 𝑟)) ∈ ℂ) |
122 | 121 | adantr 483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐴 − 𝑟)) ∈ ℂ) |
123 | 122 | mul02d 10838 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (0 · (abs‘(𝐴 − 𝑟))) = 0) |
124 | 115, 123 | eqtrd 2856 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝑎 · (abs‘(𝐴 − 𝑟))) = 0) |
125 | 113, 124 | breqtrd 5092 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) ≤ 0) |
126 | 36 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝐹:ℂ⟶ℂ) |
127 | 117 | recnd 10669 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑟 ∈ ℂ) |
128 | 126, 127 | ffvelrnd 6852 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝐹‘𝑟) ∈ ℂ) |
129 | 128 | adantr 483 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝐹‘𝑟) ∈ ℂ) |
130 | 129 | absge0d 14804 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → 0 ≤ (abs‘(𝐹‘𝑟))) |
131 | 128 | abscld 14796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐹‘𝑟)) ∈ ℝ) |
132 | 131 | adantr 483 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) ∈ ℝ) |
133 | | 0re 10643 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
134 | | letri3 10726 |
. . . . . . . . . . . . . . . 16
⊢
(((abs‘(𝐹‘𝑟)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((abs‘(𝐹‘𝑟)) = 0 ↔ ((abs‘(𝐹‘𝑟)) ≤ 0 ∧ 0 ≤ (abs‘(𝐹‘𝑟))))) |
135 | 132, 133,
134 | sylancl 588 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → ((abs‘(𝐹‘𝑟)) = 0 ↔ ((abs‘(𝐹‘𝑟)) ≤ 0 ∧ 0 ≤ (abs‘(𝐹‘𝑟))))) |
136 | 125, 130,
135 | mpbir2and 711 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (abs‘(𝐹‘𝑟)) = 0) |
137 | 136 | oveq2d 7172 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹‘𝑟))) = (1 · 0)) |
138 | | ax-1cn 10595 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
139 | 138 | mul01i 10830 |
. . . . . . . . . . . . 13
⊢ (1
· 0) = 0 |
140 | 137, 139 | syl6eq 2872 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹‘𝑟))) = 0) |
141 | 119 | adantr 483 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (𝐴 − 𝑟) ∈ ℂ) |
142 | 141 | absge0d 14804 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → 0 ≤ (abs‘(𝐴 − 𝑟))) |
143 | 140, 142 | eqbrtrd 5088 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (1 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) |
144 | | oveq1 7163 |
. . . . . . . . . . . 12
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) = (1 · (abs‘(𝐹‘𝑟)))) |
145 | 144 | breq1d 5076 |
. . . . . . . . . . 11
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → ((if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)) ↔ (1 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
146 | 143, 145 | syl5ibrcom 249 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 = 0) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
147 | 146 | expimpd 456 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → ((𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = 1) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
148 | | df-ne 3017 |
. . . . . . . . . . . 12
⊢ (𝑎 ≠ 0 ↔ ¬ 𝑎 = 0) |
149 | 131 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹‘𝑟)) ∈ ℝ) |
150 | 149 | recnd 10669 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹‘𝑟)) ∈ ℂ) |
151 | | simpllr 774 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → 𝑎 ∈ ℝ) |
152 | 151 | recnd 10669 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → 𝑎 ∈ ℂ) |
153 | 152, 106 | sylancom 590 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘𝑎) ∈
ℝ+) |
154 | 153 | rpcnne0d 12441 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘𝑎) ∈ ℂ ∧
(abs‘𝑎) ≠
0)) |
155 | | divrec2 11315 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘(𝐹‘𝑟)) ∈ ℂ ∧ (abs‘𝑎) ∈ ℂ ∧
(abs‘𝑎) ≠ 0)
→ ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) |
156 | 155 | 3expb 1116 |
. . . . . . . . . . . . . 14
⊢
(((abs‘(𝐹‘𝑟)) ∈ ℂ ∧ ((abs‘𝑎) ∈ ℂ ∧
(abs‘𝑎) ≠ 0))
→ ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) |
157 | 150, 154,
156 | syl2anc 586 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) |
158 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑎 ∈ ℝ) |
159 | 158, 120 | remulcld 10671 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝑎 · (abs‘(𝐴 − 𝑟))) ∈ ℝ) |
160 | 158 | recnd 10669 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑎 ∈ ℂ) |
161 | 160 | abscld 14796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘𝑎) ∈ ℝ) |
162 | 161, 120 | remulcld 10671 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → ((abs‘𝑎) · (abs‘(𝐴 − 𝑟))) ∈ ℝ) |
163 | | simprr 771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) |
164 | 119 | absge0d 14804 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 0 ≤ (abs‘(𝐴 − 𝑟))) |
165 | | leabs 14659 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ ℝ → 𝑎 ≤ (abs‘𝑎)) |
166 | 165 | ad2antlr 725 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → 𝑎 ≤ (abs‘𝑎)) |
167 | 158, 161,
120, 164, 166 | lemul1ad 11579 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (𝑎 · (abs‘(𝐴 − 𝑟))) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟)))) |
168 | 131, 159,
162, 163, 167 | letrd 10797 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (abs‘(𝐹‘𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟)))) |
169 | 168 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐹‘𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟)))) |
170 | 120 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (abs‘(𝐴 − 𝑟)) ∈ ℝ) |
171 | 149, 170,
153 | ledivmuld 12485 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → (((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) ≤ (abs‘(𝐴 − 𝑟)) ↔ (abs‘(𝐹‘𝑟)) ≤ ((abs‘𝑎) · (abs‘(𝐴 − 𝑟))))) |
172 | 169, 171 | mpbird 259 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((abs‘(𝐹‘𝑟)) / (abs‘𝑎)) ≤ (abs‘(𝐴 − 𝑟))) |
173 | 157, 172 | eqbrtrrd 5090 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ 𝑎 ≠ 0) → ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) |
174 | 148, 173 | sylan2br 596 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ ¬ 𝑎 = 0) → ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) |
175 | | oveq1 7163 |
. . . . . . . . . . . 12
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) = ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟)))) |
176 | 175 | breq1d 5076 |
. . . . . . . . . . 11
⊢ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → ((if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)) ↔ ((1 / (abs‘𝑎)) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
177 | 174, 176 | syl5ibrcom 249 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) ∧ ¬ 𝑎 = 0) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎)) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
178 | 177 | expimpd 456 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → ((¬ 𝑎 = 0 ∧ if(𝑎 = 0, 1, (1 / (abs‘𝑎))) = (1 / (abs‘𝑎))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
179 | 147, 178 | jaod 855 |
. . . . . . . 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‘(𝐴 − 𝑟)))) |
180 | 112, 179 | mpi 20 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) |
181 | 180 | expr 459 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ) → ((abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟))) → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
182 | 181 | imim2d 57 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑟 ∈ ℝ) → (((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
183 | 182 | ralimdva 3177 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 →
(abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
184 | | oveq1 7163 |
. . . . . . . 8
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (𝑥 · (abs‘(𝐹‘𝑟))) = (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟)))) |
185 | 184 | breq1d 5076 |
. . . . . . 7
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → ((𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)) ↔ (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
186 | 185 | imbi2d 343 |
. . . . . 6
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (((abs‘(𝐴 − 𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) ↔ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
187 | 186 | ralbidv 3197 |
. . . . 5
⊢ (𝑥 = if(𝑎 = 0, 1, (1 / (abs‘𝑎))) → (∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))) ↔ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
188 | 187 | rspcev 3623 |
. . . 4
⊢
((if(𝑎 = 0, 1, (1 /
(abs‘𝑎))) ∈
ℝ+ ∧ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (if(𝑎 = 0, 1, (1 / (abs‘𝑎))) · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |
189 | 109, 183,
188 | syl6an 682 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 →
(abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
190 | 189 | rexlimdva 3284 |
. 2
⊢ (𝜑 → (∃𝑎 ∈ ℝ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (abs‘(𝐹‘𝑟)) ≤ (𝑎 · (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))) |
191 | 100, 190 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ
((abs‘(𝐴 −
𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) |