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

Theorem efopn 24626
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 22807 . . . . . . 7 𝐽 ∈ (TopOn‘ℂ)
3 toponss 20953 . . . . . . 7 ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆𝐽) → 𝑆 ⊆ ℂ)
42, 3mpan 664 . . . . . 6 (𝑆𝐽𝑆 ⊆ ℂ)
54sselda 3753 . . . . 5 ((𝑆𝐽𝑥𝑆) → 𝑥 ∈ ℂ)
6 cnxmet 22797 . . . . . 6 (abs ∘ − ) ∈ (∞Met‘ℂ)
7 pirp 24435 . . . . . . 7 π ∈ ℝ+
81cnfldtopn 22806 . . . . . . . 8 𝐽 = (MetOpen‘(abs ∘ − ))
98mopni3 22520 . . . . . . 7 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆𝐽𝑥𝑆) ∧ π ∈ ℝ+) → ∃𝑟 ∈ ℝ+ (𝑟 < π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆))
107, 9mpan2 665 . . . . . 6 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆𝐽𝑥𝑆) → ∃𝑟 ∈ ℝ+ (𝑟 < π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆))
116, 10mp3an1 1559 . . . . 5 ((𝑆𝐽𝑥𝑆) → ∃𝑟 ∈ ℝ+ (𝑟 < π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆))
12 imass2 5643 . . . . . . . 8 ((𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆 → (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆))
13 imassrn 5619 . . . . . . . . . . . . . 14 (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ ran exp
14 eff 15019 . . . . . . . . . . . . . . 15 exp:ℂ⟶ℂ
15 frn 6194 . . . . . . . . . . . . . . 15 (exp:ℂ⟶ℂ → ran exp ⊆ ℂ)
1614, 15ax-mp 5 . . . . . . . . . . . . . 14 ran exp ⊆ ℂ
1713, 16sstri 3762 . . . . . . . . . . . . 13 (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ ℂ
18 sseqin2 3969 . . . . . . . . . . . . 13 ((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ ℂ ↔ (ℂ ∩ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) = (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)))
1917, 18mpbi 220 . . . . . . . . . . . 12 (ℂ ∩ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) = (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))
20 rpxr 12044 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
21 blssm 22444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
226, 21mp3an1 1559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
2320, 22sylan2 574 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
2423ad2antrr 699 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
2524sselda 3753 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑦 ∈ ℂ)
26 simp-4l 762 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑥 ∈ ℂ)
2725, 26subcld 10595 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦𝑥) ∈ ℂ)
2827subid1d 10584 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦𝑥) − 0) = (𝑦𝑥))
2928fveq2d 6337 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (abs‘((𝑦𝑥) − 0)) = (abs‘(𝑦𝑥)))
30 0cn 10235 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℂ
31 eqid 2771 . . . . . . . . . . . . . . . . . . . . . . 23 (abs ∘ − ) = (abs ∘ − )
3231cnmetdval 22795 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑦𝑥)(abs ∘ − )0) = (abs‘((𝑦𝑥) − 0)))
3327, 30, 32sylancl 568 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦𝑥)(abs ∘ − )0) = (abs‘((𝑦𝑥) − 0)))
3431cnmetdval 22795 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑦(abs ∘ − )𝑥) = (abs‘(𝑦𝑥)))
3525, 26, 34syl2anc 567 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦(abs ∘ − )𝑥) = (abs‘(𝑦𝑥)))
3629, 33, 353eqtr4d 2815 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦𝑥)(abs ∘ − )0) = (𝑦(abs ∘ − )𝑥))
37 simpr 471 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
386a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
39 simpllr 754 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → 𝑟 ∈ ℝ+)
4039adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑟 ∈ ℝ+)
4140rpxrd 12077 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 𝑟 ∈ ℝ*)
42 elbl3 22418 . . . . . . . . . . . . . . . . . . . . . 22 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ (𝑦(abs ∘ − )𝑥) < 𝑟))
4338, 41, 26, 25, 42syl22anc 1477 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ (𝑦(abs ∘ − )𝑥) < 𝑟))
4437, 43mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦(abs ∘ − )𝑥) < 𝑟)
4536, 44eqbrtrd 4809 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦𝑥)(abs ∘ − )0) < 𝑟)
46 0cnd 10236 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → 0 ∈ ℂ)
47 elbl3 22418 . . . . . . . . . . . . . . . . . . . 20 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ (𝑦𝑥) ∈ ℂ)) → ((𝑦𝑥) ∈ (0(ball‘(abs ∘ − ))𝑟) ↔ ((𝑦𝑥)(abs ∘ − )0) < 𝑟))
4838, 41, 46, 27, 47syl22anc 1477 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((𝑦𝑥) ∈ (0(ball‘(abs ∘ − ))𝑟) ↔ ((𝑦𝑥)(abs ∘ − )0) < 𝑟))
4945, 48mpbird 247 . . . . . . . . . . . . . . . . . 18 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦𝑥) ∈ (0(ball‘(abs ∘ − ))𝑟))
50 efsub 15037 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (exp‘(𝑦𝑥)) = ((exp‘𝑦) / (exp‘𝑥)))
5125, 26, 50syl2anc 567 . . . . . . . . . . . . . . . . . 18 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → (exp‘(𝑦𝑥)) = ((exp‘𝑦) / (exp‘𝑥)))
52 fveq2 6333 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝑦𝑥) → (exp‘𝑤) = (exp‘(𝑦𝑥)))
5352eqeq1d 2773 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝑦𝑥) → ((exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)) ↔ (exp‘(𝑦𝑥)) = ((exp‘𝑦) / (exp‘𝑥))))
5453rspcev 3461 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥) ∈ (0(ball‘(abs ∘ − ))𝑟) ∧ (exp‘(𝑦𝑥)) = ((exp‘𝑦) / (exp‘𝑥))) → ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)))
5549, 51, 54syl2anc 567 . . . . . . . . . . . . . . . . 17 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)))
56 oveq1 6801 . . . . . . . . . . . . . . . . . . 19 ((exp‘𝑦) = 𝑧 → ((exp‘𝑦) / (exp‘𝑥)) = (𝑧 / (exp‘𝑥)))
5756eqeq2d 2781 . . . . . . . . . . . . . . . . . 18 ((exp‘𝑦) = 𝑧 → ((exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)) ↔ (exp‘𝑤) = (𝑧 / (exp‘𝑥))))
5857rexbidv 3200 . . . . . . . . . . . . . . . . 17 ((exp‘𝑦) = 𝑧 → (∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = ((exp‘𝑦) / (exp‘𝑥)) ↔ ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
5955, 58syl5ibcom 235 . . . . . . . . . . . . . . . 16 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((exp‘𝑦) = 𝑧 → ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
6059rexlimdva 3179 . . . . . . . . . . . . . . 15 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧 → ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
61 eqcom 2778 . . . . . . . . . . . . . . . . . 18 ((exp‘𝑤) = (𝑧 / (exp‘𝑥)) ↔ (𝑧 / (exp‘𝑥)) = (exp‘𝑤))
62 simplr 746 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑧 ∈ ℂ)
63 simp-4l 762 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑥 ∈ ℂ)
64 efcl 15020 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ → (exp‘𝑥) ∈ ℂ)
6563, 64syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (exp‘𝑥) ∈ ℂ)
6639rpxrd 12077 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → 𝑟 ∈ ℝ*)
67 blssm 22444 . . . . . . . . . . . . . . . . . . . . . . 23 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (0(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
686, 30, 67mp3an12 1562 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 ∈ ℝ* → (0(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
6966, 68syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (0(ball‘(abs ∘ − ))𝑟) ⊆ ℂ)
7069sselda 3753 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑤 ∈ ℂ)
71 efcl 15020 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℂ → (exp‘𝑤) ∈ ℂ)
7270, 71syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (exp‘𝑤) ∈ ℂ)
73 efne0 15034 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ → (exp‘𝑥) ≠ 0)
7463, 73syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (exp‘𝑥) ≠ 0)
7562, 65, 72, 74divmuld 11026 . . . . . . . . . . . . . . . . . 18 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑧 / (exp‘𝑥)) = (exp‘𝑤) ↔ ((exp‘𝑥) · (exp‘𝑤)) = 𝑧))
7661, 75syl5bb 272 . . . . . . . . . . . . . . . . 17 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((exp‘𝑤) = (𝑧 / (exp‘𝑥)) ↔ ((exp‘𝑥) · (exp‘𝑤)) = 𝑧))
7763, 70pncan2d 10597 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤) − 𝑥) = 𝑤)
7870subid1d 10584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑤 − 0) = 𝑤)
7977, 78eqtr4d 2808 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤) − 𝑥) = (𝑤 − 0))
8079fveq2d 6337 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (abs‘((𝑥 + 𝑤) − 𝑥)) = (abs‘(𝑤 − 0)))
8163, 70addcld 10262 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑥 + 𝑤) ∈ ℂ)
8231cnmetdval 22795 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 + 𝑤) ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) = (abs‘((𝑥 + 𝑤) − 𝑥)))
8381, 63, 82syl2anc 567 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) = (abs‘((𝑥 + 𝑤) − 𝑥)))
8431cnmetdval 22795 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑤(abs ∘ − )0) = (abs‘(𝑤 − 0)))
8570, 30, 84sylancl 568 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑤(abs ∘ − )0) = (abs‘(𝑤 − 0)))
8680, 83, 853eqtr4d 2815 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) = (𝑤(abs ∘ − )0))
87 simpr 471 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟))
886a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
8939adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑟 ∈ ℝ+)
9089rpxrd 12077 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 𝑟 ∈ ℝ*)
91 0cnd 10236 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → 0 ∈ ℂ)
92 elbl3 22418 . . . . . . . . . . . . . . . . . . . . . . 23 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟) ↔ (𝑤(abs ∘ − )0) < 𝑟))
9388, 90, 91, 70, 92syl22anc 1477 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟) ↔ (𝑤(abs ∘ − )0) < 𝑟))
9487, 93mpbid 222 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑤(abs ∘ − )0) < 𝑟)
9586, 94eqbrtrd 4809 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤)(abs ∘ − )𝑥) < 𝑟)
96 elbl3 22418 . . . . . . . . . . . . . . . . . . . . 21 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑥 ∈ ℂ ∧ (𝑥 + 𝑤) ∈ ℂ)) → ((𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥 + 𝑤)(abs ∘ − )𝑥) < 𝑟))
9788, 90, 63, 81, 96syl22anc 1477 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥 + 𝑤)(abs ∘ − )𝑥) < 𝑟))
9895, 97mpbird 247 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
99 efadd 15031 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤)))
10063, 70, 99syl2anc 567 . . . . . . . . . . . . . . . . . . 19 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤)))
101 fveq2 6333 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑥 + 𝑤) → (exp‘𝑦) = (exp‘(𝑥 + 𝑤)))
102101eqeq1d 2773 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑥 + 𝑤) → ((exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)) ↔ (exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤))))
103102rspcev 3461 . . . . . . . . . . . . . . . . . . 19 (((𝑥 + 𝑤) ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ∧ (exp‘(𝑥 + 𝑤)) = ((exp‘𝑥) · (exp‘𝑤))) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)))
10498, 100, 103syl2anc 567 . . . . . . . . . . . . . . . . . 18 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)))
105 eqeq2 2782 . . . . . . . . . . . . . . . . . . 19 (((exp‘𝑥) · (exp‘𝑤)) = 𝑧 → ((exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)) ↔ (exp‘𝑦) = 𝑧))
106105rexbidv 3200 . . . . . . . . . . . . . . . . . 18 (((exp‘𝑥) · (exp‘𝑤)) = 𝑧 → (∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = ((exp‘𝑥) · (exp‘𝑤)) ↔ ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
107104, 106syl5ibcom 235 . . . . . . . . . . . . . . . . 17 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → (((exp‘𝑥) · (exp‘𝑤)) = 𝑧 → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
10876, 107sylbid 230 . . . . . . . . . . . . . . . 16 (((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) ∧ 𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)) → ((exp‘𝑤) = (𝑧 / (exp‘𝑥)) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
109108rexlimdva 3179 . . . . . . . . . . . . . . 15 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥)) → ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
11060, 109impbid 202 . . . . . . . . . . . . . 14 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧 ↔ ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
111 ffn 6186 . . . . . . . . . . . . . . . 16 (exp:ℂ⟶ℂ → exp Fn ℂ)
11214, 111ax-mp 5 . . . . . . . . . . . . . . 15 exp Fn ℂ
113 fvelimab 6396 . . . . . . . . . . . . . . 15 ((exp Fn ℂ ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ ℂ) → (𝑧 ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
114112, 24, 113sylancr 569 . . . . . . . . . . . . . 14 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (𝑧 ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)(exp‘𝑦) = 𝑧))
115 fvelimab 6396 . . . . . . . . . . . . . . 15 ((exp Fn ℂ ∧ (0(ball‘(abs ∘ − ))𝑟) ⊆ ℂ) → ((𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
116112, 69, 115sylancr 569 . . . . . . . . . . . . . 14 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → ((𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (0(ball‘(abs ∘ − ))𝑟)(exp‘𝑤) = (𝑧 / (exp‘𝑥))))
117110, 114, 1163bitr4d 300 . . . . . . . . . . . . 13 ((((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) ∧ 𝑧 ∈ ℂ) → (𝑧 ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ↔ (𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟))))
118117rabbi2dva 3971 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (ℂ ∩ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) = {𝑧 ∈ ℂ ∣ (𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟))})
11919, 118syl5eqr 2819 . . . . . . . . . . 11 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) = {𝑧 ∈ ℂ ∣ (𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟))})
120 eqid 2771 . . . . . . . . . . . 12 (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) = (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥)))
121120mptpreima 5773 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs ∘ − ))𝑟))) = {𝑧 ∈ ℂ ∣ (𝑧 / (exp‘𝑥)) ∈ (exp “ (0(ball‘(abs ∘ − ))𝑟))}
122119, 121syl6eqr 2823 . . . . . . . . . 10 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) = ((𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs ∘ − ))𝑟))))
12364ad2antrr 699 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp‘𝑥) ∈ ℂ)
12473ad2antrr 699 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp‘𝑥) ≠ 0)
125120divccncf 22930 . . . . . . . . . . . . 13 (((exp‘𝑥) ∈ ℂ ∧ (exp‘𝑥) ≠ 0) → (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) ∈ (ℂ–cn→ℂ))
126123, 124, 125syl2anc 567 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) ∈ (ℂ–cn→ℂ))
1271cncfcn1 22934 . . . . . . . . . . . 12 (ℂ–cn→ℂ) = (𝐽 Cn 𝐽)
128126, 127syl6eleq 2860 . . . . . . . . . . 11 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) ∈ (𝐽 Cn 𝐽))
1291efopnlem2 24625 . . . . . . . . . . . 12 ((𝑟 ∈ ℝ+𝑟 < π) → (exp “ (0(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽)
130129adantll 687 . . . . . . . . . . 11 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp “ (0(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽)
131 cnima 21291 . . . . . . . . . . 11 (((𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) ∈ (𝐽 Cn 𝐽) ∧ (exp “ (0(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽) → ((𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs ∘ − ))𝑟))) ∈ 𝐽)
132128, 130, 131syl2anc 567 . . . . . . . . . 10 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → ((𝑧 ∈ ℂ ↦ (𝑧 / (exp‘𝑥))) “ (exp “ (0(ball‘(abs ∘ − ))𝑟))) ∈ 𝐽)
133122, 132eqeltrd 2850 . . . . . . . . 9 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽)
134 blcntr 22439 . . . . . . . . . . . 12 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
1356, 134mp3an1 1559 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘(abs ∘ − ))𝑟))
136 ffun 6189 . . . . . . . . . . . . 13 (exp:ℂ⟶ℂ → Fun exp)
13714, 136ax-mp 5 . . . . . . . . . . . 12 Fun exp
13814fdmi 6193 . . . . . . . . . . . . 13 dom exp = ℂ
13923, 138syl6sseqr 3802 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ dom exp)
140 funfvima2 6637 . . . . . . . . . . . 12 ((Fun exp ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ dom exp) → (𝑥 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) → (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))))
141137, 139, 140sylancr 569 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → (𝑥 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) → (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))))
142135, 141mpd 15 . . . . . . . . . 10 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)))
143142adantr 466 . . . . . . . . 9 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)))
144 eleq2 2839 . . . . . . . . . . . 12 (𝑦 = (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) → ((exp‘𝑥) ∈ 𝑦 ↔ (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))))
145 sseq1 3776 . . . . . . . . . . . 12 (𝑦 = (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) → (𝑦 ⊆ (exp “ 𝑆) ↔ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆)))
146144, 145anbi12d 610 . . . . . . . . . . 11 (𝑦 = (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) → (((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆)) ↔ ((exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∧ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆))))
147146rspcev 3461 . . . . . . . . . 10 (((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽 ∧ ((exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∧ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆))) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆)))
148147expr 444 . . . . . . . . 9 (((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ∈ 𝐽 ∧ (exp‘𝑥) ∈ (exp “ (𝑥(ball‘(abs ∘ − ))𝑟))) → ((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
149133, 143, 148syl2anc 567 . . . . . . . 8 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → ((exp “ (𝑥(ball‘(abs ∘ − ))𝑟)) ⊆ (exp “ 𝑆) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
15012, 149syl5 34 . . . . . . 7 (((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) ∧ 𝑟 < π) → ((𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆 → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
151150expimpd 441 . . . . . 6 ((𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → ((𝑟 < π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
152151rexlimdva 3179 . . . . 5 (𝑥 ∈ ℂ → (∃𝑟 ∈ ℝ+ (𝑟 < π ∧ (𝑥(ball‘(abs ∘ − ))𝑟) ⊆ 𝑆) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
1535, 11, 152sylc 65 . . . 4 ((𝑆𝐽𝑥𝑆) → ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆)))
154153ralrimiva 3115 . . 3 (𝑆𝐽 → ∀𝑥𝑆𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆)))
155 eleq1 2838 . . . . . . 7 (𝑧 = (exp‘𝑥) → (𝑧𝑦 ↔ (exp‘𝑥) ∈ 𝑦))
156155anbi1d 609 . . . . . 6 (𝑧 = (exp‘𝑥) → ((𝑧𝑦𝑦 ⊆ (exp “ 𝑆)) ↔ ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
157156rexbidv 3200 . . . . 5 (𝑧 = (exp‘𝑥) → (∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆)) ↔ ∃𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
158157ralima 6642 . . . 4 ((exp Fn ℂ ∧ 𝑆 ⊆ ℂ) → (∀𝑧 ∈ (exp “ 𝑆)∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆)) ↔ ∀𝑥𝑆𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
159112, 4, 158sylancr 569 . . 3 (𝑆𝐽 → (∀𝑧 ∈ (exp “ 𝑆)∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆)) ↔ ∀𝑥𝑆𝑦𝐽 ((exp‘𝑥) ∈ 𝑦𝑦 ⊆ (exp “ 𝑆))))
160154, 159mpbird 247 . 2 (𝑆𝐽 → ∀𝑧 ∈ (exp “ 𝑆)∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆)))
1611cnfldtop 22808 . . 3 𝐽 ∈ Top
162 eltop2 21001 . . 3 (𝐽 ∈ Top → ((exp “ 𝑆) ∈ 𝐽 ↔ ∀𝑧 ∈ (exp “ 𝑆)∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆))))
163161, 162ax-mp 5 . 2 ((exp “ 𝑆) ∈ 𝐽 ↔ ∀𝑧 ∈ (exp “ 𝑆)∃𝑦𝐽 (𝑧𝑦𝑦 ⊆ (exp “ 𝑆)))
164160, 163sylibr 224 1 (𝑆𝐽 → (exp “ 𝑆) ∈ 𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  cin 3723  wss 3724   class class class wbr 4787  cmpt 4864  ccnv 5249  dom cdm 5250  ran crn 5251  cima 5253  ccom 5254  Fun wfun 6026   Fn wfn 6027  wf 6028  cfv 6032  (class class class)co 6794  cc 10137  0cc0 10139   + caddc 10142   · cmul 10144  *cxr 10276   < clt 10277  cmin 10469   / cdiv 10887  +crp 12036  abscabs 14183  expce 14999  πcpi 15004  TopOpenctopn 16291  ∞Metcxmt 19947  ballcbl 19949  fldccnfld 19962  Topctop 20919  TopOnctopon 20936   Cn ccn 21250  cnccncf 22900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-inf2 8703  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216  ax-pre-sup 10217  ax-addf 10218  ax-mulf 10219
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-isom 6041  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-of 7045  df-om 7214  df-1st 7316  df-2nd 7317  df-supp 7448  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-2o 7715  df-oadd 7718  df-er 7897  df-map 8012  df-pm 8013  df-ixp 8064  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-fsupp 8433  df-fi 8474  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8966  df-cda 9193  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-div 10888  df-nn 11224  df-2 11282  df-3 11283  df-4 11284  df-5 11285  df-6 11286  df-7 11287  df-8 11288  df-9 11289  df-n0 11496  df-z 11581  df-dec 11697  df-uz 11890  df-q 11993  df-rp 12037  df-xneg 12152  df-xadd 12153  df-xmul 12154  df-ioo 12385  df-ioc 12386  df-ico 12387  df-icc 12388  df-fz 12535  df-fzo 12675  df-fl 12802  df-mod 12878  df-seq 13010  df-exp 13069  df-fac 13266  df-bc 13295  df-hash 13323  df-shft 14016  df-cj 14048  df-re 14049  df-im 14050  df-sqrt 14184  df-abs 14185  df-limsup 14411  df-clim 14428  df-rlim 14429  df-sum 14626  df-ef 15005  df-sin 15007  df-cos 15008  df-tan 15009  df-pi 15010  df-struct 16067  df-ndx 16068  df-slot 16069  df-base 16071  df-sets 16072  df-ress 16073  df-plusg 16163  df-mulr 16164  df-starv 16165  df-sca 16166  df-vsca 16167  df-ip 16168  df-tset 16169  df-ple 16170  df-ds 16173  df-unif 16174  df-hom 16175  df-cco 16176  df-rest 16292  df-topn 16293  df-0g 16311  df-gsum 16312  df-topgen 16313  df-pt 16314  df-prds 16317  df-xrs 16371  df-qtop 16376  df-imas 16377  df-xps 16379  df-mre 16455  df-mrc 16456  df-acs 16458  df-mgm 17451  df-sgrp 17493  df-mnd 17504  df-submnd 17545  df-mulg 17750  df-cntz 17958  df-cmn 18403  df-psmet 19954  df-xmet 19955  df-met 19956  df-bl 19957  df-mopn 19958  df-fbas 19959  df-fg 19960  df-cnfld 19963  df-top 20920  df-topon 20937  df-topsp 20959  df-bases 20972  df-cld 21045  df-ntr 21046  df-cls 21047  df-nei 21124  df-lp 21162  df-perf 21163  df-cn 21253  df-cnp 21254  df-haus 21341  df-cmp 21412  df-tx 21587  df-hmeo 21780  df-fil 21871  df-fm 21963  df-flim 21964  df-flf 21965  df-xms 22346  df-ms 22347  df-tms 22348  df-cncf 22902  df-limc 23851  df-dv 23852  df-log 24525
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator