efopn

Description: The exponential map is an open map. (Contributed by Mario Carneiro, 23-Apr-2015)

		Ref	Expression
	Hypothesis	efopn.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
	Assertion	efopn	⊢ ( 𝑆 ∈ 𝐽 → ( exp “ 𝑆 ) ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		efopn.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
2	1	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
3		toponss	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ⊆ ℂ )
4	2 3	mpan	⊢ ( 𝑆 ∈ 𝐽 → 𝑆 ⊆ ℂ )
5	4	sselda	⊢ ( ( 𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ℂ )
6		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
7		pirp	⊢ π ∈ ℝ⁺
8	1	cnfldtopn	⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
9	8	mopni3	⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆 ) ∧ π ∈ ℝ⁺ ) → ∃ 𝑟 ∈ ℝ⁺ ( 𝑟 < π ∧ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑆 ) )
10	7 9	mpan2	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑟 ∈ ℝ⁺ ( 𝑟 < π ∧ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑆 ) )
11	6 10	mp3an1	⊢ ( ( 𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑟 ∈ ℝ⁺ ( 𝑟 < π ∧ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑆 ) )
12		imass2	⊢ ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑆 → ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ⊆ ( exp “ 𝑆 ) )
13		imassrn	⊢ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ⊆ ran exp
14		eff	⊢ exp : ℂ ⟶ ℂ
15		frn	⊢ ( exp : ℂ ⟶ ℂ → ran exp ⊆ ℂ )
16	14 15	ax-mp	⊢ ran exp ⊆ ℂ
17	13 16	sstri	⊢ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ⊆ ℂ
18		sseqin2	⊢ ( ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ⊆ ℂ ↔ ( ℂ ∩ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) = ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
19	17 18	mpbi	⊢ ( ℂ ∩ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) = ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
20		rpxr	⊢ ( 𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^* )
21		blssm	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ^* ) → ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ ℂ )
22	6 21	mp3an1	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ^* ) → ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ ℂ )
23	20 22	sylan2	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) → ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ ℂ )
24	23	ad2antrr	⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ ℂ )
25	24	sselda	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 𝑦 ∈ ℂ )
26		simp-4l	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 𝑥 ∈ ℂ )
27	25 26	subcld	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑦 − 𝑥 ) ∈ ℂ )
28	27	subid1d	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑦 − 𝑥 ) − 0 ) = ( 𝑦 − 𝑥 ) )
29	28	fveq2d	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( abs ‘ ( ( 𝑦 − 𝑥 ) − 0 ) ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
30		0cn	⊢ 0 ∈ ℂ
31		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
32	31	cnmetdval	⊢ ( ( ( 𝑦 − 𝑥 ) ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( 𝑦 − 𝑥 ) ( abs ∘ − ) 0 ) = ( abs ‘ ( ( 𝑦 − 𝑥 ) − 0 ) ) )
33	27 30 32	sylancl	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑦 − 𝑥 ) ( abs ∘ − ) 0 ) = ( abs ‘ ( ( 𝑦 − 𝑥 ) − 0 ) ) )
34	31	cnmetdval	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑦 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
35	25 26 34	syl2anc	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑦 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
36	29 33 35	3eqtr4d	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑦 − 𝑥 ) ( abs ∘ − ) 0 ) = ( 𝑦 ( abs ∘ − ) 𝑥 ) )
37		simpr	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
38	6	a1i	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
39		simpllr	⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) → 𝑟 ∈ ℝ⁺ )
40	39	adantr	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 𝑟 ∈ ℝ⁺ )
41	40	rpxrd	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 𝑟 ∈ ℝ^* )
42		elbl3	⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑟 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( 𝑦 ( abs ∘ − ) 𝑥 ) < 𝑟 ) )
43	38 41 26 25 42	syl22anc	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( 𝑦 ( abs ∘ − ) 𝑥 ) < 𝑟 ) )
44	37 43	mpbid	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑦 ( abs ∘ − ) 𝑥 ) < 𝑟 )
45	36 44	eqbrtrd	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑦 − 𝑥 ) ( abs ∘ − ) 0 ) < 𝑟 )
46		0cnd	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 0 ∈ ℂ )
47		elbl3	⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑟 ∈ ℝ^* ) ∧ ( 0 ∈ ℂ ∧ ( 𝑦 − 𝑥 ) ∈ ℂ ) ) → ( ( 𝑦 − 𝑥 ) ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( ( 𝑦 − 𝑥 ) ( abs ∘ − ) 0 ) < 𝑟 ) )
48	38 41 46 27 47	syl22anc	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑦 − 𝑥 ) ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( ( 𝑦 − 𝑥 ) ( abs ∘ − ) 0 ) < 𝑟 ) )
49	45 48	mpbird	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑦 − 𝑥 ) ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
50		efsub	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( exp ‘ ( 𝑦 − 𝑥 ) ) = ( ( exp ‘ 𝑦 ) / ( exp ‘ 𝑥 ) ) )
51	25 26 50	syl2anc	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( exp ‘ ( 𝑦 − 𝑥 ) ) = ( ( exp ‘ 𝑦 ) / ( exp ‘ 𝑥 ) ) )
52		fveqeq2	⊢ ( 𝑤 = ( 𝑦 − 𝑥 ) → ( ( exp ‘ 𝑤 ) = ( ( exp ‘ 𝑦 ) / ( exp ‘ 𝑥 ) ) ↔ ( exp ‘ ( 𝑦 − 𝑥 ) ) = ( ( exp ‘ 𝑦 ) / ( exp ‘ 𝑥 ) ) ) )
53	52	rspcev	⊢ ( ( ( 𝑦 − 𝑥 ) ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ ( exp ‘ ( 𝑦 − 𝑥 ) ) = ( ( exp ‘ 𝑦 ) / ( exp ‘ 𝑥 ) ) ) → ∃ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑤 ) = ( ( exp ‘ 𝑦 ) / ( exp ‘ 𝑥 ) ) )
54	49 51 53	syl2anc	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∃ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑤 ) = ( ( exp ‘ 𝑦 ) / ( exp ‘ 𝑥 ) ) )
55		oveq1	⊢ ( ( exp ‘ 𝑦 ) = 𝑧 → ( ( exp ‘ 𝑦 ) / ( exp ‘ 𝑥 ) ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) )
56	55	eqeq2d	⊢ ( ( exp ‘ 𝑦 ) = 𝑧 → ( ( exp ‘ 𝑤 ) = ( ( exp ‘ 𝑦 ) / ( exp ‘ 𝑥 ) ) ↔ ( exp ‘ 𝑤 ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) ) )
57	56	rexbidv	⊢ ( ( exp ‘ 𝑦 ) = 𝑧 → ( ∃ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑤 ) = ( ( exp ‘ 𝑦 ) / ( exp ‘ 𝑥 ) ) ↔ ∃ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑤 ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) ) )
58	54 57	syl5ibcom	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( exp ‘ 𝑦 ) = 𝑧 → ∃ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑤 ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) ) )
59	58	rexlimdva	⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) → ( ∃ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑦 ) = 𝑧 → ∃ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑤 ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) ) )
60		eqcom	⊢ ( ( exp ‘ 𝑤 ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) ↔ ( 𝑧 / ( exp ‘ 𝑥 ) ) = ( exp ‘ 𝑤 ) )
61		simplr	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 𝑧 ∈ ℂ )
62		simp-4l	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 𝑥 ∈ ℂ )
63		efcl	⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ℂ )
64	62 63	syl	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( exp ‘ 𝑥 ) ∈ ℂ )
65	39	rpxrd	⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) → 𝑟 ∈ ℝ^* )
66		blssm	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑟 ∈ ℝ^* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ ℂ )
67	6 30 65 66	mp3an12i	⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ ℂ )
68	67	sselda	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 𝑤 ∈ ℂ )
69		efcl	⊢ ( 𝑤 ∈ ℂ → ( exp ‘ 𝑤 ) ∈ ℂ )
70	68 69	syl	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( exp ‘ 𝑤 ) ∈ ℂ )
71		efne0	⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ≠ 0 )
72	62 71	syl	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( exp ‘ 𝑥 ) ≠ 0 )
73	61 64 70 72	divmuld	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑧 / ( exp ‘ 𝑥 ) ) = ( exp ‘ 𝑤 ) ↔ ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) = 𝑧 ) )
74	60 73	bitrid	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( exp ‘ 𝑤 ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) ↔ ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) = 𝑧 ) )
75	62 68	pncan2d	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑥 + 𝑤 ) − 𝑥 ) = 𝑤 )
76	68	subid1d	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑤 − 0 ) = 𝑤 )
77	75 76	eqtr4d	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑥 + 𝑤 ) − 𝑥 ) = ( 𝑤 − 0 ) )
78	77	fveq2d	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( abs ‘ ( ( 𝑥 + 𝑤 ) − 𝑥 ) ) = ( abs ‘ ( 𝑤 − 0 ) ) )
79	62 68	addcld	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑥 + 𝑤 ) ∈ ℂ )
80	31	cnmetdval	⊢ ( ( ( 𝑥 + 𝑤 ) ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 + 𝑤 ) ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( ( 𝑥 + 𝑤 ) − 𝑥 ) ) )
81	79 62 80	syl2anc	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑥 + 𝑤 ) ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( ( 𝑥 + 𝑤 ) − 𝑥 ) ) )
82	31	cnmetdval	⊢ ( ( 𝑤 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑤 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑤 − 0 ) ) )
83	68 30 82	sylancl	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑤 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑤 − 0 ) ) )
84	78 81 83	3eqtr4d	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑥 + 𝑤 ) ( abs ∘ − ) 𝑥 ) = ( 𝑤 ( abs ∘ − ) 0 ) )
85		simpr	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
86	6	a1i	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
87	39	adantr	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 𝑟 ∈ ℝ⁺ )
88	87	rpxrd	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 𝑟 ∈ ℝ^* )
89		0cnd	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → 0 ∈ ℂ )
90		elbl3	⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑟 ∈ ℝ^* ) ∧ ( 0 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) → ( 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( 𝑤 ( abs ∘ − ) 0 ) < 𝑟 ) )
91	86 88 89 68 90	syl22anc	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( 𝑤 ( abs ∘ − ) 0 ) < 𝑟 ) )
92	85 91	mpbid	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑤 ( abs ∘ − ) 0 ) < 𝑟 )
93	84 92	eqbrtrd	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑥 + 𝑤 ) ( abs ∘ − ) 𝑥 ) < 𝑟 )
94		elbl3	⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑟 ∈ ℝ^* ) ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝑤 ) ∈ ℂ ) ) → ( ( 𝑥 + 𝑤 ) ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( ( 𝑥 + 𝑤 ) ( abs ∘ − ) 𝑥 ) < 𝑟 ) )
95	86 88 62 79 94	syl22anc	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑥 + 𝑤 ) ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( ( 𝑥 + 𝑤 ) ( abs ∘ − ) 𝑥 ) < 𝑟 ) )
96	93 95	mpbird	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑥 + 𝑤 ) ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
97		efadd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( exp ‘ ( 𝑥 + 𝑤 ) ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) )
98	62 68 97	syl2anc	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( exp ‘ ( 𝑥 + 𝑤 ) ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) )
99		fveqeq2	⊢ ( 𝑦 = ( 𝑥 + 𝑤 ) → ( ( exp ‘ 𝑦 ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) ↔ ( exp ‘ ( 𝑥 + 𝑤 ) ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) ) )
100	99	rspcev	⊢ ( ( ( 𝑥 + 𝑤 ) ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∧ ( exp ‘ ( 𝑥 + 𝑤 ) ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) ) → ∃ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑦 ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) )
101	96 98 100	syl2anc	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∃ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑦 ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) )
102		eqeq2	⊢ ( ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) = 𝑧 → ( ( exp ‘ 𝑦 ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) ↔ ( exp ‘ 𝑦 ) = 𝑧 ) )
103	102	rexbidv	⊢ ( ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) = 𝑧 → ( ∃ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑦 ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) ↔ ∃ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑦 ) = 𝑧 ) )
104	101 103	syl5ibcom	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑤 ) ) = 𝑧 → ∃ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑦 ) = 𝑧 ) )
105	74 104	sylbid	⊢ ( ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( exp ‘ 𝑤 ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑦 ) = 𝑧 ) )
106	105	rexlimdva	⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) → ( ∃ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑤 ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑦 ) = 𝑧 ) )
107	59 106	impbid	⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) → ( ∃ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑦 ) = 𝑧 ↔ ∃ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑤 ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) ) )
108		ffn	⊢ ( exp : ℂ ⟶ ℂ → exp Fn ℂ )
109	14 108	ax-mp	⊢ exp Fn ℂ
110		fvelimab	⊢ ( ( exp Fn ℂ ∧ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ ℂ ) → ( 𝑧 ∈ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ∃ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑦 ) = 𝑧 ) )
111	109 24 110	sylancr	⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) → ( 𝑧 ∈ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ∃ 𝑦 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑦 ) = 𝑧 ) )
112		fvelimab	⊢ ( ( exp Fn ℂ ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ ℂ ) → ( ( 𝑧 / ( exp ‘ 𝑥 ) ) ∈ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ∃ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑤 ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) ) )
113	109 67 112	sylancr	⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝑧 / ( exp ‘ 𝑥 ) ) ∈ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ∃ 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ( exp ‘ 𝑤 ) = ( 𝑧 / ( exp ‘ 𝑥 ) ) ) )
114	107 111 113	3bitr4d	⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) ∧ 𝑧 ∈ ℂ ) → ( 𝑧 ∈ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ( 𝑧 / ( exp ‘ 𝑥 ) ) ∈ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
115	114	rabbi2dva	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( ℂ ∩ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) = { 𝑧 ∈ ℂ ∣ ( 𝑧 / ( exp ‘ 𝑥 ) ) ∈ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) } )
116	19 115	eqtr3id	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) = { 𝑧 ∈ ℂ ∣ ( 𝑧 / ( exp ‘ 𝑥 ) ) ∈ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) } )
117		eqid	⊢ ( 𝑧 ∈ ℂ ↦ ( 𝑧 / ( exp ‘ 𝑥 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 / ( exp ‘ 𝑥 ) ) )
118	117	mptpreima	⊢ ( ^◡ ( 𝑧 ∈ ℂ ↦ ( 𝑧 / ( exp ‘ 𝑥 ) ) ) “ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) = { 𝑧 ∈ ℂ ∣ ( 𝑧 / ( exp ‘ 𝑥 ) ) ∈ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) }
119	116 118	eqtr4di	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) = ( ^◡ ( 𝑧 ∈ ℂ ↦ ( 𝑧 / ( exp ‘ 𝑥 ) ) ) “ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
120	63	ad2antrr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( exp ‘ 𝑥 ) ∈ ℂ )
121	71	ad2antrr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( exp ‘ 𝑥 ) ≠ 0 )
122	117	divccncf	⊢ ( ( ( exp ‘ 𝑥 ) ∈ ℂ ∧ ( exp ‘ 𝑥 ) ≠ 0 ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 / ( exp ‘ 𝑥 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
123	120 121 122	syl2anc	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 / ( exp ‘ 𝑥 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
124	1	cncfcn1	⊢ ( ℂ –cn→ ℂ ) = ( 𝐽 Cn 𝐽 )
125	123 124	eleqtrdi	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 / ( exp ‘ 𝑥 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
126	1	efopnlem2	⊢ ( ( 𝑟 ∈ ℝ⁺ ∧ 𝑟 < π ) → ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∈ 𝐽 )
127	126	adantll	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∈ 𝐽 )
128		cnima	⊢ ( ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 / ( exp ‘ 𝑥 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) ∧ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∈ 𝐽 ) → ( ^◡ ( 𝑧 ∈ ℂ ↦ ( 𝑧 / ( exp ‘ 𝑥 ) ) ) “ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) ∈ 𝐽 )
129	125 127 128	syl2anc	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( ^◡ ( 𝑧 ∈ ℂ ↦ ( 𝑧 / ( exp ‘ 𝑥 ) ) ) “ ( exp “ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) ∈ 𝐽 )
130	119 129	eqeltrd	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∈ 𝐽 )
131		blcntr	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
132	6 131	mp3an1	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
133		ffun	⊢ ( exp : ℂ ⟶ ℂ → Fun exp )
134	14 133	ax-mp	⊢ Fun exp
135	14	fdmi	⊢ dom exp = ℂ
136	23 135	sseqtrrdi	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) → ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ dom exp )
137		funfvima2	⊢ ( ( Fun exp ∧ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ dom exp ) → ( 𝑥 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ( exp ‘ 𝑥 ) ∈ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
138	134 136 137	sylancr	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) → ( 𝑥 ∈ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ( exp ‘ 𝑥 ) ∈ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
139	132 138	mpd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) → ( exp ‘ 𝑥 ) ∈ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
140	139	adantr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( exp ‘ 𝑥 ) ∈ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
141		eleq2	⊢ ( 𝑦 = ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( exp ‘ 𝑥 ) ∈ 𝑦 ↔ ( exp ‘ 𝑥 ) ∈ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
142		sseq1	⊢ ( 𝑦 = ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑦 ⊆ ( exp “ 𝑆 ) ↔ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ⊆ ( exp “ 𝑆 ) ) )
143	141 142	anbi12d	⊢ ( 𝑦 = ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ↔ ( ( exp ‘ 𝑥 ) ∈ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∧ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ⊆ ( exp “ 𝑆 ) ) ) )
144	143	rspcev	⊢ ( ( ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∈ 𝐽 ∧ ( ( exp ‘ 𝑥 ) ∈ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∧ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ⊆ ( exp “ 𝑆 ) ) ) → ∃ 𝑦 ∈ 𝐽 ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) )
145	144	expr	⊢ ( ( ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∈ 𝐽 ∧ ( exp ‘ 𝑥 ) ∈ ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) → ( ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ⊆ ( exp “ 𝑆 ) → ∃ 𝑦 ∈ 𝐽 ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ) )
146	130 140 145	syl2anc	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( ( exp “ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ⊆ ( exp “ 𝑆 ) → ∃ 𝑦 ∈ 𝐽 ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ) )
147	12 146	syl5	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑟 < π ) → ( ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑆 → ∃ 𝑦 ∈ 𝐽 ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ) )
148	147	expimpd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑟 ∈ ℝ⁺ ) → ( ( 𝑟 < π ∧ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑆 ) → ∃ 𝑦 ∈ 𝐽 ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ) )
149	148	rexlimdva	⊢ ( 𝑥 ∈ ℂ → ( ∃ 𝑟 ∈ ℝ⁺ ( 𝑟 < π ∧ ( 𝑥 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑆 ) → ∃ 𝑦 ∈ 𝐽 ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ) )
150	5 11 149	sylc	⊢ ( ( 𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑦 ∈ 𝐽 ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) )
151	150	ralrimiva	⊢ ( 𝑆 ∈ 𝐽 → ∀ 𝑥 ∈ 𝑆 ∃ 𝑦 ∈ 𝐽 ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) )
152		eleq1	⊢ ( 𝑧 = ( exp ‘ 𝑥 ) → ( 𝑧 ∈ 𝑦 ↔ ( exp ‘ 𝑥 ) ∈ 𝑦 ) )
153	152	anbi1d	⊢ ( 𝑧 = ( exp ‘ 𝑥 ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ↔ ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ) )
154	153	rexbidv	⊢ ( 𝑧 = ( exp ‘ 𝑥 ) → ( ∃ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ↔ ∃ 𝑦 ∈ 𝐽 ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ) )
155	154	ralima	⊢ ( ( exp Fn ℂ ∧ 𝑆 ⊆ ℂ ) → ( ∀ 𝑧 ∈ ( exp “ 𝑆 ) ∃ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ∃ 𝑦 ∈ 𝐽 ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ) )
156	109 4 155	sylancr	⊢ ( 𝑆 ∈ 𝐽 → ( ∀ 𝑧 ∈ ( exp “ 𝑆 ) ∃ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ∃ 𝑦 ∈ 𝐽 ( ( exp ‘ 𝑥 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ) )
157	151 156	mpbird	⊢ ( 𝑆 ∈ 𝐽 → ∀ 𝑧 ∈ ( exp “ 𝑆 ) ∃ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) )
158	1	cnfldtop	⊢ 𝐽 ∈ Top
159		eltop2	⊢ ( 𝐽 ∈ Top → ( ( exp “ 𝑆 ) ∈ 𝐽 ↔ ∀ 𝑧 ∈ ( exp “ 𝑆 ) ∃ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) ) )
160	158 159	ax-mp	⊢ ( ( exp “ 𝑆 ) ∈ 𝐽 ↔ ∀ 𝑧 ∈ ( exp “ 𝑆 ) ∃ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ⊆ ( exp “ 𝑆 ) ) )
161	157 160	sylibr	⊢ ( 𝑆 ∈ 𝐽 → ( exp “ 𝑆 ) ∈ 𝐽 )

Metamath Proof Explorer

Theorem efopn

Proof