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

Theorem efopn 24942
Description: The exponential map is an open map. (Contributed by Mario Carneiro, 23-Apr-2015.)
Hypothesis
Ref Expression
efopn.j 𝐽 = (TopOpen‘ℂfld)
Assertion
Ref Expression
efopn (𝑆𝐽 → (exp “ 𝑆) ∈ 𝐽)

Proof of Theorem efopn
Dummy variables 𝑤 𝑟 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efopn.j . . . . . . . 8 𝐽 = (TopOpen‘ℂfld)
21cnfldtopon 23094 . . . . . . 7 𝐽 ∈ (TopOn‘ℂ)
3 toponss 21239 . . . . . . 7 ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆𝐽) → 𝑆 ⊆ ℂ)
42, 3mpan 677 . . . . . 6 (𝑆𝐽𝑆 ⊆ ℂ)
54sselda 3858 . . . . 5 ((𝑆𝐽𝑥𝑆) → 𝑥 ∈ ℂ)
6 cnxmet 23084 . . . . . 6 (abs ∘ − ) ∈ (∞Met‘ℂ)
7 pirp 24750 . . . . . . 7 π ∈ ℝ+
81cnfldtopn 23093 . . . . . . . 8 𝐽 = (MetOpen‘(abs ∘ − ))
98mopni3 22807 . . . . . . 7 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆𝐽𝑥𝑆) ∧ π ∈ ℝ+) → ∃𝑟 ∈ ℝ+ (𝑟 < π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆))
107, 9mpan2 678 . . . . . 6 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆𝐽𝑥𝑆) → ∃𝑟 ∈ ℝ+ (𝑟 < π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆))
116, 10mp3an1 1427 . . . . 5 ((𝑆𝐽𝑥𝑆) → ∃𝑟 ∈ ℝ+ (𝑟 < π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆))
12 imass2 5805 . . . . . . . 8 ((𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆 → (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆))
13 imassrn 5781 . . . . . . . . . . . . . 14 (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ ran exp
14 eff 15295 . . . . . . . . . . . . . . 15 exp:ℂ⟶ℂ
15 frn 6350 . . . . . . . . . . . . . . 15 (exp:ℂ⟶ℂ → ran exp ⊆ ℂ)
1614, 15ax-mp 5 . . . . . . . . . . . . . 14 ran exp ⊆ ℂ
1713, 16sstri 3867 . . . . . . . . . . . . 13 (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ ℂ
18 sseqin2 4079 . . . . . . . . . . . . 13 ((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ ℂ ↔ (ℂ ∩ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) = (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)))
1917, 18mpbi 222 . . . . . . . . . . . 12 (ℂ ∩ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) = (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))
20 rpxr 12215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
21 blssm 22731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
226, 21mp3an1 1427 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
2320, 22sylan2 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
2423ad2antrr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
2524sselda 3858 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑦 ∈ ℂ)
26 simp-4l 770 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑥 ∈ ℂ)
2725, 26subcld 10798 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦𝑥) ∈ ℂ)
2827subid1d 10787 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦𝑥) − 0) = (𝑦𝑥))
2928fveq2d 6503 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (abs‘((𝑦𝑥) − 0)) = (abs‘(𝑦𝑥)))
30 0cn 10431 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℂ
31 eqid 2778 . . . . . . . . . . . . . . . . . . . . . . 23 (abs ∘ − ) = (abs ∘ − )
3231cnmetdval 23082 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑦𝑥)(abs ∘ − )0) = (abs‘((𝑦𝑥) − 0)))
3327, 30, 32sylancl 577 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦𝑥)(abs ∘ − )0) = (abs‘((𝑦𝑥) − 0)))
3431cnmetdval 23082 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑦(abs ∘ − )𝑥) = (abs‘(𝑦𝑥)))
3525, 26, 34syl2anc 576 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦(abs ∘ − )𝑥) = (abs‘(𝑦𝑥)))
3629, 33, 353eqtr4d 2824 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦𝑥)(abs ∘ − )0) = (𝑦(abs ∘ − )𝑥))
37 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
386a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
39 simpllr 763 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → 𝑟 ∈ ℝ+)
4039adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑟 ∈ ℝ+)
4140rpxrd 12249 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑟 ∈ ℝ*)
42 elbl3 22705 . . . . . . . . . . . . . . . . . . . . . 22 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ (𝑦(abs ∘ − )𝑥) < 𝑟))
4338, 41, 26, 25, 42syl22anc 826 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ (𝑦(abs ∘ − )𝑥) < 𝑟))
4437, 43mpbid 224 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦(abs ∘ − )𝑥) < 𝑟)
4536, 44eqbrtrd 4951 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦𝑥)(abs ∘ − )0) < 𝑟)
46 0cnd 10432 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 0 ∈ ℂ)
47 elbl3 22705 . . . . . . . . . . . . . . . . . . . 20 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ (𝑦𝑥) ∈ ℂ)) → ((𝑦𝑥) ∈ (0(ball‘(abs ∘ − ))𝑟) ↔ ((𝑦𝑥)(abs ∘ − )0) < 𝑟))
4838, 41, 46, 27, 47syl22anc 826 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦𝑥) ∈ (0(ball‘(abs ∘ − ))𝑟) ↔ ((𝑦𝑥)(abs ∘ − )0) < 𝑟))
4945, 48mpbird 249 . . . . . . . . . . . . . . . . . 18 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦𝑥) ∈ (0(ball‘(abs ∘ − ))𝑟))
50 efsub 15313 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (exp‘(𝑦𝑥)) = ((exp‘𝑦) / (exp‘𝑥)))
5125, 26, 50syl2anc 576 . . . . . . . . . . . . . . . . . 18 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (exp‘(𝑦𝑥)) = ((exp‘𝑦) / (exp‘𝑥)))
52 fveqeq2 6508 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝑦𝑥) → ((exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)) ↔ (exp‘(𝑦𝑥)) = ((exp‘𝑦) / (exp‘𝑥))))
5352rspcev 3535 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥) ∈ (0(ball‘(abs ∘ − ))𝑟) ∧ (exp‘(𝑦𝑥)) = ((exp‘𝑦) / (exp‘𝑥))) → ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)))
5449, 51, 53syl2anc 576 . . . . . . . . . . . . . . . . 17 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)))
55 oveq1 6983 . . . . . . . . . . . . . . . . . . 19 ((exp‘𝑦) = 𝑧 → ((exp‘𝑦) / (exp‘𝑥)) = (𝑧 / (exp‘𝑥)))
5655eqeq2d 2788 . . . . . . . . . . . . . . . . . 18 ((exp‘𝑦) = 𝑧 → ((exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)) ↔ (exp‘𝑤) = (𝑧 / (exp‘𝑥))))
5756rexbidv 3242 . . . . . . . . . . . . . . . . 17 ((exp‘𝑦) = 𝑧 → (∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)) ↔ ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
5854, 57syl5ibcom 237 . . . . . . . . . . . . . . . 16 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((exp‘𝑦) = 𝑧 → ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
5958rexlimdva 3229 . . . . . . . . . . . . . . 15 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧 → ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
60 eqcom 2785 . . . . . . . . . . . . . . . . . 18 ((exp‘𝑤) = (𝑧 / (exp‘𝑥)) ↔ (𝑧 / (exp‘𝑥)) = (exp‘𝑤))
61 simplr 756 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑧 ∈ ℂ)
62 simp-4l 770 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑥 ∈ ℂ)
63 efcl 15296 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ → (exp‘𝑥) ∈ ℂ)
6462, 63syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (exp‘𝑥) ∈ ℂ)
6539rpxrd 12249 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → 𝑟 ∈ ℝ*)
66 blssm 22731 . . . . . . . . . . . . . . . . . . . . . 22 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (0(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
676, 30, 65, 66mp3an12i 1444 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (0(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
6867sselda 3858 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑤 ∈ ℂ)
69 efcl 15296 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℂ → (exp‘𝑤) ∈ ℂ)
7068, 69syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (exp‘𝑤) ∈ ℂ)
71 efne0 15310 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ → (exp‘𝑥) ≠ 0)
7262, 71syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (exp‘𝑥) ≠ 0)
7361, 64, 70, 72divmuld 11239 . . . . . . . . . . . . . . . . . 18 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑧 / (exp‘𝑥)) = (exp‘𝑤) ↔ ((exp‘𝑥) · (exp‘𝑤)) = 𝑧))
7460, 73syl5bb 275 . . . . . . . . . . . . . . . . 17 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((exp‘𝑤) = (𝑧 / (exp‘𝑥)) ↔ ((exp‘𝑥) · (exp‘𝑤)) = 𝑧))
7562, 68pncan2d 10800 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤) − 𝑥) = 𝑤)
7668subid1d 10787 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑤 − 0) = 𝑤)
7775, 76eqtr4d 2817 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤) − 𝑥) = (𝑤 − 0))
7877fveq2d 6503 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (abs‘((𝑥 + 𝑤) − 𝑥)) = (abs‘(𝑤 − 0)))
7962, 68addcld 10459 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑥 + 𝑤) ∈ ℂ)
8031cnmetdval 23082 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 + 𝑤) ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) = (abs‘((𝑥 + 𝑤) − 𝑥)))
8179, 62, 80syl2anc 576 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) = (abs‘((𝑥 + 𝑤) − 𝑥)))
8231cnmetdval 23082 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑤(abs ∘ − )0) = (abs‘(𝑤 − 0)))
8368, 30, 82sylancl 577 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑤(abs ∘ − )0) = (abs‘(𝑤 − 0)))
8478, 81, 833eqtr4d 2824 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) = (𝑤(abs ∘ − )0))
85 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟))
866a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
8739adantr 473 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑟 ∈ ℝ+)
8887rpxrd 12249 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑟 ∈ ℝ*)
89 0cnd 10432 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 0 ∈ ℂ)
90 elbl3 22705 . . . . . . . . . . . . . . . . . . . . . . 23 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟) ↔ (𝑤(abs ∘ − )0) < 𝑟))
9186, 88, 89, 68, 90syl22anc 826 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟) ↔ (𝑤(abs ∘ − )0) < 𝑟))
9285, 91mpbid 224 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑤(abs ∘ − )0) < 𝑟)
9384, 92eqbrtrd 4951 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) < 𝑟)
94 elbl3 22705 . . . . . . . . . . . . . . . . . . . . 21 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑥 ∈ ℂ ∧ (𝑥 + 𝑤) ∈ ℂ)) → ((𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥 + 𝑤)(abs ∘ − )𝑥) < 𝑟))
9586, 88, 62, 79, 94syl22anc 826 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥 + 𝑤)(abs ∘ − )𝑥) < 𝑟))
9693, 95mpbird 249 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
97 efadd 15307 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤)))
9862, 68, 97syl2anc 576 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤)))
99 fveqeq2 6508 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑥 + 𝑤) → ((exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)) ↔ (exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤))))
10099rspcev 3535 . . . . . . . . . . . . . . . . . . 19 (((𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ∧ (exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤))) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)))
10196, 98, 100syl2anc 576 . . . . . . . . . . . . . . . . . 18 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)))
102 eqeq2 2789 . . . . . . . . . . . . . . . . . . 19 (((exp‘𝑥) · (exp‘𝑤)) = 𝑧 → ((exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)) ↔ (exp‘𝑦) = 𝑧))
103102rexbidv 3242 . . . . . . . . . . . . . . . . . 18 (((exp‘𝑥) · (exp‘𝑤)) = 𝑧 → (∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)) ↔ ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
104101, 103syl5ibcom 237 . . . . . . . . . . . . . . . . 17 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (((exp‘𝑥) · (exp‘𝑤)) = 𝑧 → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
10574, 104sylbid 232 . . . . . . . . . . . . . . . 16 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((exp‘𝑤) = (𝑧 / (exp‘𝑥)) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
106105rexlimdva 3229 . . . . . . . . . . . . . . 15 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥)) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
10759, 106impbid 204 . . . . . . . . . . . . . 14 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧 ↔ ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
108 ffn 6344 . . . . . . . . . . . . . . . 16 (exp:ℂ⟶ℂ → exp Fn ℂ)
10914, 108ax-mp 5 . . . . . . . . . . . . . . 15 exp Fn ℂ
110 fvelimab 6566 . . . . . . . . . . . . . . 15 ((exp Fn ℂ ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ ℂ) → (𝑧 ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
111109, 24, 110sylancr 578 . . . . . . . . . . . . . 14 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (𝑧 ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
112 fvelimab 6566 . . . . . . . . . . . . . . 15 ((exp Fn ℂ ∧ (0(ball‘(abs ∘ − ))𝑟) ⊆ ℂ) → ((𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
113109, 67, 112sylancr 578 . . . . . . . . . . . . . 14 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → ((𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
114107, 111, 1133bitr4d 303 . . . . . . . . . . . . 13 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (𝑧 ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ↔ (𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟))))
115114rabbi2dva 4081 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (ℂ ∩ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) = {𝑧 ∈ ℂ ∣ (𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟))})
11619, 115syl5eqr 2828 . . . . . . . . . . 11 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) = {𝑧 ∈ ℂ ∣ (𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟))})
117 eqid 2778 . . . . . . . . . . . 12 (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) = (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥)))
118117mptpreima 5931 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs ∘ − ))𝑟))) = {𝑧 ∈ ℂ ∣ (𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟))}
119116, 118syl6eqr 2832 . . . . . . . . . 10 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) = ((𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs ∘ − ))𝑟))))
12063ad2antrr 713 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp‘𝑥) ∈ ℂ)
12171ad2antrr 713 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp‘𝑥) ≠ 0)
122117divccncf 23217 . . . . . . . . . . . . 13 (((exp‘𝑥) ∈ ℂ ∧ (exp‘𝑥) ≠ 0) → (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) ∈ (ℂ–cn→ℂ))
123120, 121, 122syl2anc 576 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) ∈ (ℂ–cn→ℂ))
1241cncfcn1 23221 . . . . . . . . . . . 12 (ℂ–cn→ℂ) = (𝐽 Cn 𝐽)
125123, 124syl6eleq 2876 . . . . . . . . . . 11 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) ∈ (𝐽 Cn 𝐽))
1261efopnlem2 24941 . . . . . . . . . . . 12 ((𝑟 ∈ ℝ+𝑟 < π) → (exp “ (0(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽)
127126adantll 701 . . . . . . . . . . 11 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp “ (0(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽)
128 cnima 21577 . . . . . . . . . . 11 (((𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) ∈ (𝐽 Cn 𝐽) ∧ (exp “ (0(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽) → ((𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs ∘ − ))𝑟))) ∈ 𝐽)
129125, 127, 128syl2anc 576 . . . . . . . . . 10 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → ((𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs ∘ − ))𝑟))) ∈ 𝐽)
130119, 129eqeltrd 2866 . . . . . . . . 9 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽)
131 blcntr 22726 . . . . . . . . . . . 12 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
1326, 131mp3an1 1427 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
133 ffun 6347 . . . . . . . . . . . . 13 (exp:ℂ⟶ℂ → Fun exp)
13414, 133ax-mp 5 . . . . . . . . . . . 12 Fun exp
13514fdmi 6354 . . . . . . . . . . . . 13 dom exp = ℂ
13623, 135syl6sseqr 3908 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ dom exp)
137 funfvima2 6819 . . . . . . . . . . . 12 ((Fun exp ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ dom exp) → (𝑥 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) → (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))))
138134, 136, 137sylancr 578 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → (𝑥 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) → (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))))
139132, 138mpd 15 . . . . . . . . . 10 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)))
140139adantr 473 . . . . . . . . 9 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)))
141 eleq2 2854 . . . . . . . . . . . 12 (𝑦 = (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((exp‘𝑥) ∈ 𝑦 ↔ (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))))
142 sseq1 3882 . . . . . . . . . . . 12 (𝑦 = (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦 ⊆ (exp “ 𝑆) ↔ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆)))
143141, 142anbi12d 621 . . . . . . . . . . 11 (𝑦 = (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) → (((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆)) ↔ ((exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∧ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆))))
144143rspcev 3535 . . . . . . . . . 10 (((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽 ∧ ((exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∧ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆))) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆)))
145144expr 449 . . . . . . . . 9 (((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽 ∧ (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) → ((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
146130, 140, 145syl2anc 576 . . . . . . . 8 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → ((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
14712, 146syl5 34 . . . . . . 7 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → ((𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆 → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
148147expimpd 446 . . . . . 6 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → ((𝑟 < π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
149148rexlimdva 3229 . . . . 5 (𝑥 ∈ ℂ → (∃𝑟 ∈ ℝ+ (𝑟 < π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
1505, 11, 149sylc 65 . . . 4 ((𝑆𝐽𝑥𝑆) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆)))
151150ralrimiva 3132 . . 3 (𝑆𝐽 → ∀𝑥𝑆𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆)))
152 eleq1 2853 . . . . . . 7 (𝑧 = (exp‘𝑥) → (𝑧𝑦 ↔ (exp‘𝑥) ∈ 𝑦))
153152anbi1d 620 . . . . . 6 (𝑧 = (exp‘𝑥) → ((𝑧𝑦𝑦 ⊆ (exp “ 𝑆)) ↔ ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
154153rexbidv 3242 . . . . 5 (𝑧 = (exp‘𝑥) → (∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆)) ↔ ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
155154ralima 6825 . . . 4 ((exp Fn ℂ ∧ 𝑆 ⊆ ℂ) → (∀𝑧 ∈ (exp “ 𝑆)∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆)) ↔ ∀𝑥𝑆𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
156109, 4, 155sylancr 578 . . 3 (𝑆𝐽 → (∀𝑧 ∈ (exp “ 𝑆)∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆)) ↔ ∀𝑥𝑆𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
157151, 156mpbird 249 . 2 (𝑆𝐽 → ∀𝑧 ∈ (exp “ 𝑆)∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆)))
1581cnfldtop 23095 . . 3 𝐽 ∈ Top
159 eltop2 21287 . . 3 (𝐽 ∈ Top → ((exp “ 𝑆) ∈ 𝐽 ↔ ∀𝑧 ∈ (exp “ 𝑆)∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆))))
160158, 159ax-mp 5 . 2 ((exp “ 𝑆) ∈ 𝐽 ↔ ∀𝑧 ∈ (exp “ 𝑆)∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆)))
161157, 160sylibr 226 1 (𝑆𝐽 → (exp “ 𝑆) ∈ 𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2050  wne 2967  wral 3088  wrex 3089  {crab 3092  cin 3828  wss 3829   class class class wbr 4929  cmpt 5008  ccnv 5406  dom cdm 5407  ran crn 5408  cima 5410  ccom 5411  Fun wfun 6182   Fn wfn 6183  wf 6184  cfv 6188  (class class class)co 6976  cc 10333  0cc0 10335   + caddc 10338   · cmul 10340  *cxr 10473   < clt 10474  cmin 10670   / cdiv 11098  +crp 12204  abscabs 14454  expce 15275  πcpi 15280  TopOpenctopn 16551  ∞Metcxmet 20232  ballcbl 20234  fldccnfld 20247  Topctop 21205  TopOnctopon 21222   Cn ccn 21536  cnccncf 23187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-inf2 8898  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412  ax-pre-sup 10413  ax-addf 10414  ax-mulf 10415
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-iin 4795  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-se 5367  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-isom 6197  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-of 7227  df-om 7397  df-1st 7501  df-2nd 7502  df-supp 7634  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-1o 7905  df-2o 7906  df-oadd 7909  df-er 8089  df-map 8208  df-pm 8209  df-ixp 8260  df-en 8307  df-dom 8308  df-sdom 8309  df-fin 8310  df-fsupp 8629  df-fi 8670  df-sup 8701  df-inf 8702  df-oi 8769  df-card 9162  df-cda 9388  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-div 11099  df-nn 11440  df-2 11503  df-3 11504  df-4 11505  df-5 11506  df-6 11507  df-7 11508  df-8 11509  df-9 11510  df-n0 11708  df-z 11794  df-dec 11912  df-uz 12059  df-q 12163  df-rp 12205  df-xneg 12324  df-xadd 12325  df-xmul 12326  df-ioo 12558  df-ioc 12559  df-ico 12560  df-icc 12561  df-fz 12709  df-fzo 12850  df-fl 12977  df-mod 13053  df-seq 13185  df-exp 13245  df-fac 13449  df-bc 13478  df-hash 13506  df-shft 14287  df-cj 14319  df-re 14320  df-im 14321  df-sqrt 14455  df-abs 14456  df-limsup 14689  df-clim 14706  df-rlim 14707  df-sum 14904  df-ef 15281  df-sin 15283  df-cos 15284  df-tan 15285  df-pi 15286  df-struct 16341  df-ndx 16342  df-slot 16343  df-base 16345  df-sets 16346  df-ress 16347  df-plusg 16434  df-mulr 16435  df-starv 16436  df-sca 16437  df-vsca 16438  df-ip 16439  df-tset 16440  df-ple 16441  df-ds 16443  df-unif 16444  df-hom 16445  df-cco 16446  df-rest 16552  df-topn 16553  df-0g 16571  df-gsum 16572  df-topgen 16573  df-pt 16574  df-prds 16577  df-xrs 16631  df-qtop 16636  df-imas 16637  df-xps 16639  df-mre 16715  df-mrc 16716  df-acs 16718  df-mgm 17710  df-sgrp 17752  df-mnd 17763  df-submnd 17804  df-mulg 18012  df-cntz 18218  df-cmn 18668  df-psmet 20239  df-xmet 20240  df-met 20241  df-bl 20242  df-mopn 20243  df-fbas 20244  df-fg 20245  df-cnfld 20248  df-top 21206  df-topon 21223  df-topsp 21245  df-bases 21258  df-cld 21331  df-ntr 21332  df-cls 21333  df-nei 21410  df-lp 21448  df-perf 21449  df-cn 21539  df-cnp 21540  df-haus 21627  df-cmp 21699  df-tx 21874  df-hmeo 22067  df-fil 22158  df-fm 22250  df-flim 22251  df-flf 22252  df-xms 22633  df-ms 22634  df-tms 22635  df-cncf 23189  df-limc 24167  df-dv 24168  df-log 24841
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator