lgamucov - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lgamucov		Structured version Visualization version GIF version

Theorem lgamucov 27347

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

**Hypotheses**
Ref	Expression
lgamucov.u	⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}
lgamucov.a	⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
lgamucov.j	⊢ 𝐽 = (TopOpen‘ℂ_fld)

**Assertion**
Ref	Expression
lgamucov	⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))

Distinct variable groups: 𝑘,𝑟,𝑥,𝐴 𝜑,𝑘,𝑟,𝑥 Allowed substitution hints: 𝑈(𝑥, 𝑘, 𝑟) 𝐽(𝑥, 𝑘, 𝑟)

Proof of Theorem lgamucov Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnxmet 25071	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
2		difss 4083	. . . . 5 ⊢ (ℤ ∖ ℕ) ⊆ ℤ
3		lgamucov.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
4	3	sszcld 25117	. . . . 5 ⊢ ((ℤ ∖ ℕ) ⊆ ℤ → (ℤ ∖ ℕ) ∈ (Clsd‘𝐽))
5	3	cnfldtopon 25081	. . . . . . 7 ⊢ 𝐽 ∈ (TopOn‘ℂ)
6	5	toponunii 23214	. . . . . 6 ⊢ ℂ = ∪ 𝐽
7	6	cldopn 23329	. . . . 5 ⊢ ((ℤ ∖ ℕ) ∈ (Clsd‘𝐽) → (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽)
8	2, 4, 7	mp2b 10	. . . 4 ⊢ (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽
9	8	a1i 11	. . 3 ⊢ (𝜑 → (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽)
10		lgamucov.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
11	3	cnfldtopn 25080	. . . 4 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
12	11	mopni2 24792	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽 ∧ 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) → ∃𝑎 ∈ ℝ⁺ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
13	1, 9, 10, 12	mp3an2i 1495	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ⁺ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
14	10	eldifad 3911	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
15	14	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝐴 ∈ ℂ)
16	15	abscld 15586	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (abs‘𝐴) ∈ ℝ)
17		simprl 783	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ⁺)
18	17	rpred 13145	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ)
19	16, 18	readdcld 11319	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ((abs‘𝐴) + 𝑎) ∈ ℝ)
20		2re 12398	. . . . . . 7 ⊢ 2 ∈ ℝ
21	20	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 2 ∈ ℝ)
22	21, 17	rerpdivcld 13176	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (2 / 𝑎) ∈ ℝ)
23	19, 22	readdcld 11319	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
24		arch 12584	. . . 4 ⊢ ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
25	23, 24	syl 18	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
26	3	cnfldtop 25082	. . . . . . . 8 ⊢ 𝐽 ∈ Top
27	26	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐽 ∈ Top)
28		lgamucov.u	. . . . . . . . 9 ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}
29	28	ssrab3 4030	. . . . . . . 8 ⊢ 𝑈 ⊆ ℂ
30	29	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑈 ⊆ ℂ)
31	15	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ℂ)
32	17	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑎 ∈ ℝ⁺)
33	32	rphalfcld 13157	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈ ℝ⁺)
34	33	rpxrd 13146	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈ ℝ^*)
35	11	blopn 24799	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽)
36	1, 31, 34, 35	mp3an2i 1495	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽)
37		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑥 ∈ ℂ)
38	37	abscld 15586	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ∈ ℝ)
39		simp-4r 796	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℕ)
40	39	nnred 12331	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℝ)
41	23	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
42	19	ad4antr 745	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) ∈ ℝ)
43	16	ad4antr 745	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝐴) ∈ ℝ)
44	38, 43	resubcld 11725	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ∈ ℝ)
45	18	ad4antr 745	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ)
46	45	rehalfcld 12574	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) ∈ ℝ)
47	31	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝐴 ∈ ℂ)
48	37, 47	subcld 11650	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑥 − 𝐴) ∈ ℂ)
49	48	abscld 15586	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) ∈ ℝ)
50	37, 47	abs2difd 15607	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ≤ (abs‘(𝑥 − 𝐴)))
51		eqid 2761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs ∘ − ) = (abs ∘ − )
52	51	cnmetdval 25069	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥)))
53	47, 37, 52	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥)))
54	47, 37	abssubd 15603	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝐴 − 𝑥)) = (abs‘(𝑥 − 𝐴)))
55	53, 54	eqtrd 2796	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐴)))
56		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))
57	55, 56	eqbrtrrd 5129	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) < (𝑎 / 2))
58	44, 49, 46, 50, 57	lelttrd 11449	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < (𝑎 / 2))
59	32	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ⁺)
60		rphalflt 13132	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℝ⁺ → (𝑎 / 2) < 𝑎)
61	59, 60	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) < 𝑎)
62	44, 46, 45, 58, 61	lttrd 11452	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < 𝑎)
63	38, 43, 45	ltsubadd2d 11895	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝑥) − (abs‘𝐴)) < 𝑎 ↔ (abs‘𝑥) < ((abs‘𝐴) + 𝑎)))
64	62, 63	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < ((abs‘𝐴) + 𝑎))
65		2rp 13106	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ⁺
66	65	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 2 ∈ ℝ⁺)
67	66, 59	rpdivcld 13162	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (2 / 𝑎) ∈ ℝ⁺)
68	42, 67	ltaddrpd 13178	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎)))
69	38, 42, 41, 64, 68	lttrd 11452	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎)))
70		simpllr 788	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
71	38, 41, 40, 69, 70	lttrd 11452	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < 𝑟)
72	38, 40, 71	ltled 11439	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ≤ 𝑟)
73	39	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℕ)
74	73	nnrecred 12370	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) ∈ ℝ)
75		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑥 ∈ ℂ)
76		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
77	76	nn0cnd 12650	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℂ)
78	75, 77	addcld 11309	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥 + 𝑘) ∈ ℂ)
79	78	abscld 15586	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑥 + 𝑘)) ∈ ℝ)
80	46	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑎 / 2) ∈ ℝ)
81	22	ad5antr 747	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) ∈ ℝ)
82	41	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
83	40	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℝ)
84	47	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ ℂ)
85	10	ad6antr 749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
86	85	dmgmn0 27335	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ≠ 0)
87	84, 86	absrpcld 15598	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ⁺)
88	59	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℝ⁺)
89	87, 88	rpaddcld 13160	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((abs‘𝐴) + 𝑎) ∈ ℝ⁺)
90	81, 89	ltaddrp2d 13179	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎)))
91		simp-4r 796	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
92	81, 82, 83, 90, 91	lttrd 11452	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) < 𝑟)
93	67	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) ∈ ℝ⁺)
94	73	nnrpd 13143	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℝ⁺)
95	93, 94	ltrecd 13163	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((2 / 𝑎) < 𝑟 ↔ (1 / 𝑟) < (1 / (2 / 𝑎))))
96	92, 95	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (1 / (2 / 𝑎)))
97		2cnd 12402	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 2 ∈ ℂ)
98	88	rpcnd 13147	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℂ)
99		2ne0 12430	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
100	99	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 2 ≠ 0)
101	88	rpne0d 13150	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ≠ 0)
102	97, 98, 100, 101	recdivd 12091	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / (2 / 𝑎)) = (𝑎 / 2))
103	96, 102	breqtrd 5131	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (𝑎 / 2))
104		eldmgm 27331	. . . . . . . . . . . . . . . . 17 ⊢ (-𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↔ (-𝑘 ∈ ℂ ∧ ¬ --𝑘 ∈ ℕ₀))
105	104	simprbi 503	. . . . . . . . . . . . . . . 16 ⊢ (-𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → ¬ --𝑘 ∈ ℕ₀)
106	77	negnegd 11641	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → --𝑘 = 𝑘)
107	106, 76	eqeltrd 2861	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → --𝑘 ∈ ℕ₀)
108	105, 107	nsyl3 139	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ¬ -𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
109	1	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs ∘ − ) ∈ (∞Met‘ℂ))
110	34	ad3antrrr 743	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑎 / 2) ∈ ℝ^*)
111	77	negcld 11637	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → -𝑘 ∈ ℂ)
112		elbl2 24689	. . . . . . . . . . . . . . . . . 18 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ)) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2)))
113	109, 110, 75, 111, 112	syl22anc 852	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2)))
114	51	cnmetdval 25069	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘)))
115	75, 111, 114	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘)))
116	75, 77	subnegd 11657	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥 − -𝑘) = (𝑥 + 𝑘))
117	116	fveq2d 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑥 − -𝑘)) = (abs‘(𝑥 + 𝑘)))
118	115, 117	eqtrd 2796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 + 𝑘)))
119	118	breq1d 5113	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((𝑥(abs ∘ − )-𝑘) < (𝑎 / 2) ↔ (abs‘(𝑥 + 𝑘)) < (𝑎 / 2)))
120	79, 80	ltnled 11438	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((abs‘(𝑥 + 𝑘)) < (𝑎 / 2) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))))
121	113, 119, 120	3bitrd 308	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))))
122	45	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℝ)
123		simplr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))
124		elbl3 24691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ^*) ∧ (𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ)) → (𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)))
125	109, 110, 75, 84, 124	syl22anc 852	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)))
126	123, 125	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)))
127		blhalf 24704	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ∈ ℝ ∧ 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)))) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ − ))𝑎))
128	109, 75, 122, 126, 127	syl22anc 852	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ − ))𝑎))
129		simprr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
130	129	ad5antr 747	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
131	128, 130	sstrd 3941	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
132	131	sseld 3930	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) → -𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ))))
133	121, 132	sylbird 263	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)) → -𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ))))
134	108, 133	mt3d 149	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)))
135	74, 80, 79, 103, 134	ltletrd 11451	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (abs‘(𝑥 + 𝑘)))
136	74, 79, 135	ltled 11439	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))
137	136	ralrimiva 3155	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))
138	72, 137	jca 521	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))))
139	138	ex 418	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) → ((𝐴(abs ∘ − )𝑥) < (𝑎 / 2) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))))
140	139	ss2rabdv 4023	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)} ⊆ {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))})
141		blval 24685	. . . . . . . . 9 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) = {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)})
142	1, 31, 34, 141	mp3an2i 1495	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) = {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)})
143	28	a1i 11	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))})
144	140, 142, 143	3sstr4d 3986	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)
145	6	ssntr 23356	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑈 ⊆ ℂ) ∧ ((𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽 ∧ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈))
146	27, 30, 36, 144, 145	syl22anc 852	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈))
147		blcntr 24712	. . . . . . 7 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ⁺) → 𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)))
148	1, 31, 33, 147	mp3an2i 1495	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)))
149	146, 148	sseldd 3932	. . . . 5 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ((int‘𝐽)‘𝑈))
150	149	ex 418	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) → ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → 𝐴 ∈ ((int‘𝐽)‘𝑈)))
151	150	reximdva 3176	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)))
152	25, 151	mpd 16	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))
153	13, 152	rexlimddv 3170	1 ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 {crab 3413 ∖ cdif 3896 ⊆ wss 3899 class class class wbr 5103 ∘ ccom 5655 ‘cfv 6531 (class class class)co 7412 ℂcc 11179 ℝcr 11180 0cc0 11181 1c1 11182 + caddc 11184 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 − cmin 11522 -cneg 11523 / cdiv 11954 ℕcn 12316 2c2 12378 ℕ₀cn0 12587 ℤcz 12674 ℝ⁺crp 13101 abscabs 15381 TopOpenctopn 17572 ∞Metcxmet 21643 ballcbl 21645 ℂ_fldccnfld 21658 Topctop 23191 Clsdccld 23314 intcnt 23315

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-er 8701 df-map 8833 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fi 9387 df-sup 9418 df-inf 9419 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-5 12389 df-6 12390 df-7 12391 df-8 12392 df-9 12393 df-n0 12588 df-z 12675 df-dec 12796 df-uz 12947 df-q 13057 df-rp 13102 df-xneg 13222 df-xadd 13223 df-xmul 13224 df-ioo 13461 df-fz 13621 df-fl 13912 df-seq 14125 df-exp 14185 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-struct 17305 df-slot 17340 df-ndx 17352 df-base 17368 df-plusg 17421 df-mulr 17422 df-starv 17423 df-tset 17427 df-ple 17428 df-ds 17430 df-unif 17431 df-rest 17573 df-topn 17574 df-topgen 17594 df-psmet 21650 df-xmet 21651 df-met 21652 df-bl 21653 df-mopn 21654 df-cnfld 21659 df-top 23192 df-topon 23209 df-topsp 23231 df-bases 23244 df-cld 23317 df-ntr 23318 df-xms 24619 df-ms 24620

This theorem is used by: lgamucov2 27348

W3C validator