# Metamath Proof Explorer

## Theorem aalioulem2

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 15-Nov-2014) (Proof shortened by AV, 28-Sep-2020)

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 ℝ$
Assertion aalioulem2 ${⊢}{\phi }\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{N}}}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\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 1rp ${⊢}1\in {ℝ}^{+}$
6 snssi ${⊢}1\in {ℝ}^{+}\to \left\{1\right\}\subseteq {ℝ}^{+}$
7 5 6 ax-mp ${⊢}\left\{1\right\}\subseteq {ℝ}^{+}$
8 ssrab2 ${⊢}\left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\subseteq {ℝ}^{+}$
9 7 8 unssi ${⊢}\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\subseteq {ℝ}^{+}$
10 ltso ${⊢}<\mathrm{Or}ℝ$
11 10 a1i ${⊢}{\phi }\to <\mathrm{Or}ℝ$
12 snfi ${⊢}\left\{1\right\}\in \mathrm{Fin}$
13 3 nnne0d ${⊢}{\phi }\to {N}\ne 0$
14 1 eqcomi ${⊢}\mathrm{deg}\left({F}\right)={N}$
15 dgr0 ${⊢}\mathrm{deg}\left({0}_{𝑝}\right)=0$
16 13 14 15 3netr4g ${⊢}{\phi }\to \mathrm{deg}\left({F}\right)\ne \mathrm{deg}\left({0}_{𝑝}\right)$
17 fveq2 ${⊢}{F}={0}_{𝑝}\to \mathrm{deg}\left({F}\right)=\mathrm{deg}\left({0}_{𝑝}\right)$
18 17 necon3i ${⊢}\mathrm{deg}\left({F}\right)\ne \mathrm{deg}\left({0}_{𝑝}\right)\to {F}\ne {0}_{𝑝}$
19 16 18 syl ${⊢}{\phi }\to {F}\ne {0}_{𝑝}$
20 eqid ${⊢}{{F}}^{-1}\left[\left\{0\right\}\right]={{F}}^{-1}\left[\left\{0\right\}\right]$
21 20 fta1 ${⊢}\left({F}\in \mathrm{Poly}\left(ℤ\right)\wedge {F}\ne {0}_{𝑝}\right)\to \left({{F}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{F}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({F}\right)\right)$
22 2 19 21 syl2anc ${⊢}{\phi }\to \left({{F}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{{F}}^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left({F}\right)\right)$
23 22 simpld ${⊢}{\phi }\to {{F}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}$
24 abrexfi ${⊢}{{F}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\to \left\{{a}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\in \mathrm{Fin}$
25 23 24 syl ${⊢}{\phi }\to \left\{{a}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\in \mathrm{Fin}$
26 rabssab ${⊢}\left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\subseteq \left\{{a}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}$
27 ssfi ${⊢}\left(\left\{{a}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\in \mathrm{Fin}\wedge \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\subseteq \left\{{a}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)\to \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\in \mathrm{Fin}$
28 25 26 27 sylancl ${⊢}{\phi }\to \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\in \mathrm{Fin}$
29 unfi ${⊢}\left(\left\{1\right\}\in \mathrm{Fin}\wedge \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\in \mathrm{Fin}\right)\to \left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\in \mathrm{Fin}$
30 12 28 29 sylancr ${⊢}{\phi }\to \left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\in \mathrm{Fin}$
31 1ex ${⊢}1\in \mathrm{V}$
32 31 snid ${⊢}1\in \left\{1\right\}$
33 elun1 ${⊢}1\in \left\{1\right\}\to 1\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)$
34 ne0i ${⊢}1\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)\to \left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\ne \varnothing$
35 32 33 34 mp2b ${⊢}\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\ne \varnothing$
36 35 a1i ${⊢}{\phi }\to \left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\ne \varnothing$
37 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
38 9 37 sstri ${⊢}\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\subseteq ℝ$
39 38 a1i ${⊢}{\phi }\to \left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\subseteq ℝ$
40 fiinfcl ${⊢}\left(<\mathrm{Or}ℝ\wedge \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\in \mathrm{Fin}\wedge \left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\ne \varnothing \wedge \left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\subseteq ℝ\right)\right)\to sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)$
41 11 30 36 39 40 syl13anc ${⊢}{\phi }\to sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)$
42 9 41 sseldi ${⊢}{\phi }\to sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\in {ℝ}^{+}$
43 0re ${⊢}0\in ℝ$
44 rpge0 ${⊢}{d}\in {ℝ}^{+}\to 0\le {d}$
45 44 rgen ${⊢}\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}0\le {d}$
46 breq1 ${⊢}{c}=0\to \left({c}\le {d}↔0\le {d}\right)$
47 46 ralbidv ${⊢}{c}=0\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{c}\le {d}↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}0\le {d}\right)$
48 47 rspcev ${⊢}\left(0\in ℝ\wedge \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}0\le {d}\right)\to \exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{c}\le {d}$
49 43 45 48 mp2an ${⊢}\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{c}\le {d}$
50 ssralv ${⊢}\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\subseteq {ℝ}^{+}\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{c}\le {d}\to \forall {d}\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}{c}\le {d}\right)$
51 9 50 ax-mp ${⊢}\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{c}\le {d}\to \forall {d}\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}{c}\le {d}$
52 51 reximi ${⊢}\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{c}\le {d}\to \exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {d}\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}{c}\le {d}$
53 49 52 ax-mp ${⊢}\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {d}\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}{c}\le {d}$
54 eqeq1 ${⊢}{a}=\left|{A}-{r}\right|\to \left({a}=\left|{A}-{b}\right|↔\left|{A}-{r}\right|=\left|{A}-{b}\right|\right)$
55 54 rexbidv ${⊢}{a}=\left|{A}-{r}\right|\to \left(\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|↔\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}\left|{A}-{r}\right|=\left|{A}-{b}\right|\right)$
56 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to {A}\in ℝ$
57 simplr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to {r}\in ℝ$
58 56 57 resubcld ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to {A}-{r}\in ℝ$
59 58 recnd ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to {A}-{r}\in ℂ$
60 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge {F}\left({r}\right)=0\right)\to {A}\in ℝ$
61 60 recnd ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge {F}\left({r}\right)=0\right)\to {A}\in ℂ$
62 simplr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge {F}\left({r}\right)=0\right)\to {r}\in ℝ$
63 62 recnd ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge {F}\left({r}\right)=0\right)\to {r}\in ℂ$
64 61 63 subeq0ad ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge {F}\left({r}\right)=0\right)\to \left({A}-{r}=0↔{A}={r}\right)$
65 64 necon3abid ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge {F}\left({r}\right)=0\right)\to \left({A}-{r}\ne 0↔¬{A}={r}\right)$
66 65 biimprd ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge {F}\left({r}\right)=0\right)\to \left(¬{A}={r}\to {A}-{r}\ne 0\right)$
67 66 impr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to {A}-{r}\ne 0$
68 59 67 absrpcld ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to \left|{A}-{r}\right|\in {ℝ}^{+}$
69 57 recnd ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to {r}\in ℂ$
70 simprl ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to {F}\left({r}\right)=0$
71 plyf ${⊢}{F}\in \mathrm{Poly}\left(ℤ\right)\to {F}:ℂ⟶ℂ$
72 2 71 syl ${⊢}{\phi }\to {F}:ℂ⟶ℂ$
73 72 ffnd ${⊢}{\phi }\to {F}Fnℂ$
74 73 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to {F}Fnℂ$
75 fniniseg ${⊢}{F}Fnℂ\to \left({r}\in {{F}}^{-1}\left[\left\{0\right\}\right]↔\left({r}\in ℂ\wedge {F}\left({r}\right)=0\right)\right)$
76 74 75 syl ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to \left({r}\in {{F}}^{-1}\left[\left\{0\right\}\right]↔\left({r}\in ℂ\wedge {F}\left({r}\right)=0\right)\right)$
77 69 70 76 mpbir2and ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to {r}\in {{F}}^{-1}\left[\left\{0\right\}\right]$
78 eqid ${⊢}\left|{A}-{r}\right|=\left|{A}-{r}\right|$
79 oveq2 ${⊢}{b}={r}\to {A}-{b}={A}-{r}$
80 79 fveq2d ${⊢}{b}={r}\to \left|{A}-{b}\right|=\left|{A}-{r}\right|$
81 80 rspceeqv ${⊢}\left({r}\in {{F}}^{-1}\left[\left\{0\right\}\right]\wedge \left|{A}-{r}\right|=\left|{A}-{r}\right|\right)\to \exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}\left|{A}-{r}\right|=\left|{A}-{b}\right|$
82 77 78 81 sylancl ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to \exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}\left|{A}-{r}\right|=\left|{A}-{b}\right|$
83 55 68 82 elrabd ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to \left|{A}-{r}\right|\in \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}$
84 elun2 ${⊢}\left|{A}-{r}\right|\in \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\to \left|{A}-{r}\right|\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)$
85 83 84 syl ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to \left|{A}-{r}\right|\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)$
86 infrelb ${⊢}\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\subseteq ℝ\wedge \exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {d}\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)\phantom{\rule{.4em}{0ex}}{c}\le {d}\wedge \left|{A}-{r}\right|\in \left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\}\right)\right)\to sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\le \left|{A}-{r}\right|$
87 38 53 85 86 mp3an12i ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge \left({F}\left({r}\right)=0\wedge ¬{A}={r}\right)\right)\to sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\le \left|{A}-{r}\right|$
88 87 expr ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge {F}\left({r}\right)=0\right)\to \left(¬{A}={r}\to sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\le \left|{A}-{r}\right|\right)$
89 88 orrd ${⊢}\left(\left({\phi }\wedge {r}\in ℝ\right)\wedge {F}\left({r}\right)=0\right)\to \left({A}={r}\vee sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\le \left|{A}-{r}\right|\right)$
90 89 ex ${⊢}\left({\phi }\wedge {r}\in ℝ\right)\to \left({F}\left({r}\right)=0\to \left({A}={r}\vee sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\le \left|{A}-{r}\right|\right)\right)$
91 90 ralrimiva ${⊢}{\phi }\to \forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\left({F}\left({r}\right)=0\to \left({A}={r}\vee sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\le \left|{A}-{r}\right|\right)\right)$
92 breq1 ${⊢}{x}=sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\to \left({x}\le \left|{A}-{r}\right|↔sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\le \left|{A}-{r}\right|\right)$
93 92 orbi2d ${⊢}{x}=sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\to \left(\left({A}={r}\vee {x}\le \left|{A}-{r}\right|\right)↔\left({A}={r}\vee sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\le \left|{A}-{r}\right|\right)\right)$
94 93 imbi2d ${⊢}{x}=sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\to \left(\left({F}\left({r}\right)=0\to \left({A}={r}\vee {x}\le \left|{A}-{r}\right|\right)\right)↔\left({F}\left({r}\right)=0\to \left({A}={r}\vee sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\le \left|{A}-{r}\right|\right)\right)\right)$
95 94 ralbidv ${⊢}{x}=sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\to \left(\forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\left({F}\left({r}\right)=0\to \left({A}={r}\vee {x}\le \left|{A}-{r}\right|\right)\right)↔\forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\left({F}\left({r}\right)=0\to \left({A}={r}\vee sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\le \left|{A}-{r}\right|\right)\right)\right)$
96 95 rspcev ${⊢}\left(sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\in {ℝ}^{+}\wedge \forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\left({F}\left({r}\right)=0\to \left({A}={r}\vee sup\left(\left\{1\right\}\cup \left\{{a}\in {ℝ}^{+}|\exists {b}\in {{F}}^{-1}\left[\left\{0\right\}\right]\phantom{\rule{.4em}{0ex}}{a}=\left|{A}-{b}\right|\right\},ℝ,<\right)\le \left|{A}-{r}\right|\right)\right)\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\left({F}\left({r}\right)=0\to \left({A}={r}\vee {x}\le \left|{A}-{r}\right|\right)\right)$
97 42 91 96 syl2anc ${⊢}{\phi }\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\left({F}\left({r}\right)=0\to \left({A}={r}\vee {x}\le \left|{A}-{r}\right|\right)\right)$
98 fveqeq2 ${⊢}{r}=\frac{{p}}{{q}}\to \left({F}\left({r}\right)=0↔{F}\left(\frac{{p}}{{q}}\right)=0\right)$
99 eqeq2 ${⊢}{r}=\frac{{p}}{{q}}\to \left({A}={r}↔{A}=\frac{{p}}{{q}}\right)$
100 oveq2 ${⊢}{r}=\frac{{p}}{{q}}\to {A}-{r}={A}-\left(\frac{{p}}{{q}}\right)$
101 100 fveq2d ${⊢}{r}=\frac{{p}}{{q}}\to \left|{A}-{r}\right|=\left|{A}-\left(\frac{{p}}{{q}}\right)\right|$
102 101 breq2d ${⊢}{r}=\frac{{p}}{{q}}\to \left({x}\le \left|{A}-{r}\right|↔{x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$
103 99 102 orbi12d ${⊢}{r}=\frac{{p}}{{q}}\to \left(\left({A}={r}\vee {x}\le \left|{A}-{r}\right|\right)↔\left({A}=\frac{{p}}{{q}}\vee {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)$
104 98 103 imbi12d ${⊢}{r}=\frac{{p}}{{q}}\to \left(\left({F}\left({r}\right)=0\to \left({A}={r}\vee {x}\le \left|{A}-{r}\right|\right)\right)↔\left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)\right)$
105 104 rspcv ${⊢}\frac{{p}}{{q}}\in ℝ\to \left(\forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\left({F}\left({r}\right)=0\to \left({A}={r}\vee {x}\le \left|{A}-{r}\right|\right)\right)\to \left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)\right)$
106 znq ${⊢}\left({p}\in ℤ\wedge {q}\in ℕ\right)\to \frac{{p}}{{q}}\in ℚ$
107 qre ${⊢}\frac{{p}}{{q}}\in ℚ\to \frac{{p}}{{q}}\in ℝ$
108 106 107 syl ${⊢}\left({p}\in ℤ\wedge {q}\in ℕ\right)\to \frac{{p}}{{q}}\in ℝ$
109 105 108 syl11 ${⊢}\forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\left({F}\left({r}\right)=0\to \left({A}={r}\vee {x}\le \left|{A}-{r}\right|\right)\right)\to \left(\left({p}\in ℤ\wedge {q}\in ℕ\right)\to \left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)\right)$
110 109 ralrimivv ${⊢}\forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\left({F}\left({r}\right)=0\to \left({A}={r}\vee {x}\le \left|{A}-{r}\right|\right)\right)\to \forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)$
111 110 reximi ${⊢}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\left({F}\left({r}\right)=0\to \left({A}={r}\vee {x}\le \left|{A}-{r}\right|\right)\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)$
112 97 111 syl ${⊢}{\phi }\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)$
113 simplr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {x}\in {ℝ}^{+}$
114 simprr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {q}\in ℕ$
115 3 nnnn0d ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
116 115 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {N}\in {ℕ}_{0}$
117 114 116 nnexpcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {{q}}^{{N}}\in ℕ$
118 117 nnrpd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {{q}}^{{N}}\in {ℝ}^{+}$
119 113 118 rpdivcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{{x}}{{{q}}^{{N}}}\in {ℝ}^{+}$
120 119 rpred ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{{x}}{{{q}}^{{N}}}\in ℝ$
121 120 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\wedge {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\to \frac{{x}}{{{q}}^{{N}}}\in ℝ$
122 simpllr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\wedge {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\to {x}\in {ℝ}^{+}$
123 122 rpred ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\wedge {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\to {x}\in ℝ$
124 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {A}\in ℝ$
125 108 adantl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{{p}}{{q}}\in ℝ$
126 124 125 resubcld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {A}-\left(\frac{{p}}{{q}}\right)\in ℝ$
127 126 recnd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {A}-\left(\frac{{p}}{{q}}\right)\in ℂ$
128 127 abscld ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\in ℝ$
129 128 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\wedge {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\to \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\in ℝ$
130 rpre ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℝ$
131 130 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to {x}\in ℝ$
132 113 rpcnne0d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left({x}\in ℂ\wedge {x}\ne 0\right)$
133 divid ${⊢}\left({x}\in ℂ\wedge {x}\ne 0\right)\to \frac{{x}}{{x}}=1$
134 132 133 syl ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{{x}}{{x}}=1$
135 117 nnge1d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to 1\le {{q}}^{{N}}$
136 134 135 eqbrtrd ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{{x}}{{x}}\le {{q}}^{{N}}$
137 131 113 118 136 lediv23d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \frac{{x}}{{{q}}^{{N}}}\le {x}$
138 137 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\wedge {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\to \frac{{x}}{{{q}}^{{N}}}\le {x}$
139 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\wedge {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\to {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|$
140 121 123 129 138 139 letrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\wedge {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\to \frac{{x}}{{{q}}^{{N}}}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|$
141 140 ex ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left({x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\to \frac{{x}}{{{q}}^{{N}}}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)$
142 141 orim2d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left(\left({A}=\frac{{p}}{{q}}\vee {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\to \left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{N}}}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)$
143 142 imim2d ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({p}\in ℤ\wedge {q}\in ℕ\right)\right)\to \left(\left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)\to \left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{N}}}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)\right)$
144 143 ralimdvva ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)\to \forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{N}}}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)\right)$
145 144 reximdva ${⊢}{\phi }\to \left(\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee {x}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{N}}}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)\right)$
146 112 145 mpd ${⊢}{\phi }\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {p}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℕ\phantom{\rule{.4em}{0ex}}\left({F}\left(\frac{{p}}{{q}}\right)=0\to \left({A}=\frac{{p}}{{q}}\vee \frac{{x}}{{{q}}^{{N}}}\le \left|{A}-\left(\frac{{p}}{{q}}\right)\right|\right)\right)$