# Metamath Proof Explorer

## Theorem aalioulem3

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 15-Nov-2014)

Ref Expression
Hypotheses aalioulem2.a ${⊢}{N}=\mathrm{deg}\left({F}\right)$
aalioulem2.b ${⊢}{\phi }\to {F}\in \mathrm{Poly}\left(ℤ\right)$
aalioulem2.c ${⊢}{\phi }\to {N}\in ℕ$
aalioulem2.d ${⊢}{\phi }\to {A}\in ℝ$
aalioulem3.e ${⊢}{\phi }\to {F}\left({A}\right)=0$
Assertion aalioulem3 ${⊢}{\phi }\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\left|{A}-{r}\right|\le 1\to {x}\left|{F}\left({r}\right)\right|\le \left|{A}-{r}\right|\right)$

### Proof

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