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 27239

Description: The 𝑈 regions used in the proof of lgamgulm 27236 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 24966	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
2		difss 4093	. . . . 5 ⊢ (ℤ ∖ ℕ) ⊆ ℤ
3		lgamucov.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
4	3	sszcld 25012	. . . . 5 ⊢ ((ℤ ∖ ℕ) ⊆ ℤ → (ℤ ∖ ℕ) ∈ (Clsd‘𝐽))
5	3	cnfldtopon 24976	. . . . . . 7 ⊢ 𝐽 ∈ (TopOn‘ℂ)
6	5	toponunii 23110	. . . . . 6 ⊢ ℂ = ∪ 𝐽
7	6	cldopn 23225	. . . . 5 ⊢ ((ℤ ∖ ℕ) ∈ (Clsd‘𝐽) → (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽)
8	2, 4, 7	mp2b 10	. . . 4 ⊢ (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽
9	8	a1i 11	. . 3 ⊢ (𝜑 → (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽)
10		lgamucov.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
11	3	cnfldtopn 24975	. . . 4 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
12	11	mopni2 24687	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ (ℤ ∖ ℕ)) ∈ 𝐽 ∧ 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ))) → ∃𝑎 ∈ ℝ⁺ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
13	1, 9, 10, 12	mp3an2i 1495	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ⁺ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
14	10	eldifad 3920	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
15	14	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝐴 ∈ ℂ)
16	15	abscld 15516	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (abs‘𝐴) ∈ ℝ)
17		simprl 783	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ⁺)
18	17	rpred 13078	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ)
19	16, 18	readdcld 11256	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ((abs‘𝐴) + 𝑎) ∈ ℝ)
20		2re 12333	. . . . . . 7 ⊢ 2 ∈ ℝ
21	20	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → 2 ∈ ℝ)
22	21, 17	rerpdivcld 13109	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (2 / 𝑎) ∈ ℝ)
23	19, 22	readdcld 11256	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ)
24		arch 12519	. . . 4 ⊢ ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
25	23, 24	syl 18	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟)
26	3	cnfldtop 24977	. . . . . . . 8 ⊢ 𝐽 ∈ Top
27	26	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐽 ∈ Top)
28		lgamucov.u	. . . . . . . . 9 ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}
29	28	ssrab3 4039	. . . . . . . 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 13090	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈ ℝ⁺)
34	33	rpxrd 13079	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈ ℝ^*)
35	11	blopn 24694	. . . . . . . 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 15516	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ∈ ℝ)
39		simp-4r 796	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℕ)
40	39	nnred 12266	. . . . . . . . . . . 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 11660	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ∈ ℝ)
45	18	ad4antr 745	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ)
46	45	rehalfcld 12509	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) ∈ ℝ)
47	31	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝐴 ∈ ℂ)
48	37, 47	subcld 11587	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑥 − 𝐴) ∈ ℂ)
49	48	abscld 15516	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) ∈ ℝ)
50	37, 47	abs2difd 15537	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ≤ (abs‘(𝑥 − 𝐴)))
51		eqid 2766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs ∘ − ) = (abs ∘ − )
52	51	cnmetdval 24964	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥)))
53	47, 37, 52	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥)))
54	47, 37	abssubd 15533	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝐴 − 𝑥)) = (abs‘(𝑥 − 𝐴)))
55	53, 54	eqtrd 2801	. . . . . . . . . . . . . . . . . 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 5140	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) < (𝑎 / 2))
58	44, 49, 46, 50, 57	lelttrd 11386	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < (𝑎 / 2))
59	32	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ⁺)
60		rphalflt 13065	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℝ⁺ → (𝑎 / 2) < 𝑎)
61	59, 60	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) < 𝑎)
62	44, 46, 45, 58, 61	lttrd 11389	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < 𝑎)
63	38, 43, 45	ltsubadd2d 11830	. . . . . . . . . . . . . . 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 13039	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ⁺
66	65	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 2 ∈ ℝ⁺)
67	66, 59	rpdivcld 13095	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (2 / 𝑎) ∈ ℝ⁺)
68	42, 67	ltaddrpd 13111	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎)))
69	38, 42, 41, 64, 68	lttrd 11389	. . . . . . . . . . . . 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 11389	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < 𝑟)
72	38, 40, 71	ltled 11376	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ≤ 𝑟)
73	39	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℕ)
74	73	nnrecred 12305	. . . . . . . . . . . . 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 12585	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℂ)
78	75, 77	addcld 11246	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥 + 𝑘) ∈ ℂ)
79	78	abscld 15516	. . . . . . . . . . . . 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 27227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ≠ 0)
87	84, 86	absrpcld 15528	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘𝐴) ∈ ℝ⁺)
88	59	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℝ⁺)
89	87, 88	rpaddcld 13093	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((abs‘𝐴) + 𝑎) ∈ ℝ⁺)
90	81, 89	ltaddrp2d 13112	. . . . . . . . . . . . . . . . 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 11389	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) < 𝑟)
93	67	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (2 / 𝑎) ∈ ℝ⁺)
94	73	nnrpd 13076	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑟 ∈ ℝ⁺)
95	93, 94	ltrecd 13096	. . . . . . . . . . . . . . . 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 12337	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 2 ∈ ℂ)
98	88	rpcnd 13080	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ∈ ℂ)
99		2ne0 12365	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
100	99	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 2 ≠ 0)
101	88	rpne0d 13083	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → 𝑎 ≠ 0)
102	97, 98, 100, 101	recdivd 12026	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / (2 / 𝑎)) = (𝑎 / 2))
103	96, 102	breqtrd 5142	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (𝑎 / 2))
104		eldmgm 27223	. . . . . . . . . . . . . . . . 17 ⊢ (-𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↔ (-𝑘 ∈ ℂ ∧ ¬ --𝑘 ∈ ℕ₀))
105	104	simprbi 503	. . . . . . . . . . . . . . . 16 ⊢ (-𝑘 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → ¬ --𝑘 ∈ ℕ₀)
106	77	negnegd 11578	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → --𝑘 = 𝑘)
107	106, 76	eqeltrd 2866	. . . . . . . . . . . . . . . 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 11574	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → -𝑘 ∈ ℂ)
112		elbl2 24584	. . . . . . . . . . . . . . . . . 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 24964	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘)))
115	75, 111, 114	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘)))
116	75, 77	subnegd 11594	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥 − -𝑘) = (𝑥 + 𝑘))
117	116	fveq2d 6892	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (abs‘(𝑥 − -𝑘)) = (abs‘(𝑥 + 𝑘)))
118	115, 117	eqtrd 2801	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 + 𝑘)))
119	118	breq1d 5124	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → ((𝑥(abs ∘ − )-𝑘) < (𝑎 / 2) ↔ (abs‘(𝑥 + 𝑘)) < (𝑎 / 2)))
120	79, 80	ltnled 11375	. . . . . . . . . . . . . . . . 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 24586	. . . . . . . . . . . . . . . . . . . . 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 24599	. . . . . . . . . . . . . . . . . . 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 3950	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
132	131	sseld 3939	. . . . . . . . . . . . . . . 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 11388	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) < (abs‘(𝑥 + 𝑘)))
136	74, 79, 135	ltled 11376	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ₀) → (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))
137	136	ralrimiva 3160	. . . . . . . . . . 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 4032	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)} ⊆ {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))})
141		blval 24580	. . . . . . . . 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 3995	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)
145	6	ssntr 23252	. . . . . . 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 24607	. . . . . . 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 3941	. . . . 5 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ((int‘𝐽)‘𝑈))
150	149	ex 418	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) → ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → 𝐴 ∈ ((int‘𝐽)‘𝑈)))
151	150	reximdva 3181	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → (∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)))
152	25, 151	mpd 16	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))
153	13, 152	rexlimddv 3175	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 2146 ≠ wne 2961 ∀wral 3082 ∃wrex 3092 {crab 3419 ∖ cdif 3905 ⊆ wss 3908 class class class wbr 5114 ∘ ccom 5670 ‘cfv 6543 (class class class)co 7423 ℂcc 11116 ℝcr 11117 0cc0 11118 1c1 11119 + caddc 11121 ℝ^*cxr 11260 < clt 11261 ≤ cle 11262 − cmin 11459 -cneg 11460 / cdiv 11889 ℕcn 12251 2c2 12313 ℕ₀cn0 12522 ℤcz 12609 ℝ⁺crp 13034 abscabs 15311 TopOpenctopn 17499 ∞Metcxmet 21544 ballcbl 21546 ℂ_fldccnfld 21559 Topctop 23087 Clsdccld 23210 intcnt 23211

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-iin 4964 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8703 df-map 8835 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-fi 9381 df-sup 9412 df-inf 9413 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-4 12323 df-5 12324 df-6 12325 df-7 12326 df-8 12327 df-9 12328 df-n0 12523 df-z 12610 df-dec 12730 df-uz 12881 df-q 12991 df-rp 13035 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13394 df-fz 13554 df-fl 13845 df-seq 14058 df-exp 14118 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-struct 17232 df-slot 17267 df-ndx 17279 df-base 17295 df-plusg 17348 df-mulr 17349 df-starv 17350 df-tset 17354 df-ple 17355 df-ds 17357 df-unif 17358 df-rest 17500 df-topn 17501 df-topgen 17521 df-psmet 21551 df-xmet 21552 df-met 21553 df-bl 21554 df-mopn 21555 df-cnfld 21560 df-top 23088 df-topon 23105 df-topsp 23127 df-bases 23140 df-cld 23213 df-ntr 23214 df-xms 24514 df-ms 24515

This theorem is used by: lgamucov2 27240

W3C validator