Step | Hyp | Ref
| Expression |
1 | | cnxmet 23528 |
. . 3
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
2 | | difss 4023 |
. . . . 5
⊢ (ℤ
∖ ℕ) ⊆ ℤ |
3 | | lgamucov.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
4 | 3 | sszcld 23572 |
. . . . 5
⊢ ((ℤ
∖ ℕ) ⊆ ℤ → (ℤ ∖ ℕ) ∈
(Clsd‘𝐽)) |
5 | 3 | cnfldtopon 23538 |
. . . . . . 7
⊢ 𝐽 ∈
(TopOn‘ℂ) |
6 | 5 | toponunii 21670 |
. . . . . 6
⊢ ℂ =
∪ 𝐽 |
7 | 6 | cldopn 21785 |
. . . . 5
⊢ ((ℤ
∖ ℕ) ∈ (Clsd‘𝐽) → (ℂ ∖ (ℤ ∖
ℕ)) ∈ 𝐽) |
8 | 2, 4, 7 | mp2b 10 |
. . . 4
⊢ (ℂ
∖ (ℤ ∖ ℕ)) ∈ 𝐽 |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → (ℂ ∖ (ℤ
∖ ℕ)) ∈ 𝐽) |
10 | | lgamucov.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
11 | 3 | cnfldtopn 23537 |
. . . 4
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
12 | 11 | mopni2 23249 |
. . 3
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖
(ℤ ∖ ℕ)) ∈ 𝐽 ∧ 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) → ∃𝑎
∈ ℝ+ (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖
(ℤ ∖ ℕ))) |
13 | 1, 9, 10, 12 | mp3an2i 1467 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ ℝ+ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) |
14 | 10 | eldifad 3856 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
15 | 14 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝐴 ∈ ℂ) |
16 | 15 | abscld 14889 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (abs‘𝐴) ∈ ℝ) |
17 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ+) |
18 | 17 | rpred 12517 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 𝑎 ∈ ℝ) |
19 | 16, 18 | readdcld 10751 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ((abs‘𝐴) + 𝑎) ∈ ℝ) |
20 | | 2re 11793 |
. . . . . . 7
⊢ 2 ∈
ℝ |
21 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → 2 ∈ ℝ) |
22 | 21, 17 | rerpdivcld 12548 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (2 / 𝑎) ∈ ℝ) |
23 | 19, 22 | readdcld 10751 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ) |
24 | | arch 11976 |
. . . 4
⊢
((((abs‘𝐴) +
𝑎) + (2 / 𝑎)) ∈ ℝ →
∃𝑟 ∈ ℕ
(((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) |
25 | 23, 24 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) |
26 | 3 | cnfldtop 23539 |
. . . . . . . 8
⊢ 𝐽 ∈ Top |
27 | 26 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐽 ∈ Top) |
28 | | lgamucov.u |
. . . . . . . . 9
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} |
29 | 28 | ssrab3 3972 |
. . . . . . . 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 12529 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈
ℝ+) |
34 | 33 | rpxrd 12518 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝑎 / 2) ∈
ℝ*) |
35 | 11 | blopn 23256 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ (𝑎 / 2) ∈ ℝ*) →
(𝐴(ball‘(abs ∘
− ))(𝑎 / 2)) ∈
𝐽) |
36 | 1, 31, 34, 35 | mp3an2i 1467 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ∈ 𝐽) |
37 | | simplr 769 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑥 ∈ ℂ) |
38 | 37 | abscld 14889 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ∈ ℝ) |
39 | | simp-4r 784 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑟 ∈ ℕ) |
40 | 39 | nnred 11734 |
. . . . . . . . . . . 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 11149 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ∈ ℝ) |
45 | 18 | ad4antr 732 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ) |
46 | 45 | rehalfcld 11966 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) ∈ ℝ) |
47 | 31 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝐴 ∈ ℂ) |
48 | 37, 47 | subcld 11078 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑥 − 𝐴) ∈ ℂ) |
49 | 48 | abscld 14889 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) ∈ ℝ) |
50 | 37, 47 | abs2difd 14910 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) ≤ (abs‘(𝑥 − 𝐴))) |
51 | | eqid 2739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (abs
∘ − ) = (abs ∘ − ) |
52 | 51 | cnmetdval 23526 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥))) |
53 | 47, 37, 52 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝐴 − 𝑥))) |
54 | 47, 37 | abssubd 14906 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝐴 − 𝑥)) = (abs‘(𝑥 − 𝐴))) |
55 | 53, 54 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝐴))) |
56 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) |
57 | 55, 56 | eqbrtrrd 5055 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘(𝑥 − 𝐴)) < (𝑎 / 2)) |
58 | 44, 49, 46, 50, 57 | lelttrd 10879 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < (𝑎 / 2)) |
59 | 32 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 𝑎 ∈ ℝ+) |
60 | | rphalflt 12504 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ℝ+
→ (𝑎 / 2) < 𝑎) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (𝑎 / 2) < 𝑎) |
62 | 44, 46, 45, 58, 61 | lttrd 10882 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) − (abs‘𝐴)) < 𝑎) |
63 | 38, 43, 45 | ltsubadd2d 11319 |
. . . . . . . . . . . . . . 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 12480 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → 2 ∈
ℝ+) |
67 | 66, 59 | rpdivcld 12534 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (2 / 𝑎) ∈
ℝ+) |
68 | 42, 67 | ltaddrpd 12550 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝐴) + 𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎))) |
69 | 38, 42, 41, 64, 68 | lttrd 10882 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎))) |
70 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) |
71 | 38, 41, 40, 69, 70 | lttrd 10882 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) < 𝑟) |
72 | 38, 40, 71 | ltled 10869 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → (abs‘𝑥) ≤ 𝑟) |
73 | 39 | adantr 484 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℕ) |
74 | 73 | nnrecred 11770 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) ∈
ℝ) |
75 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈
ℂ) |
76 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
77 | 76 | nn0cnd 12041 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) |
78 | 75, 77 | addcld 10741 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥 + 𝑘) ∈ ℂ) |
79 | 78 | abscld 14889 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝑥 + 𝑘)) ∈
ℝ) |
80 | 46 | adantr 484 |
. . . . . . . . . . . . . 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 484 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(((abs‘𝐴) + 𝑎) + (2 / 𝑎)) ∈ ℝ) |
83 | 40 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℝ) |
84 | 47 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈
ℂ) |
85 | 10 | ad6antr 736 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ (ℂ ∖
(ℤ ∖ ℕ))) |
86 | 85 | dmgmn0 25766 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ≠ 0) |
87 | 84, 86 | absrpcld 14901 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ+) |
88 | 59 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℝ+) |
89 | 87, 88 | rpaddcld 12532 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
((abs‘𝐴) + 𝑎) ∈
ℝ+) |
90 | 81, 89 | ltaddrp2d 12551 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) < (((abs‘𝐴) + 𝑎) + (2 / 𝑎))) |
91 | | simp-4r 784 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) |
92 | 81, 82, 83, 90, 91 | lttrd 10882 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) < 𝑟) |
93 | 67 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (2 /
𝑎) ∈
ℝ+) |
94 | 73 | nnrpd 12515 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑟 ∈
ℝ+) |
95 | 93, 94 | ltrecd 12535 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → ((2 /
𝑎) < 𝑟 ↔ (1 / 𝑟) < (1 / (2 / 𝑎)))) |
96 | 92, 95 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (1 / (2 / 𝑎))) |
97 | | 2cnd 11797 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℂ) |
98 | 88 | rpcnd 12519 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℂ) |
99 | | 2ne0 11823 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ≠
0 |
100 | 99 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 2 ≠
0) |
101 | 88 | rpne0d 12522 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ≠ 0) |
102 | 97, 98, 100, 101 | recdivd 11514 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 / (2 /
𝑎)) = (𝑎 / 2)) |
103 | 96, 102 | breqtrd 5057 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (𝑎 / 2)) |
104 | | eldmgm 25762 |
. . . . . . . . . . . . . . . . 17
⊢ (-𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)) ↔ (-𝑘 ∈ ℂ ∧ ¬ --𝑘 ∈
ℕ0)) |
105 | 104 | simprbi 500 |
. . . . . . . . . . . . . . . 16
⊢ (-𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)) → ¬ --𝑘 ∈ ℕ0) |
106 | 77 | negnegd 11069 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → --𝑘 = 𝑘) |
107 | 106, 76 | eqeltrd 2834 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → --𝑘 ∈
ℕ0) |
108 | 105, 107 | nsyl3 140 |
. . . . . . . . . . . . . . 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 11065 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → -𝑘 ∈
ℂ) |
112 | | elbl2 23146 |
. . . . . . . . . . . . . . . . . 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 23526 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧ -𝑘 ∈ ℂ) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘))) |
115 | 75, 111, 114 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 − -𝑘))) |
116 | 75, 77 | subnegd 11085 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥 − -𝑘) = (𝑥 + 𝑘)) |
117 | 116 | fveq2d 6681 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝑥 −
-𝑘)) = (abs‘(𝑥 + 𝑘))) |
118 | 115, 117 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(abs ∘ − )-𝑘) = (abs‘(𝑥 + 𝑘))) |
119 | 118 | breq1d 5041 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → ((𝑥(abs ∘ − )-𝑘) < (𝑎 / 2) ↔ (abs‘(𝑥 + 𝑘)) < (𝑎 / 2))) |
120 | 79, 80 | ltnled 10868 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) →
((abs‘(𝑥 + 𝑘)) < (𝑎 / 2) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)))) |
121 | 113, 119,
120 | 3bitrd 308 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) ↔ ¬ (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘)))) |
122 | 45 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈
ℝ) |
123 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) |
124 | | elbl3 23148 |
. . . . . . . . . . . . . . . . . . . . 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 260 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2))) |
127 | | blhalf 23161 |
. . . . . . . . . . . . . . . . . . 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 773 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (𝐴(ball‘(abs ∘ − ))𝑎) ⊆ (ℂ ∖
(ℤ ∖ ℕ))) |
130 | 129 | ad5antr 734 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) |
131 | 128, 130 | sstrd 3888 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑥(ball‘(abs ∘ −
))(𝑎 / 2)) ⊆ (ℂ
∖ (ℤ ∖ ℕ))) |
132 | 131 | sseld 3877 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (-𝑘 ∈ (𝑥(ball‘(abs ∘ − ))(𝑎 / 2)) → -𝑘 ∈ (ℂ ∖
(ℤ ∖ ℕ)))) |
133 | 121, 132 | sylbird 263 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (¬
(𝑎 / 2) ≤
(abs‘(𝑥 + 𝑘)) → -𝑘 ∈ (ℂ ∖ (ℤ ∖
ℕ)))) |
134 | 108, 133 | mt3d 150 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (𝑎 / 2) ≤ (abs‘(𝑥 + 𝑘))) |
135 | 74, 80, 79, 103, 134 | ltletrd 10881 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) < (abs‘(𝑥 + 𝑘))) |
136 | 74, 79, 135 | ltled 10869 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) ∧ 𝑘 ∈ ℕ0) → (1 /
𝑟) ≤ (abs‘(𝑥 + 𝑘))) |
137 | 136 | ralrimiva 3097 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))) |
138 | 72, 137 | jca 515 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) ∧ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))) |
139 | 138 | ex 416 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑎 ∈ ℝ+
∧ (𝐴(ball‘(abs
∘ − ))𝑎)
⊆ (ℂ ∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) ∧ 𝑥 ∈ ℂ) → ((𝐴(abs ∘ − )𝑥) < (𝑎 / 2) → ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))))) |
140 | 139 | ss2rabdv 3966 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → {𝑥 ∈ ℂ ∣ (𝐴(abs ∘ − )𝑥) < (𝑎 / 2)} ⊆ {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}) |
141 | | blval 23142 |
. . . . . . . . 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 3925 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → (𝐴(ball‘(abs ∘ − ))(𝑎 / 2)) ⊆ 𝑈) |
145 | 6 | ssntr 21812 |
. . . . . . 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 23169 |
. . . . . . 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 3879 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) ∧ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟) → 𝐴 ∈ ((int‘𝐽)‘𝑈)) |
150 | 149 | ex 416 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) ∧ 𝑟 ∈ ℕ) → ((((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → 𝐴 ∈ ((int‘𝐽)‘𝑈))) |
151 | 150 | reximdva 3185 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → (∃𝑟 ∈ ℕ (((abs‘𝐴) + 𝑎) + (2 / 𝑎)) < 𝑟 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))) |
152 | 25, 151 | mpd 15 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ (𝐴(ball‘(abs ∘ −
))𝑎) ⊆ (ℂ
∖ (ℤ ∖ ℕ)))) → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)) |
153 | 13, 152 | rexlimddv 3202 |
1
⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈)) |