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 = \{x \in ℂ \| (\|x\| \leq r \land \forall k \in ℕ_{0} \frac{1}{r} \leq \|x + k\|)\}$
	lgamucov.a	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
	lgamucov.j	$⊢ J = TopOpen (ℂ_{fld})$
Assertion	lgamucov	$⊢ φ \to \exists r \in ℕ A \in int (J) (U)$

Proof

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

Metamath Proof Explorer

Theorem lgamucov

Proof