# Metamath Proof Explorer

## Theorem lgamucov

Description: The U regions used in the proof of lgamgulm have interiors which cover the entire domain of the Gamma function. (Contributed by Mario Carneiro, 6-Jul-2017)

Ref Expression
Hypotheses lgamucov.u ${⊢}{U}=\left\{{x}\in ℂ|\left(\left|{x}\right|\le {r}\wedge \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\frac{1}{{r}}\le \left|{x}+{k}\right|\right)\right\}$
lgamucov.a ${⊢}{\phi }\to {A}\in \left(ℂ\setminus \left(ℤ\setminus ℕ\right)\right)$
lgamucov.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
Assertion lgamucov ${⊢}{\phi }\to \exists {r}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{int}\left({J}\right)\left({U}\right)$

### Proof

Step Hyp Ref Expression
1 lgamucov.u ${⊢}{U}=\left\{{x}\in ℂ|\left(\left|{x}\right|\le {r}\wedge \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\frac{1}{{r}}\le \left|{x}+{k}\right|\right)\right\}$
2 lgamucov.a ${⊢}{\phi }\to {A}\in \left(ℂ\setminus \left(ℤ\setminus ℕ\right)\right)$
3 lgamucov.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
4 cnxmet ${⊢}\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
5 difss ${⊢}ℤ\setminus ℕ\subseteq ℤ$
6 3 sszcld ${⊢}ℤ\setminus ℕ\subseteq ℤ\to ℤ\setminus ℕ\in \mathrm{Clsd}\left({J}\right)$
7 3 cnfldtopon ${⊢}{J}\in \mathrm{TopOn}\left(ℂ\right)$
8 7 toponunii ${⊢}ℂ=\bigcup {J}$
9 8 cldopn ${⊢}ℤ\setminus ℕ\in \mathrm{Clsd}\left({J}\right)\to ℂ\setminus \left(ℤ\setminus ℕ\right)\in {J}$
10 5 6 9 mp2b ${⊢}ℂ\setminus \left(ℤ\setminus ℕ\right)\in {J}$
11 10 a1i ${⊢}{\phi }\to ℂ\setminus \left(ℤ\setminus ℕ\right)\in {J}$
12 3 cnfldtopn ${⊢}{J}=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$
13 12 mopni2 ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge ℂ\setminus \left(ℤ\setminus ℕ\right)\in {J}\wedge {A}\in \left(ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to \exists {a}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)$
14 4 11 2 13 mp3an2i ${⊢}{\phi }\to \exists {a}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)$
15 2 eldifad ${⊢}{\phi }\to {A}\in ℂ$
16 15 adantr ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to {A}\in ℂ$
17 16 abscld ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to \left|{A}\right|\in ℝ$
18 simprl ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to {a}\in {ℝ}^{+}$
19 18 rpred ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to {a}\in ℝ$
20 17 19 readdcld ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to \left|{A}\right|+{a}\in ℝ$
21 2re ${⊢}2\in ℝ$
22 21 a1i ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to 2\in ℝ$
23 22 18 rerpdivcld ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to \frac{2}{{a}}\in ℝ$
24 20 23 readdcld ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)\in ℝ$
25 arch ${⊢}\left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)\in ℝ\to \exists {r}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}$
26 24 25 syl ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to \exists {r}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}$
27 3 cnfldtop ${⊢}{J}\in \mathrm{Top}$
28 27 a1i ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to {J}\in \mathrm{Top}$
29 1 ssrab3 ${⊢}{U}\subseteq ℂ$
30 29 a1i ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to {U}\subseteq ℂ$
31 16 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to {A}\in ℂ$
32 18 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to {a}\in {ℝ}^{+}$
33 32 rphalfcld ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to \frac{{a}}{2}\in {ℝ}^{+}$
34 33 rpxrd ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to \frac{{a}}{2}\in {ℝ}^{*}$
35 12 blopn ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge {A}\in ℂ\wedge \frac{{a}}{2}\in {ℝ}^{*}\right)\to {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\in {J}$
36 4 31 34 35 mp3an2i ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\in {J}$
37 simplr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to {x}\in ℂ$
38 37 abscld ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{x}\right|\in ℝ$
39 simp-4r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to {r}\in ℕ$
40 39 nnred ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to {r}\in ℝ$
41 24 ad4antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)\in ℝ$
42 20 ad4antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{A}\right|+{a}\in ℝ$
43 17 ad4antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{A}\right|\in ℝ$
44 38 43 resubcld ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{x}\right|-\left|{A}\right|\in ℝ$
45 19 ad4antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to {a}\in ℝ$
46 45 rehalfcld ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \frac{{a}}{2}\in ℝ$
47 31 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to {A}\in ℂ$
48 37 47 subcld ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to {x}-{A}\in ℂ$
49 48 abscld ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{x}-{A}\right|\in ℝ$
50 37 47 abs2difd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{x}\right|-\left|{A}\right|\le \left|{x}-{A}\right|$
51 eqid ${⊢}\mathrm{abs}\circ -=\mathrm{abs}\circ -$
52 51 cnmetdval ${⊢}\left({A}\in ℂ\wedge {x}\in ℂ\right)\to {A}\left(\mathrm{abs}\circ -\right){x}=\left|{A}-{x}\right|$
53 47 37 52 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to {A}\left(\mathrm{abs}\circ -\right){x}=\left|{A}-{x}\right|$
54 47 37 abssubd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{A}-{x}\right|=\left|{x}-{A}\right|$
55 53 54 eqtrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to {A}\left(\mathrm{abs}\circ -\right){x}=\left|{x}-{A}\right|$
56 simpr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}$
57 55 56 eqbrtrrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{x}-{A}\right|<\frac{{a}}{2}$
58 44 49 46 50 57 lelttrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{x}\right|-\left|{A}\right|<\frac{{a}}{2}$
59 32 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to {a}\in {ℝ}^{+}$
60 rphalflt ${⊢}{a}\in {ℝ}^{+}\to \frac{{a}}{2}<{a}$
61 59 60 syl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \frac{{a}}{2}<{a}$
62 44 46 45 58 61 lttrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{x}\right|-\left|{A}\right|<{a}$
63 38 43 45 ltsubadd2d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left(\left|{x}\right|-\left|{A}\right|<{a}↔\left|{x}\right|<\left|{A}\right|+{a}\right)$
64 62 63 mpbid ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{x}\right|<\left|{A}\right|+{a}$
65 2rp ${⊢}2\in {ℝ}^{+}$
66 65 a1i ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to 2\in {ℝ}^{+}$
67 66 59 rpdivcld ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \frac{2}{{a}}\in {ℝ}^{+}$
68 42 67 ltaddrpd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{A}\right|+{a}<\left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)$
69 38 42 41 64 68 lttrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{x}\right|<\left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)$
70 simpllr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}$
71 38 41 40 69 70 lttrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{x}\right|<{r}$
72 38 40 71 ltled ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left|{x}\right|\le {r}$
73 39 adantr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {r}\in ℕ$
74 73 nnrecred ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{1}{{r}}\in ℝ$
75 simpllr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {x}\in ℂ$
76 simpr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
77 76 nn0cnd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in ℂ$
78 75 77 addcld ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {x}+{k}\in ℂ$
79 78 abscld ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left|{x}+{k}\right|\in ℝ$
80 46 adantr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{{a}}{2}\in ℝ$
81 23 ad5antr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{2}{{a}}\in ℝ$
82 41 adantr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)\in ℝ$
83 40 adantr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {r}\in ℝ$
84 47 adantr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}\in ℂ$
85 2 ad6antr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}\in \left(ℂ\setminus \left(ℤ\setminus ℕ\right)\right)$
86 85 dmgmn0 ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}\ne 0$
87 84 86 absrpcld ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left|{A}\right|\in {ℝ}^{+}$
88 59 adantr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {a}\in {ℝ}^{+}$
89 87 88 rpaddcld ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left|{A}\right|+{a}\in {ℝ}^{+}$
90 81 89 ltaddrp2d ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{2}{{a}}<\left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)$
91 simp-4r ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}$
92 81 82 83 90 91 lttrd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{2}{{a}}<{r}$
93 67 adantr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{2}{{a}}\in {ℝ}^{+}$
94 73 nnrpd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {r}\in {ℝ}^{+}$
95 93 94 ltrecd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(\frac{2}{{a}}<{r}↔\frac{1}{{r}}<\frac{1}{\frac{2}{{a}}}\right)$
96 92 95 mpbid ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{1}{{r}}<\frac{1}{\frac{2}{{a}}}$
97 2cnd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to 2\in ℂ$
98 88 rpcnd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {a}\in ℂ$
99 2ne0 ${⊢}2\ne 0$
100 99 a1i ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to 2\ne 0$
101 88 rpne0d ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {a}\ne 0$
102 97 98 100 101 recdivd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{1}{\frac{2}{{a}}}=\frac{{a}}{2}$
103 96 102 breqtrd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{1}{{r}}<\frac{{a}}{2}$
104 eldmgm ${⊢}-{k}\in \left(ℂ\setminus \left(ℤ\setminus ℕ\right)\right)↔\left(-{k}\in ℂ\wedge ¬-\left(-{k}\right)\in {ℕ}_{0}\right)$
105 104 simprbi ${⊢}-{k}\in \left(ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\to ¬-\left(-{k}\right)\in {ℕ}_{0}$
106 77 negnegd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to -\left(-{k}\right)={k}$
107 106 76 eqeltrd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to -\left(-{k}\right)\in {ℕ}_{0}$
108 105 107 nsyl3 ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to ¬-{k}\in \left(ℂ\setminus \left(ℤ\setminus ℕ\right)\right)$
109 4 a1i ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
110 34 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{{a}}{2}\in {ℝ}^{*}$
111 77 negcld ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to -{k}\in ℂ$
112 elbl2 ${⊢}\left(\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge \frac{{a}}{2}\in {ℝ}^{*}\right)\wedge \left({x}\in ℂ\wedge -{k}\in ℂ\right)\right)\to \left(-{k}\in \left({x}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\right)↔{x}\left(\mathrm{abs}\circ -\right)\left(-{k}\right)<\frac{{a}}{2}\right)$
113 109 110 75 111 112 syl22anc ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(-{k}\in \left({x}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\right)↔{x}\left(\mathrm{abs}\circ -\right)\left(-{k}\right)<\frac{{a}}{2}\right)$
114 51 cnmetdval ${⊢}\left({x}\in ℂ\wedge -{k}\in ℂ\right)\to {x}\left(\mathrm{abs}\circ -\right)\left(-{k}\right)=\left|{x}-\left(-{k}\right)\right|$
115 75 111 114 syl2anc ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {x}\left(\mathrm{abs}\circ -\right)\left(-{k}\right)=\left|{x}-\left(-{k}\right)\right|$
116 75 77 subnegd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {x}-\left(-{k}\right)={x}+{k}$
117 116 fveq2d ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left|{x}-\left(-{k}\right)\right|=\left|{x}+{k}\right|$
118 115 117 eqtrd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {x}\left(\mathrm{abs}\circ -\right)\left(-{k}\right)=\left|{x}+{k}\right|$
119 118 breq1d ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({x}\left(\mathrm{abs}\circ -\right)\left(-{k}\right)<\frac{{a}}{2}↔\left|{x}+{k}\right|<\frac{{a}}{2}\right)$
120 79 80 ltnled ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(\left|{x}+{k}\right|<\frac{{a}}{2}↔¬\frac{{a}}{2}\le \left|{x}+{k}\right|\right)$
121 113 119 120 3bitrd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(-{k}\in \left({x}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\right)↔¬\frac{{a}}{2}\le \left|{x}+{k}\right|\right)$
122 45 adantr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {a}\in ℝ$
123 simplr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}$
124 elbl3 ${⊢}\left(\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge \frac{{a}}{2}\in {ℝ}^{*}\right)\wedge \left({x}\in ℂ\wedge {A}\in ℂ\right)\right)\to \left({A}\in \left({x}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\right)↔{A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)$
125 109 110 75 84 124 syl22anc ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({A}\in \left({x}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\right)↔{A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)$
126 123 125 mpbird ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}\in \left({x}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\right)$
127 blhalf ${⊢}\left(\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge {x}\in ℂ\right)\wedge \left({a}\in ℝ\wedge {A}\in \left({x}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\right)\right)\right)\to {x}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\subseteq {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}$
128 109 75 122 126 127 syl22anc ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {x}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\subseteq {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}$
129 simprr ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)$
130 129 ad5antr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)$
131 128 130 sstrd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to {x}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)$
132 131 sseld ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(-{k}\in \left({x}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\right)\to -{k}\in \left(ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)$
133 121 132 sylbird ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(¬\frac{{a}}{2}\le \left|{x}+{k}\right|\to -{k}\in \left(ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)$
134 108 133 mt3d ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{{a}}{2}\le \left|{x}+{k}\right|$
135 74 80 79 103 134 ltletrd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{1}{{r}}<\left|{x}+{k}\right|$
136 74 79 135 ltled ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\wedge {k}\in {ℕ}_{0}\right)\to \frac{1}{{r}}\le \left|{x}+{k}\right|$
137 136 ralrimiva ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\frac{1}{{r}}\le \left|{x}+{k}\right|$
138 72 137 jca ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\wedge {A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right)\to \left(\left|{x}\right|\le {r}\wedge \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\frac{1}{{r}}\le \left|{x}+{k}\right|\right)$
139 138 ex ${⊢}\left(\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\wedge {x}\in ℂ\right)\to \left({A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\to \left(\left|{x}\right|\le {r}\wedge \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\frac{1}{{r}}\le \left|{x}+{k}\right|\right)\right)$
140 139 ss2rabdv ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to \left\{{x}\in ℂ|{A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right\}\subseteq \left\{{x}\in ℂ|\left(\left|{x}\right|\le {r}\wedge \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\frac{1}{{r}}\le \left|{x}+{k}\right|\right)\right\}$
141 blval ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge {A}\in ℂ\wedge \frac{{a}}{2}\in {ℝ}^{*}\right)\to {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)=\left\{{x}\in ℂ|{A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right\}$
142 4 31 34 141 mp3an2i ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)=\left\{{x}\in ℂ|{A}\left(\mathrm{abs}\circ -\right){x}<\frac{{a}}{2}\right\}$
143 1 a1i ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to {U}=\left\{{x}\in ℂ|\left(\left|{x}\right|\le {r}\wedge \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\frac{1}{{r}}\le \left|{x}+{k}\right|\right)\right\}$
144 140 142 143 3sstr4d ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\subseteq {U}$
145 8 ssntr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {U}\subseteq ℂ\right)\wedge \left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\in {J}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\subseteq {U}\right)\right)\to {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\subseteq \mathrm{int}\left({J}\right)\left({U}\right)$
146 28 30 36 144 145 syl22anc ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\subseteq \mathrm{int}\left({J}\right)\left({U}\right)$
147 blcntr ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge {A}\in ℂ\wedge \frac{{a}}{2}\in {ℝ}^{+}\right)\to {A}\in \left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\right)$
148 4 31 33 147 mp3an2i ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to {A}\in \left({A}\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{{a}}{2}\right)\right)$
149 146 148 sseldd ${⊢}\left(\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\wedge \left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\right)\to {A}\in \mathrm{int}\left({J}\right)\left({U}\right)$
150 149 ex ${⊢}\left(\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\wedge {r}\in ℕ\right)\to \left(\left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\to {A}\in \mathrm{int}\left({J}\right)\left({U}\right)\right)$
151 150 reximdva ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to \left(\exists {r}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{A}\right|+{a}+\left(\frac{2}{{a}}\right)<{r}\to \exists {r}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{int}\left({J}\right)\left({U}\right)\right)$
152 26 151 mpd ${⊢}\left({\phi }\wedge \left({a}\in {ℝ}^{+}\wedge {A}\mathrm{ball}\left(\mathrm{abs}\circ -\right){a}\subseteq ℂ\setminus \left(ℤ\setminus ℕ\right)\right)\right)\to \exists {r}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{int}\left({J}\right)\left({U}\right)$
153 14 152 rexlimddv ${⊢}{\phi }\to \exists {r}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{int}\left({J}\right)\left({U}\right)$