| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cnxmet 24794 | . . 3
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) | 
| 2 |  | difss 4135 | . . . . 5
⊢ (ℤ
∖ ℕ) ⊆ ℤ | 
| 3 |  | lgamucov.j | . . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) | 
| 4 | 3 | sszcld 24840 | . . . . 5
⊢ ((ℤ
∖ ℕ) ⊆ ℤ → (ℤ ∖ ℕ) ∈
(Clsd‘𝐽)) | 
| 5 | 3 | cnfldtopon 24804 | . . . . . . 7
⊢ 𝐽 ∈
(TopOn‘ℂ) | 
| 6 | 5 | toponunii 22923 | . . . . . 6
⊢ ℂ =
∪ 𝐽 | 
| 7 | 6 | cldopn 23040 | . . . . 5
⊢ ((ℤ
∖ ℕ) ∈ (Clsd‘𝐽) → (ℂ ∖ (ℤ ∖
ℕ)) ∈ 𝐽) | 
| 8 | 2, 4, 7 | mp2b 10 | . . . 4
⊢ (ℂ
∖ (ℤ ∖ ℕ)) ∈ 𝐽 | 
| 9 | 8 | a1i 11 | . . 3
⊢ (𝜑 → (ℂ ∖ (ℤ
∖ ℕ)) ∈ 𝐽) | 
| 10 |  | lgamucov.a | . . 3
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) | 
| 11 | 3 | cnfldtopn 24803 | . . . 4
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) | 
| 12 | 11 | mopni2 24507 | . . 3
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖
(ℤ ∖ ℕ)) ∈ 𝐽 ∧ 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) → ∃𝑎
∈ ℝ+ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖
(ℤ ∖ ℕ))) | 
| 13 | 1, 9, 10, 12 | mp3an2i 1467 | . 2
⊢ (𝜑 → ∃𝑎 ∈ ℝ+ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) | 
| 14 | 10 | eldifad 3962 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 15 | 14 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝐴 ∈ ℂ) | 
| 16 | 15 | abscld 15476 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (abs‘𝐴) ∈ ℝ) | 
| 17 |  | simprl 770 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ+) | 
| 18 | 17 | rpred 13078 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ) | 
| 19 | 16, 18 | readdcld 11291 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ((abs‘𝐴) + 𝑎) ∈ ℝ) | 
| 20 |  | 2re 12341 | . . . . . . 7
⊢ 2 ∈
ℝ | 
| 21 | 20 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 2 ∈ ℝ) | 
| 22 | 21, 17 | rerpdivcld 13109 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (2 / 𝑎) ∈ ℝ) | 
| 23 | 19, 22 | readdcld 11291 | . . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ) | 
| 24 |  | arch 12525 | . . . 4
⊢
((((abs‘𝐴) +
𝑎) + (2 / 𝑎)) ∈ ℝ →
∃𝑟 ∈ ℕ
(((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) | 
| 25 | 23, 24 | syl 17 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) | 
| 26 | 3 | cnfldtop 24805 | . . . . . . . 8
⊢ 𝐽 ∈ Top | 
| 27 | 26 | a1i 11 | . . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐽 ∈ Top) | 
| 28 |  | lgamucov.u | . . . . . . . . 9
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} | 
| 29 | 28 | ssrab3 4081 | . . . . . . . 8
⊢ 𝑈 ⊆
ℂ | 
| 30 | 29 | a1i 11 | . . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑈 ⊆ ℂ) | 
| 31 | 15 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ℂ) | 
| 32 | 17 | ad2antrr 726 | . . . . . . . . . 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 24514 | . . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ*) →
(𝐴(ball‘(abs ∘
− ))(𝑎 / 2)) ∈
𝐽) | 
| 36 | 1, 31, 34, 35 | mp3an2i 1467 | . . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽) | 
| 37 |  | simplr 768 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑥 ∈ ℂ) | 
| 38 | 37 | abscld 15476 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ∈ ℝ) | 
| 39 |  | simp-4r 783 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℕ) | 
| 40 | 39 | nnred 12282 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℝ) | 
| 41 | 23 | ad4antr 732 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ) | 
| 42 | 19 | ad4antr 732 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) ∈ ℝ) | 
| 43 | 16 | ad4antr 732 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝐴) ∈ ℝ) | 
| 44 | 38, 43 | resubcld 11692 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ∈ ℝ) | 
| 45 | 18 | ad4antr 732 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ) | 
| 46 | 45 | rehalfcld 12515 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) ∈ ℝ) | 
| 47 | 31 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝐴 ∈ ℂ) | 
| 48 | 37, 47 | subcld 11621 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑥 − 𝐴) ∈ ℂ) | 
| 49 | 48 | abscld 15476 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) ∈ ℝ) | 
| 50 | 37, 47 | abs2difd 15497 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ≤ (abs‘(𝑥 − 𝐴))) | 
| 51 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 52 | 51 | cnmetdval 24792 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥))) | 
| 53 | 47, 37, 52 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥))) | 
| 54 | 47, 37 | abssubd 15493 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝐴 − 𝑥)) = (abs‘(𝑥 − 𝐴))) | 
| 55 | 53, 54 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐴))) | 
| 56 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) | 
| 57 | 55, 56 | eqbrtrrd 5166 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) < (𝑎 / 2)) | 
| 58 | 44, 49, 46, 50, 57 | lelttrd 11420 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < (𝑎 / 2)) | 
| 59 | 32 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ+) | 
| 60 |  | rphalflt 13065 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ℝ+
→ (𝑎 / 2) < 𝑎) | 
| 61 | 59, 60 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) < 𝑎) | 
| 62 | 44, 46, 45, 58, 61 | lttrd 11423 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < 𝑎) | 
| 63 | 38, 43, 45 | ltsubadd2d 11862 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝑥) − (abs‘𝐴)) < 𝑎 ↔ (abs‘𝑥) < ((abs‘𝐴) + 𝑎))) | 
| 64 | 62, 63 | mpbid 232 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < ((abs‘𝐴) + 𝑎)) | 
| 65 |  | 2rp 13040 | . . . . . . . . . . . . . . . . 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 11423 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎))) | 
| 70 |  | simpllr 775 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) | 
| 71 | 38, 41, 40, 69, 70 | lttrd 11423 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < 𝑟) | 
| 72 | 38, 40, 71 | ltled 11410 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ≤ 𝑟) | 
| 73 | 39 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℕ) | 
| 74 | 73 | nnrecred 12318 | . . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) ∈
ℝ) | 
| 75 |  | simpllr 775 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈
ℂ) | 
| 76 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) | 
| 77 | 76 | nn0cnd 12591 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) | 
| 78 | 75, 77 | addcld 11281 | . . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥 + 𝑘) ∈ ℂ) | 
| 79 | 78 | abscld 15476 | . . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝑥 + 𝑘)) ∈
ℝ) | 
| 80 | 46 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑎 / 2) ∈
ℝ) | 
| 81 | 22 | ad5antr 734 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) ∈
ℝ) | 
| 82 | 41 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ) | 
| 83 | 40 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℝ) | 
| 84 | 47 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈
ℂ) | 
| 85 | 10 | ad6antr 736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ (ℂ ∖
(ℤ ∖ ℕ))) | 
| 86 | 85 | dmgmn0 27070 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ≠ 0) | 
| 87 | 84, 86 | absrpcld 15488 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ+) | 
| 88 | 59 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℝ+) | 
| 89 | 87, 88 | rpaddcld 13093 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
((abs‘𝐴) + 𝑎) ∈
ℝ+) | 
| 90 | 81, 89 | ltaddrp2d 13112 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎))) | 
| 91 |  | simp-4r 783 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) | 
| 92 | 81, 82, 83, 90, 91 | lttrd 11423 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) < 𝑟) | 
| 93 | 67 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) ∈
ℝ+) | 
| 94 | 73 | nnrpd 13076 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℝ+) | 
| 95 | 93, 94 | ltrecd 13096 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → ((2 /
𝑎) < 𝑟 ↔ (1 / 𝑟) < (1 / (2 / 𝑎)))) | 
| 96 | 92, 95 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (1 / (2 / 𝑎))) | 
| 97 |  | 2cnd 12345 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℂ) | 
| 98 | 88 | rpcnd 13080 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℂ) | 
| 99 |  | 2ne0 12371 | . . . . . . . . . . . . . . . . 17
⊢ 2 ≠
0 | 
| 100 | 99 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 2 ≠
0) | 
| 101 | 88 | rpne0d 13083 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ≠ 0) | 
| 102 | 97, 98, 100, 101 | recdivd 12061 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 / (2 /
𝑎)) = (𝑎 / 2)) | 
| 103 | 96, 102 | breqtrd 5168 | . . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (𝑎 / 2)) | 
| 104 |  | eldmgm 27066 | . . . . . . . . . . . . . . . . 17
⊢ (-𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)) ↔ (-𝑘 ∈ ℂ ∧ ¬ --𝑘 ∈
ℕ0)) | 
| 105 | 104 | simprbi 496 | . . . . . . . . . . . . . . . 16
⊢ (-𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)) → ¬ --𝑘 ∈ ℕ0) | 
| 106 | 77 | negnegd 11612 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → --𝑘 = 𝑘) | 
| 107 | 106, 76 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → --𝑘 ∈
ℕ0) | 
| 108 | 105, 107 | nsyl3 138 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → ¬
-𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ))) | 
| 109 | 1 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (abs
∘ − ) ∈ (∞Met‘ℂ)) | 
| 110 | 34 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑎 / 2) ∈
ℝ*) | 
| 111 | 77 | negcld 11608 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → -𝑘 ∈
ℂ) | 
| 112 |  | elbl2 24401 | . . . . . . . . . . . . . . . . . 18
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ*) ∧
(𝑥 ∈ ℂ ∧
-𝑘 ∈ ℂ)) →
(-𝑘 ∈ (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2))) | 
| 113 | 109, 110,
75, 111, 112 | syl22anc 838 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝑥(abs ∘ − )-𝑘) < (𝑎 / 2))) | 
| 114 | 51 | cnmetdval 24792 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘))) | 
| 115 | 75, 111, 114 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘))) | 
| 116 | 75, 77 | subnegd 11628 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥 − -𝑘) = (𝑥 + 𝑘)) | 
| 117 | 116 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝑥 −
-𝑘)) = (abs‘(𝑥 + 𝑘))) | 
| 118 | 115, 117 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 + 𝑘))) | 
| 119 | 118 | breq1d 5152 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → ((𝑥(abs ∘ − )-𝑘) < (𝑎 / 2) ↔ (abs‘(𝑥 + 𝑘)) < (𝑎 / 2))) | 
| 120 | 79, 80 | ltnled 11409 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
((abs‘(𝑥 + 𝑘)) < (𝑎 / 2) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)))) | 
| 121 | 113, 119,
120 | 3bitrd 305 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)))) | 
| 122 | 45 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℝ) | 
| 123 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) | 
| 124 |  | elbl3 24403 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑎 / 2) ∈ ℝ*) ∧
(𝑥 ∈ ℂ ∧
𝐴 ∈ ℂ)) →
(𝐴 ∈ (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))) | 
| 125 | 109, 110,
75, 84, 124 | syl22anc 838 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2))) | 
| 126 | 123, 125 | mpbird 257 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2))) | 
| 127 |  | blhalf 24416 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ∈ ℝ ∧ 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)))) → (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ −
))𝑎)) | 
| 128 | 109, 75, 122, 126, 127 | syl22anc 838 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ⊆ (𝐴(ball‘(abs ∘ −
))𝑎)) | 
| 129 |  | simprr 772 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖
(ℤ ∖ ℕ))) | 
| 130 | 129 | ad5antr 734 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) | 
| 131 | 128, 130 | sstrd 3993 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) | 
| 132 | 131 | sseld 3981 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) → -𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)))) | 
| 133 | 121, 132 | sylbird 260 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (¬
(𝑎 / 2) ≤
(abs‘(𝑥 + 𝑘)) → -𝑘 ∈ (ℂ ∖ (ℤ ∖
ℕ)))) | 
| 134 | 108, 133 | mt3d 148 | . . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))) | 
| 135 | 74, 80, 79, 103, 134 | ltletrd 11422 | . . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (abs‘(𝑥 + 𝑘))) | 
| 136 | 74, 79, 135 | ltled 11410 | . . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) ≤ (abs‘(𝑥 + 𝑘))) | 
| 137 | 136 | ralrimiva 3145 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))) | 
| 138 | 72, 137 | jca 511 | . . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))) | 
| 139 | 138 | ex 412 | . . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) → ((𝐴(abs ∘ − )𝑥) < (𝑎 / 2) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))))) | 
| 140 | 139 | ss2rabdv 4075 | . . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)} ⊆ {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}) | 
| 141 |  | blval 24397 | . . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ*) →
(𝐴(ball‘(abs ∘
− ))(𝑎 / 2)) = {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)}) | 
| 142 | 1, 31, 34, 141 | mp3an2i 1467 | . . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) = {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)}) | 
| 143 | 28 | a1i 11 | . . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}) | 
| 144 | 140, 142,
143 | 3sstr4d 4038 | . . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈) | 
| 145 | 6 | ssntr 23067 | . . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑈 ⊆ ℂ) ∧ ((𝐴(ball‘(abs ∘ −
))(𝑎 / 2)) ∈ 𝐽 ∧ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈)) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈)) | 
| 146 | 27, 30, 36, 144, 145 | syl22anc 838 | . . . . . 6
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ ((int‘𝐽)‘𝑈)) | 
| 147 |  | blcntr 24424 | . . . . . . 7
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ+) →
𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2))) | 
| 148 | 1, 31, 33, 147 | mp3an2i 1467 | . . . . . 6
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ (𝐴(ball‘(abs ∘ − ))(𝑎 / 2))) | 
| 149 | 146, 148 | sseldd 3983 | . . . . 5
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ((int‘𝐽)‘𝑈)) | 
| 150 | 149 | ex 412 | . . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) → ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → 𝐴 ∈ ((int‘𝐽)‘𝑈))) | 
| 151 | 150 | reximdva 3167 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))) | 
| 152 | 25, 151 | mpd 15 | . 2
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)) | 
| 153 | 13, 152 | rexlimddv 3160 | 1
⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)) |