| Step | Hyp | Ref
| Expression |
| 1 | | efopn.j |
. . . . . . . 8
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 2 | 1 | cnfldtopon 24803 |
. . . . . . 7
⊢ 𝐽 ∈
(TopOn‘ℂ) |
| 3 | | toponss 22933 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝑆 ∈ 𝐽) → 𝑆 ⊆ ℂ) |
| 4 | 2, 3 | mpan 690 |
. . . . . 6
⊢ (𝑆 ∈ 𝐽 → 𝑆 ⊆ ℂ) |
| 5 | 4 | sselda 3983 |
. . . . 5
⊢ ((𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℂ) |
| 6 | | cnxmet 24793 |
. . . . . 6
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 7 | | pirp 26503 |
. . . . . . 7
⊢ π
∈ ℝ+ |
| 8 | 1 | cnfldtopn 24802 |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
| 9 | 8 | mopni3 24507 |
. . . . . . 7
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆) ∧ π ∈ ℝ+)
→ ∃𝑟 ∈
ℝ+ (𝑟 <
π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆)) |
| 10 | 7, 9 | mpan2 691 |
. . . . . 6
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆) → ∃𝑟 ∈ ℝ+ (𝑟 < π ∧ (𝑥(ball‘(abs ∘ −
))𝑟) ⊆ 𝑆)) |
| 11 | 6, 10 | mp3an1 1450 |
. . . . 5
⊢ ((𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆) → ∃𝑟 ∈ ℝ+ (𝑟 < π ∧ (𝑥(ball‘(abs ∘ −
))𝑟) ⊆ 𝑆)) |
| 12 | | imass2 6120 |
. . . . . . . 8
⊢ ((𝑥(ball‘(abs ∘ −
))𝑟) ⊆ 𝑆 → (exp “ (𝑥(ball‘(abs ∘ −
))𝑟)) ⊆ (exp “
𝑆)) |
| 13 | | imassrn 6089 |
. . . . . . . . . . . . . 14
⊢ (exp
“ (𝑥(ball‘(abs
∘ − ))𝑟))
⊆ ran exp |
| 14 | | eff 16117 |
. . . . . . . . . . . . . . 15
⊢
exp:ℂ⟶ℂ |
| 15 | | frn 6743 |
. . . . . . . . . . . . . . 15
⊢
(exp:ℂ⟶ℂ → ran exp ⊆
ℂ) |
| 16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ran exp
⊆ ℂ |
| 17 | 13, 16 | sstri 3993 |
. . . . . . . . . . . . 13
⊢ (exp
“ (𝑥(ball‘(abs
∘ − ))𝑟))
⊆ ℂ |
| 18 | | sseqin2 4223 |
. . . . . . . . . . . . 13
⊢ ((exp
“ (𝑥(ball‘(abs
∘ − ))𝑟))
⊆ ℂ ↔ (ℂ ∩ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) = (exp “ (𝑥(ball‘(abs ∘ −
))𝑟))) |
| 19 | 17, 18 | mpbi 230 |
. . . . . . . . . . . 12
⊢ (ℂ
∩ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) = (exp “ (𝑥(ball‘(abs ∘ −
))𝑟)) |
| 20 | | rpxr 13044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
| 21 | | blssm 24428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘(abs ∘ −
))𝑟) ⊆
ℂ) |
| 22 | 6, 21 | mp3an1 1450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ*)
→ (𝑥(ball‘(abs
∘ − ))𝑟)
⊆ ℂ) |
| 23 | 20, 22 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
→ (𝑥(ball‘(abs
∘ − ))𝑟)
⊆ ℂ) |
| 24 | 23 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) ∧
𝑧 ∈ ℂ) →
(𝑥(ball‘(abs ∘
− ))𝑟) ⊆
ℂ) |
| 25 | 24 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑦 ∈ ℂ) |
| 26 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑥 ∈ ℂ) |
| 27 | 25, 26 | subcld 11620 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦 − 𝑥) ∈ ℂ) |
| 28 | 27 | subid1d 11609 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦 − 𝑥) − 0) = (𝑦 − 𝑥)) |
| 29 | 28 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (abs‘((𝑦 − 𝑥) − 0)) = (abs‘(𝑦 − 𝑥))) |
| 30 | | 0cn 11253 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℂ |
| 31 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 32 | 31 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 − 𝑥) ∈ ℂ ∧ 0 ∈ ℂ)
→ ((𝑦 − 𝑥)(abs ∘ − )0) =
(abs‘((𝑦 −
𝑥) −
0))) |
| 33 | 27, 30, 32 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦 − 𝑥)(abs ∘ − )0) =
(abs‘((𝑦 −
𝑥) −
0))) |
| 34 | 31 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑦(abs ∘ − )𝑥) = (abs‘(𝑦 − 𝑥))) |
| 35 | 25, 26, 34 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦(abs ∘ − )𝑥) = (abs‘(𝑦 − 𝑥))) |
| 36 | 29, 33, 35 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦 − 𝑥)(abs ∘ − )0) = (𝑦(abs ∘ − )𝑥)) |
| 37 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) |
| 38 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (abs ∘ − )
∈ (∞Met‘ℂ)) |
| 39 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) ∧
𝑧 ∈ ℂ) →
𝑟 ∈
ℝ+) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑟 ∈ ℝ+) |
| 41 | 40 | rpxrd 13078 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑟 ∈ ℝ*) |
| 42 | | elbl3 24402 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ (𝑦(abs ∘ − )𝑥) < 𝑟)) |
| 43 | 38, 41, 26, 25, 42 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ (𝑦(abs ∘ − )𝑥) < 𝑟)) |
| 44 | 37, 43 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦(abs ∘ − )𝑥) < 𝑟) |
| 45 | 36, 44 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦 − 𝑥)(abs ∘ − )0) < 𝑟) |
| 46 | | 0cnd 11254 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 0 ∈
ℂ) |
| 47 | | elbl3 24402 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (0 ∈
ℂ ∧ (𝑦 −
𝑥) ∈ ℂ)) →
((𝑦 − 𝑥) ∈ (0(ball‘(abs
∘ − ))𝑟) ↔
((𝑦 − 𝑥)(abs ∘ − )0) <
𝑟)) |
| 48 | 38, 41, 46, 27, 47 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦 − 𝑥) ∈ (0(ball‘(abs ∘ −
))𝑟) ↔ ((𝑦 − 𝑥)(abs ∘ − )0) < 𝑟)) |
| 49 | 45, 48 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦 − 𝑥) ∈ (0(ball‘(abs ∘ −
))𝑟)) |
| 50 | | efsub 16136 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(exp‘(𝑦 − 𝑥)) = ((exp‘𝑦) / (exp‘𝑥))) |
| 51 | 25, 26, 50 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (exp‘(𝑦 − 𝑥)) = ((exp‘𝑦) / (exp‘𝑥))) |
| 52 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = (𝑦 − 𝑥) → ((exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)) ↔ (exp‘(𝑦 − 𝑥)) = ((exp‘𝑦) / (exp‘𝑥)))) |
| 53 | 52 | rspcev 3622 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 − 𝑥) ∈ (0(ball‘(abs ∘ −
))𝑟) ∧
(exp‘(𝑦 − 𝑥)) = ((exp‘𝑦) / (exp‘𝑥))) → ∃𝑤 ∈ (0(ball‘(abs
∘ − ))𝑟)(exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥))) |
| 54 | 49, 51, 53 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ∃𝑤 ∈ (0(ball‘(abs
∘ − ))𝑟)(exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥))) |
| 55 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢
((exp‘𝑦) =
𝑧 → ((exp‘𝑦) / (exp‘𝑥)) = (𝑧 / (exp‘𝑥))) |
| 56 | 55 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢
((exp‘𝑦) =
𝑧 → ((exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)) ↔ (exp‘𝑤) = (𝑧 / (exp‘𝑥)))) |
| 57 | 56 | rexbidv 3179 |
. . . . . . . . . . . . . . . . 17
⊢
((exp‘𝑦) =
𝑧 → (∃𝑤 ∈ (0(ball‘(abs
∘ − ))𝑟)(exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)) ↔ ∃𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥)))) |
| 58 | 54, 57 | syl5ibcom 245 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((exp‘𝑦) = 𝑧 → ∃𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥)))) |
| 59 | 58 | rexlimdva 3155 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) ∧
𝑧 ∈ ℂ) →
(∃𝑦 ∈ (𝑥(ball‘(abs ∘ −
))𝑟)(exp‘𝑦) = 𝑧 → ∃𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥)))) |
| 60 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . 18
⊢
((exp‘𝑤) =
(𝑧 / (exp‘𝑥)) ↔ (𝑧 / (exp‘𝑥)) = (exp‘𝑤)) |
| 61 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → 𝑧 ∈
ℂ) |
| 62 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → 𝑥 ∈
ℂ) |
| 63 | | efcl 16118 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
| 64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) →
(exp‘𝑥) ∈
ℂ) |
| 65 | 39 | rpxrd 13078 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) ∧
𝑧 ∈ ℂ) →
𝑟 ∈
ℝ*) |
| 66 | | blssm 24428 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 𝑟 ∈
ℝ*) → (0(ball‘(abs ∘ − ))𝑟) ⊆
ℂ) |
| 67 | 6, 30, 65, 66 | mp3an12i 1467 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) ∧
𝑧 ∈ ℂ) →
(0(ball‘(abs ∘ − ))𝑟) ⊆ ℂ) |
| 68 | 67 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → 𝑤 ∈
ℂ) |
| 69 | | efcl 16118 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ ℂ →
(exp‘𝑤) ∈
ℂ) |
| 70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) →
(exp‘𝑤) ∈
ℂ) |
| 71 | | efne0 16133 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ≠
0) |
| 72 | 62, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) →
(exp‘𝑥) ≠
0) |
| 73 | 61, 64, 70, 72 | divmuld 12065 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → ((𝑧 / (exp‘𝑥)) = (exp‘𝑤) ↔ ((exp‘𝑥) · (exp‘𝑤)) = 𝑧)) |
| 74 | 60, 73 | bitrid 283 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) →
((exp‘𝑤) = (𝑧 / (exp‘𝑥)) ↔ ((exp‘𝑥) · (exp‘𝑤)) = 𝑧)) |
| 75 | 62, 68 | pncan2d 11622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → ((𝑥 + 𝑤) − 𝑥) = 𝑤) |
| 76 | 68 | subid1d 11609 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → (𝑤 − 0) = 𝑤) |
| 77 | 75, 76 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → ((𝑥 + 𝑤) − 𝑥) = (𝑤 − 0)) |
| 78 | 77 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) →
(abs‘((𝑥 + 𝑤) − 𝑥)) = (abs‘(𝑤 − 0))) |
| 79 | 62, 68 | addcld 11280 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → (𝑥 + 𝑤) ∈ ℂ) |
| 80 | 31 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 + 𝑤) ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) = (abs‘((𝑥 + 𝑤) − 𝑥))) |
| 81 | 79, 62, 80 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) = (abs‘((𝑥 + 𝑤) − 𝑥))) |
| 82 | 31 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑤(abs
∘ − )0) = (abs‘(𝑤 − 0))) |
| 83 | 68, 30, 82 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → (𝑤(abs ∘ − )0) =
(abs‘(𝑤 −
0))) |
| 84 | 78, 81, 83 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) = (𝑤(abs ∘ − )0)) |
| 85 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → 𝑤 ∈ (0(ball‘(abs
∘ − ))𝑟)) |
| 86 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → (abs ∘
− ) ∈ (∞Met‘ℂ)) |
| 87 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → 𝑟 ∈
ℝ+) |
| 88 | 87 | rpxrd 13078 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → 𝑟 ∈
ℝ*) |
| 89 | | 0cnd 11254 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → 0 ∈
ℂ) |
| 90 | | elbl3 24402 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (0 ∈
ℂ ∧ 𝑤 ∈
ℂ)) → (𝑤 ∈
(0(ball‘(abs ∘ − ))𝑟) ↔ (𝑤(abs ∘ − )0) < 𝑟)) |
| 91 | 86, 88, 89, 68, 90 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → (𝑤 ∈ (0(ball‘(abs
∘ − ))𝑟) ↔
(𝑤(abs ∘ − )0)
< 𝑟)) |
| 92 | 85, 91 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → (𝑤(abs ∘ − )0) <
𝑟) |
| 93 | 84, 92 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) < 𝑟) |
| 94 | | elbl3 24402 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑥 ∈ ℂ ∧ (𝑥 + 𝑤) ∈ ℂ)) → ((𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥 + 𝑤)(abs ∘ − )𝑥) < 𝑟)) |
| 95 | 86, 88, 62, 79, 94 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → ((𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥 + 𝑤)(abs ∘ − )𝑥) < 𝑟)) |
| 96 | 93, 95 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → (𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) |
| 97 | | efadd 16130 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤))) |
| 98 | 62, 68, 97 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) →
(exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤))) |
| 99 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑥 + 𝑤) → ((exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)) ↔ (exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤)))) |
| 100 | 99 | rspcev 3622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ∧ (exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤))) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤))) |
| 101 | 96, 98, 100 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤))) |
| 102 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((exp‘𝑥)
· (exp‘𝑤)) =
𝑧 → ((exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)) ↔ (exp‘𝑦) = 𝑧)) |
| 103 | 102 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . 18
⊢
(((exp‘𝑥)
· (exp‘𝑤)) =
𝑧 → (∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)) ↔ ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧)) |
| 104 | 101, 103 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) →
(((exp‘𝑥) ·
(exp‘𝑤)) = 𝑧 → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧)) |
| 105 | 74, 104 | sylbid 240 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑥 ∈
ℂ ∧ 𝑟 ∈
ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)) →
((exp‘𝑤) = (𝑧 / (exp‘𝑥)) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧)) |
| 106 | 105 | rexlimdva 3155 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) ∧
𝑧 ∈ ℂ) →
(∃𝑤 ∈
(0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥)) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧)) |
| 107 | 59, 106 | impbid 212 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) ∧
𝑧 ∈ ℂ) →
(∃𝑦 ∈ (𝑥(ball‘(abs ∘ −
))𝑟)(exp‘𝑦) = 𝑧 ↔ ∃𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥)))) |
| 108 | | ffn 6736 |
. . . . . . . . . . . . . . . 16
⊢
(exp:ℂ⟶ℂ → exp Fn ℂ) |
| 109 | 14, 108 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ exp Fn
ℂ |
| 110 | | fvelimab 6981 |
. . . . . . . . . . . . . . 15
⊢ ((exp Fn
ℂ ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ ℂ) → (𝑧 ∈ (exp “ (𝑥(ball‘(abs ∘ −
))𝑟)) ↔ ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧)) |
| 111 | 109, 24, 110 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) ∧
𝑧 ∈ ℂ) →
(𝑧 ∈ (exp “
(𝑥(ball‘(abs ∘
− ))𝑟)) ↔
∃𝑦 ∈ (𝑥(ball‘(abs ∘ −
))𝑟)(exp‘𝑦) = 𝑧)) |
| 112 | | fvelimab 6981 |
. . . . . . . . . . . . . . 15
⊢ ((exp Fn
ℂ ∧ (0(ball‘(abs ∘ − ))𝑟) ⊆ ℂ) → ((𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs
∘ − ))𝑟))
↔ ∃𝑤 ∈
(0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥)))) |
| 113 | 109, 67, 112 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) ∧
𝑧 ∈ ℂ) →
((𝑧 / (exp‘𝑥)) ∈ (exp “
(0(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (0(ball‘(abs ∘ −
))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥)))) |
| 114 | 107, 111,
113 | 3bitr4d 311 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) ∧
𝑧 ∈ ℂ) →
(𝑧 ∈ (exp “
(𝑥(ball‘(abs ∘
− ))𝑟)) ↔ (𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs
∘ − ))𝑟)))) |
| 115 | 114 | rabbi2dva 4226 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
(ℂ ∩ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) = {𝑧 ∈ ℂ ∣ (𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs
∘ − ))𝑟))}) |
| 116 | 19, 115 | eqtr3id 2791 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
(exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) = {𝑧 ∈ ℂ ∣ (𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs
∘ − ))𝑟))}) |
| 117 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) = (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) |
| 118 | 117 | mptpreima 6258 |
. . . . . . . . . . 11
⊢ (◡(𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs
∘ − ))𝑟))) =
{𝑧 ∈ ℂ ∣
(𝑧 / (exp‘𝑥)) ∈ (exp “
(0(ball‘(abs ∘ − ))𝑟))} |
| 119 | 116, 118 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
(exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) = (◡(𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs
∘ − ))𝑟)))) |
| 120 | 63 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
(exp‘𝑥) ∈
ℂ) |
| 121 | 71 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
(exp‘𝑥) ≠
0) |
| 122 | 117 | divccncf 24932 |
. . . . . . . . . . . . 13
⊢
(((exp‘𝑥)
∈ ℂ ∧ (exp‘𝑥) ≠ 0) → (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) ∈ (ℂ–cn→ℂ)) |
| 123 | 120, 121,
122 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
(𝑧 ∈ ℂ ↦
(𝑧 / (exp‘𝑥))) ∈ (ℂ–cn→ℂ)) |
| 124 | 1 | cncfcn1 24937 |
. . . . . . . . . . . 12
⊢
(ℂ–cn→ℂ) =
(𝐽 Cn 𝐽) |
| 125 | 123, 124 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
(𝑧 ∈ ℂ ↦
(𝑧 / (exp‘𝑥))) ∈ (𝐽 Cn 𝐽)) |
| 126 | 1 | efopnlem2 26699 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ ℝ+
∧ 𝑟 < π) →
(exp “ (0(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽) |
| 127 | 126 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
(exp “ (0(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽) |
| 128 | | cnima 23273 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) ∈ (𝐽 Cn 𝐽) ∧ (exp “ (0(ball‘(abs
∘ − ))𝑟))
∈ 𝐽) → (◡(𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs
∘ − ))𝑟)))
∈ 𝐽) |
| 129 | 125, 127,
128 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
(◡(𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs
∘ − ))𝑟)))
∈ 𝐽) |
| 130 | 119, 129 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
(exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽) |
| 131 | | blcntr 24423 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) |
| 132 | 6, 131 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
→ 𝑥 ∈ (𝑥(ball‘(abs ∘ −
))𝑟)) |
| 133 | | ffun 6739 |
. . . . . . . . . . . . 13
⊢
(exp:ℂ⟶ℂ → Fun exp) |
| 134 | 14, 133 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun
exp |
| 135 | 14 | fdmi 6747 |
. . . . . . . . . . . . 13
⊢ dom exp =
ℂ |
| 136 | 23, 135 | sseqtrrdi 4025 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
→ (𝑥(ball‘(abs
∘ − ))𝑟)
⊆ dom exp) |
| 137 | | funfvima2 7251 |
. . . . . . . . . . . 12
⊢ ((Fun exp
∧ (𝑥(ball‘(abs
∘ − ))𝑟)
⊆ dom exp) → (𝑥
∈ (𝑥(ball‘(abs
∘ − ))𝑟) →
(exp‘𝑥) ∈ (exp
“ (𝑥(ball‘(abs
∘ − ))𝑟)))) |
| 138 | 134, 136,
137 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
→ (𝑥 ∈ (𝑥(ball‘(abs ∘ −
))𝑟) →
(exp‘𝑥) ∈ (exp
“ (𝑥(ball‘(abs
∘ − ))𝑟)))) |
| 139 | 132, 138 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
→ (exp‘𝑥) ∈
(exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) |
| 140 | 139 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
(exp‘𝑥) ∈ (exp
“ (𝑥(ball‘(abs
∘ − ))𝑟))) |
| 141 | | eleq2 2830 |
. . . . . . . . . . . 12
⊢ (𝑦 = (exp “ (𝑥(ball‘(abs ∘ −
))𝑟)) →
((exp‘𝑥) ∈ 𝑦 ↔ (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ −
))𝑟)))) |
| 142 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑦 = (exp “ (𝑥(ball‘(abs ∘ −
))𝑟)) → (𝑦 ⊆ (exp “ 𝑆) ↔ (exp “ (𝑥(ball‘(abs ∘ −
))𝑟)) ⊆ (exp “
𝑆))) |
| 143 | 141, 142 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑦 = (exp “ (𝑥(ball‘(abs ∘ −
))𝑟)) →
(((exp‘𝑥) ∈
𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)) ↔ ((exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∧ (exp “ (𝑥(ball‘(abs ∘ −
))𝑟)) ⊆ (exp “
𝑆)))) |
| 144 | 143 | rspcev 3622 |
. . . . . . . . . 10
⊢ (((exp
“ (𝑥(ball‘(abs
∘ − ))𝑟))
∈ 𝐽 ∧
((exp‘𝑥) ∈ (exp
“ (𝑥(ball‘(abs
∘ − ))𝑟)) ∧
(exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆))) → ∃𝑦 ∈ 𝐽 ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆))) |
| 145 | 144 | expr 456 |
. . . . . . . . 9
⊢ (((exp
“ (𝑥(ball‘(abs
∘ − ))𝑟))
∈ 𝐽 ∧
(exp‘𝑥) ∈ (exp
“ (𝑥(ball‘(abs
∘ − ))𝑟)))
→ ((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆) → ∃𝑦 ∈ 𝐽 ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)))) |
| 146 | 130, 140,
145 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆) → ∃𝑦 ∈ 𝐽 ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)))) |
| 147 | 12, 146 | syl5 34 |
. . . . . . 7
⊢ (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
∧ 𝑟 < π) →
((𝑥(ball‘(abs ∘
− ))𝑟) ⊆ 𝑆 → ∃𝑦 ∈ 𝐽 ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)))) |
| 148 | 147 | expimpd 453 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+)
→ ((𝑟 < π ∧
(𝑥(ball‘(abs ∘
− ))𝑟) ⊆ 𝑆) → ∃𝑦 ∈ 𝐽 ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)))) |
| 149 | 148 | rexlimdva 3155 |
. . . . 5
⊢ (𝑥 ∈ ℂ →
(∃𝑟 ∈
ℝ+ (𝑟 <
π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆) → ∃𝑦 ∈ 𝐽 ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)))) |
| 150 | 5, 11, 149 | sylc 65 |
. . . 4
⊢ ((𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝐽 ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆))) |
| 151 | 150 | ralrimiva 3146 |
. . 3
⊢ (𝑆 ∈ 𝐽 → ∀𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝐽 ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆))) |
| 152 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑧 = (exp‘𝑥) → (𝑧 ∈ 𝑦 ↔ (exp‘𝑥) ∈ 𝑦)) |
| 153 | 152 | anbi1d 631 |
. . . . . 6
⊢ (𝑧 = (exp‘𝑥) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)) ↔ ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)))) |
| 154 | 153 | rexbidv 3179 |
. . . . 5
⊢ (𝑧 = (exp‘𝑥) → (∃𝑦 ∈ 𝐽 (𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)) ↔ ∃𝑦 ∈ 𝐽 ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)))) |
| 155 | 154 | ralima 7257 |
. . . 4
⊢ ((exp Fn
ℂ ∧ 𝑆 ⊆
ℂ) → (∀𝑧
∈ (exp “ 𝑆)∃𝑦 ∈ 𝐽 (𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)) ↔ ∀𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝐽 ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)))) |
| 156 | 109, 4, 155 | sylancr 587 |
. . 3
⊢ (𝑆 ∈ 𝐽 → (∀𝑧 ∈ (exp “ 𝑆)∃𝑦 ∈ 𝐽 (𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)) ↔ ∀𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝐽 ((exp‘𝑥) ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)))) |
| 157 | 151, 156 | mpbird 257 |
. 2
⊢ (𝑆 ∈ 𝐽 → ∀𝑧 ∈ (exp “ 𝑆)∃𝑦 ∈ 𝐽 (𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆))) |
| 158 | 1 | cnfldtop 24804 |
. . 3
⊢ 𝐽 ∈ Top |
| 159 | | eltop2 22982 |
. . 3
⊢ (𝐽 ∈ Top → ((exp “
𝑆) ∈ 𝐽 ↔ ∀𝑧 ∈ (exp “ 𝑆)∃𝑦 ∈ 𝐽 (𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆)))) |
| 160 | 158, 159 | ax-mp 5 |
. 2
⊢ ((exp
“ 𝑆) ∈ 𝐽 ↔ ∀𝑧 ∈ (exp “ 𝑆)∃𝑦 ∈ 𝐽 (𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ (exp “ 𝑆))) |
| 161 | 157, 160 | sylibr 234 |
1
⊢ (𝑆 ∈ 𝐽 → (exp “ 𝑆) ∈ 𝐽) |