| Step |
Hyp |
Ref |
Expression |
| 1 |
|
aalioulem2.a |
⊢ 𝑁 = ( deg ‘ 𝐹 ) |
| 2 |
|
aalioulem2.b |
⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℤ ) ) |
| 3 |
|
aalioulem2.c |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
| 4 |
|
aalioulem2.d |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
| 5 |
|
aalioulem3.e |
⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 ) |
| 6 |
|
1re |
⊢ 1 ∈ ℝ |
| 7 |
|
resubcl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐴 − 1 ) ∈ ℝ ) |
| 8 |
4 6 7
|
sylancl |
⊢ ( 𝜑 → ( 𝐴 − 1 ) ∈ ℝ ) |
| 9 |
|
peano2re |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ ) |
| 10 |
4 9
|
syl |
⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℝ ) |
| 11 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
| 12 |
|
ssid |
⊢ ℂ ⊆ ℂ |
| 13 |
|
fncpn |
⊢ ( ℂ ⊆ ℂ → ( 𝓑C𝑛 ‘ ℂ ) Fn ℕ0 ) |
| 14 |
12 13
|
ax-mp |
⊢ ( 𝓑C𝑛 ‘ ℂ ) Fn ℕ0 |
| 15 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
| 16 |
|
fnfvelrn |
⊢ ( ( ( 𝓑C𝑛 ‘ ℂ ) Fn ℕ0 ∧ 1 ∈ ℕ0 ) → ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) ∈ ran ( 𝓑C𝑛 ‘ ℂ ) ) |
| 17 |
14 15 16
|
mp2an |
⊢ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) ∈ ran ( 𝓑C𝑛 ‘ ℂ ) |
| 18 |
|
intss1 |
⊢ ( ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) ∈ ran ( 𝓑C𝑛 ‘ ℂ ) → ∩ ran ( 𝓑C𝑛 ‘ ℂ ) ⊆ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) ) |
| 19 |
17 18
|
ax-mp |
⊢ ∩ ran ( 𝓑C𝑛 ‘ ℂ ) ⊆ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) |
| 20 |
|
plycpn |
⊢ ( 𝐹 ∈ ( Poly ‘ ℤ ) → 𝐹 ∈ ∩ ran ( 𝓑C𝑛 ‘ ℂ ) ) |
| 21 |
2 20
|
syl |
⊢ ( 𝜑 → 𝐹 ∈ ∩ ran ( 𝓑C𝑛 ‘ ℂ ) ) |
| 22 |
19 21
|
sselid |
⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) ) |
| 23 |
|
cpnres |
⊢ ( ( ℝ ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℂ ) ‘ 1 ) ) → ( 𝐹 ↾ ℝ ) ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) ) |
| 24 |
11 22 23
|
sylancr |
⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) ) |
| 25 |
|
df-ima |
⊢ ( 𝐹 “ ℝ ) = ran ( 𝐹 ↾ ℝ ) |
| 26 |
|
zssre |
⊢ ℤ ⊆ ℝ |
| 27 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
| 28 |
|
plyss |
⊢ ( ( ℤ ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( Poly ‘ ℤ ) ⊆ ( Poly ‘ ℝ ) ) |
| 29 |
26 27 28
|
mp2an |
⊢ ( Poly ‘ ℤ ) ⊆ ( Poly ‘ ℝ ) |
| 30 |
29 2
|
sselid |
⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℝ ) ) |
| 31 |
|
plyreres |
⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℝ ) |
| 32 |
30 31
|
syl |
⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) : ℝ ⟶ ℝ ) |
| 33 |
32
|
frnd |
⊢ ( 𝜑 → ran ( 𝐹 ↾ ℝ ) ⊆ ℝ ) |
| 34 |
25 33
|
eqsstrid |
⊢ ( 𝜑 → ( 𝐹 “ ℝ ) ⊆ ℝ ) |
| 35 |
|
iccssre |
⊢ ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ) → ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ⊆ ℝ ) |
| 36 |
8 10 35
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ⊆ ℝ ) |
| 37 |
36 27
|
sstrdi |
⊢ ( 𝜑 → ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ⊆ ℂ ) |
| 38 |
|
plyf |
⊢ ( 𝐹 ∈ ( Poly ‘ ℤ ) → 𝐹 : ℂ ⟶ ℂ ) |
| 39 |
2 38
|
syl |
⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ ) |
| 40 |
39
|
fdmd |
⊢ ( 𝜑 → dom 𝐹 = ℂ ) |
| 41 |
37 40
|
sseqtrrd |
⊢ ( 𝜑 → ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ⊆ dom 𝐹 ) |
| 42 |
8 10 24 34 41
|
c1lip3 |
⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) ) |
| 43 |
|
simp2 |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝑟 ∈ ℝ ) |
| 44 |
43
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝑟 ∈ ℂ ) |
| 45 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐴 ∈ ℝ ) |
| 46 |
45
|
3ad2ant1 |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝐴 ∈ ℝ ) |
| 47 |
46
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝐴 ∈ ℂ ) |
| 48 |
44 47
|
abssubd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( 𝑟 − 𝐴 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
| 49 |
|
simp3 |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) |
| 50 |
48 49
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( 𝑟 − 𝐴 ) ) ≤ 1 ) |
| 51 |
|
1red |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 1 ∈ ℝ ) |
| 52 |
|
elicc4abs |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝑟 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ↔ ( abs ‘ ( 𝑟 − 𝐴 ) ) ≤ 1 ) ) |
| 53 |
46 51 43 52
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( 𝑟 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ↔ ( abs ‘ ( 𝑟 − 𝐴 ) ) ≤ 1 ) ) |
| 54 |
50 53
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝑟 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ) |
| 55 |
4
|
recnd |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
| 56 |
55
|
subidd |
⊢ ( 𝜑 → ( 𝐴 − 𝐴 ) = 0 ) |
| 57 |
56
|
fveq2d |
⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐴 ) ) = ( abs ‘ 0 ) ) |
| 58 |
|
abs0 |
⊢ ( abs ‘ 0 ) = 0 |
| 59 |
|
0le1 |
⊢ 0 ≤ 1 |
| 60 |
58 59
|
eqbrtri |
⊢ ( abs ‘ 0 ) ≤ 1 |
| 61 |
57 60
|
eqbrtrdi |
⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐴 ) ) ≤ 1 ) |
| 62 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
| 63 |
|
elicc4abs |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ↔ ( abs ‘ ( 𝐴 − 𝐴 ) ) ≤ 1 ) ) |
| 64 |
4 62 4 63
|
syl3anc |
⊢ ( 𝜑 → ( 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ↔ ( abs ‘ ( 𝐴 − 𝐴 ) ) ≤ 1 ) ) |
| 65 |
61 64
|
mpbird |
⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ) |
| 66 |
65
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ) |
| 67 |
66
|
3ad2ant1 |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ) |
| 68 |
|
fveq2 |
⊢ ( 𝑏 = 𝑟 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑟 ) ) |
| 69 |
68
|
oveq2d |
⊢ ( 𝑏 = 𝑟 → ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑟 ) ) ) |
| 70 |
69
|
fveq2d |
⊢ ( 𝑏 = 𝑟 → ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑟 ) ) ) ) |
| 71 |
|
oveq2 |
⊢ ( 𝑏 = 𝑟 → ( 𝑐 − 𝑏 ) = ( 𝑐 − 𝑟 ) ) |
| 72 |
71
|
fveq2d |
⊢ ( 𝑏 = 𝑟 → ( abs ‘ ( 𝑐 − 𝑏 ) ) = ( abs ‘ ( 𝑐 − 𝑟 ) ) ) |
| 73 |
72
|
oveq2d |
⊢ ( 𝑏 = 𝑟 → ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) = ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑟 ) ) ) ) |
| 74 |
70 73
|
breq12d |
⊢ ( 𝑏 = 𝑟 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑟 ) ) ) ) ) |
| 75 |
|
fveq2 |
⊢ ( 𝑐 = 𝐴 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝐴 ) ) |
| 76 |
75
|
fvoveq1d |
⊢ ( 𝑐 = 𝐴 → ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑟 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) ) |
| 77 |
|
fvoveq1 |
⊢ ( 𝑐 = 𝐴 → ( abs ‘ ( 𝑐 − 𝑟 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
| 78 |
77
|
oveq2d |
⊢ ( 𝑐 = 𝐴 → ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑟 ) ) ) = ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 79 |
76 78
|
breq12d |
⊢ ( 𝑐 = 𝐴 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑟 ) ) ) ↔ ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 80 |
74 79
|
rspc2v |
⊢ ( ( 𝑟 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∧ 𝐴 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ) → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 81 |
54 67 80
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 82 |
|
simp1l |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝜑 ) |
| 83 |
82 5
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( 𝐹 ‘ 𝐴 ) = 0 ) |
| 84 |
|
0cn |
⊢ 0 ∈ ℂ |
| 85 |
83 84
|
eqeltrdi |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( 𝐹 ‘ 𝐴 ) ∈ ℂ ) |
| 86 |
39
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 : ℂ ⟶ ℂ ) |
| 87 |
86
|
3ad2ant1 |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → 𝐹 : ℂ ⟶ ℂ ) |
| 88 |
87 44
|
ffvelcdmd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( 𝐹 ‘ 𝑟 ) ∈ ℂ ) |
| 89 |
85 88
|
abssubd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑟 ) − ( 𝐹 ‘ 𝐴 ) ) ) ) |
| 90 |
83
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ( 𝐹 ‘ 𝑟 ) − ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝑟 ) − 0 ) ) |
| 91 |
88
|
subid1d |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ( 𝐹 ‘ 𝑟 ) − 0 ) = ( 𝐹 ‘ 𝑟 ) ) |
| 92 |
90 91
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ( 𝐹 ‘ 𝑟 ) − ( 𝐹 ‘ 𝐴 ) ) = ( 𝐹 ‘ 𝑟 ) ) |
| 93 |
92
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑟 ) − ( 𝐹 ‘ 𝐴 ) ) ) = ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) |
| 94 |
89 93
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) = ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) |
| 95 |
94
|
breq1d |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 96 |
81 95
|
sylibd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 ) → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 97 |
96
|
3exp |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑟 ∈ ℝ → ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ) ) |
| 98 |
97
|
com34 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑟 ∈ ℝ → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ) ) |
| 99 |
98
|
com23 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ( 𝑟 ∈ ℝ → ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ) ) |
| 100 |
99
|
ralrimdv |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ) |
| 101 |
100
|
reximdva |
⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ∀ 𝑐 ∈ ( ( 𝐴 − 1 ) [,] ( 𝐴 + 1 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑐 ) − ( 𝐹 ‘ 𝑏 ) ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝑐 − 𝑏 ) ) ) → ∃ 𝑎 ∈ ℝ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ) |
| 102 |
42 101
|
mpd |
⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 103 |
|
1rp |
⊢ 1 ∈ ℝ+ |
| 104 |
103
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑎 = 0 ) → 1 ∈ ℝ+ ) |
| 105 |
|
recn |
⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℂ ) |
| 106 |
105
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℂ ) |
| 107 |
|
neqne |
⊢ ( ¬ 𝑎 = 0 → 𝑎 ≠ 0 ) |
| 108 |
|
absrpcl |
⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) → ( abs ‘ 𝑎 ) ∈ ℝ+ ) |
| 109 |
106 107 108
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝑎 = 0 ) → ( abs ‘ 𝑎 ) ∈ ℝ+ ) |
| 110 |
109
|
rpreccld |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ¬ 𝑎 = 0 ) → ( 1 / ( abs ‘ 𝑎 ) ) ∈ ℝ+ ) |
| 111 |
104 110
|
ifclda |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) ∈ ℝ+ ) |
| 112 |
|
eqid |
⊢ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) |
| 113 |
|
eqif |
⊢ ( 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 ‘ 𝑎 ) ) ) ) ) |
| 114 |
112 113
|
mpbi |
⊢ ( ( 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 ) ∨ ( ¬ 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) ) ) |
| 115 |
|
simplrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 116 |
|
oveq1 |
⊢ ( 𝑎 = 0 → ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) = ( 0 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 117 |
116
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) = ( 0 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 118 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝐴 ∈ ℝ ) |
| 119 |
|
simprl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝑟 ∈ ℝ ) |
| 120 |
118 119
|
resubcld |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( 𝐴 − 𝑟 ) ∈ ℝ ) |
| 121 |
120
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( 𝐴 − 𝑟 ) ∈ ℂ ) |
| 122 |
121
|
abscld |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ℝ ) |
| 123 |
122
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ℂ ) |
| 124 |
123
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ℂ ) |
| 125 |
124
|
mul02d |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 0 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) = 0 ) |
| 126 |
117 125
|
eqtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) = 0 ) |
| 127 |
115 126
|
breqtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ 0 ) |
| 128 |
39
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝐹 : ℂ ⟶ ℂ ) |
| 129 |
119
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝑟 ∈ ℂ ) |
| 130 |
128 129
|
ffvelcdmd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( 𝐹 ‘ 𝑟 ) ∈ ℂ ) |
| 131 |
130
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 𝐹 ‘ 𝑟 ) ∈ ℂ ) |
| 132 |
131
|
absge0d |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) |
| 133 |
130
|
abscld |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℝ ) |
| 134 |
133
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℝ ) |
| 135 |
|
0re |
⊢ 0 ∈ ℝ |
| 136 |
|
letri3 |
⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) = 0 ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ 0 ∧ 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ) ) |
| 137 |
134 135 136
|
sylancl |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) = 0 ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ 0 ∧ 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ) ) |
| 138 |
127 132 137
|
mpbir2and |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) = 0 ) |
| 139 |
138
|
oveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) = ( 1 · 0 ) ) |
| 140 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
| 141 |
140
|
mul01i |
⊢ ( 1 · 0 ) = 0 |
| 142 |
139 141
|
eqtrdi |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) = 0 ) |
| 143 |
121
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 𝐴 − 𝑟 ) ∈ ℂ ) |
| 144 |
143
|
absge0d |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → 0 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
| 145 |
142 144
|
eqbrtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
| 146 |
|
oveq1 |
⊢ ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) = ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ) |
| 147 |
146
|
breq1d |
⊢ ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 → ( ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ↔ ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 148 |
145 147
|
syl5ibrcom |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 = 0 ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 149 |
148
|
expimpd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( ( 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 150 |
|
df-ne |
⊢ ( 𝑎 ≠ 0 ↔ ¬ 𝑎 = 0 ) |
| 151 |
133
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℝ ) |
| 152 |
151
|
recnd |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℂ ) |
| 153 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → 𝑎 ∈ ℝ ) |
| 154 |
153
|
recnd |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → 𝑎 ∈ ℂ ) |
| 155 |
154 108
|
sylancom |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ 𝑎 ) ∈ ℝ+ ) |
| 156 |
155
|
rpcnne0d |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( ( abs ‘ 𝑎 ) ∈ ℂ ∧ ( abs ‘ 𝑎 ) ≠ 0 ) ) |
| 157 |
|
divrec2 |
⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ℂ ∧ ( abs ‘ 𝑎 ) ≠ 0 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) / ( abs ‘ 𝑎 ) ) = ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ) |
| 158 |
157
|
3expb |
⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ∈ ℂ ∧ ( ( abs ‘ 𝑎 ) ∈ ℂ ∧ ( abs ‘ 𝑎 ) ≠ 0 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) / ( abs ‘ 𝑎 ) ) = ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ) |
| 159 |
152 156 158
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) / ( abs ‘ 𝑎 ) ) = ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ) |
| 160 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝑎 ∈ ℝ ) |
| 161 |
160 122
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ∈ ℝ ) |
| 162 |
160
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝑎 ∈ ℂ ) |
| 163 |
162
|
abscld |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ 𝑎 ) ∈ ℝ ) |
| 164 |
163 122
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ∈ ℝ ) |
| 165 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 166 |
121
|
absge0d |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 0 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
| 167 |
|
leabs |
⊢ ( 𝑎 ∈ ℝ → 𝑎 ≤ ( abs ‘ 𝑎 ) ) |
| 168 |
167
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → 𝑎 ≤ ( abs ‘ 𝑎 ) ) |
| 169 |
160 163 122 166 168
|
lemul1ad |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ≤ ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 170 |
133 161 164 165 169
|
letrd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 171 |
170
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 172 |
122
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ℝ ) |
| 173 |
151 172 155
|
ledivmuld |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) / ( abs ‘ 𝑎 ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( ( abs ‘ 𝑎 ) · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 174 |
171 173
|
mpbird |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) / ( abs ‘ 𝑎 ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
| 175 |
159 174
|
eqbrtrrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ 𝑎 ≠ 0 ) → ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
| 176 |
150 175
|
sylan2br |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ ¬ 𝑎 = 0 ) → ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
| 177 |
|
oveq1 |
⊢ ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) = ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ) |
| 178 |
177
|
breq1d |
⊢ ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) → ( ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ↔ ( ( 1 / ( abs ‘ 𝑎 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 179 |
176 178
|
syl5ibrcom |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ∧ ¬ 𝑎 = 0 ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 180 |
179
|
expimpd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( ( ¬ 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 181 |
149 180
|
jaod |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( ( ( 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = 1 ) ∨ ( ¬ 𝑎 = 0 ∧ if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) = ( 1 / ( abs ‘ 𝑎 ) ) ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 182 |
114 181
|
mpi |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑟 ∈ ℝ ∧ ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
| 183 |
182
|
expr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 184 |
183
|
imim2d |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑟 ∈ ℝ ) → ( ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 185 |
184
|
ralimdva |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 186 |
|
oveq1 |
⊢ ( 𝑥 = if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) = ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ) |
| 187 |
186
|
breq1d |
⊢ ( 𝑥 = if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) → ( ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ↔ ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 188 |
187
|
imbi2d |
⊢ ( 𝑥 = if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) → ( ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 189 |
188
|
ralbidv |
⊢ ( 𝑥 = if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) → ( ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 190 |
189
|
rspcev |
⊢ ( ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( if ( 𝑎 = 0 , 1 , ( 1 / ( abs ‘ 𝑎 ) ) ) · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
| 191 |
111 185 190
|
syl6an |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 192 |
191
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℝ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ≤ ( 𝑎 · ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
| 193 |
102 192
|
mpd |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑟 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |