efopn

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

		Ref	Expression
	Hypothesis	efopn.j	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	efopn	$⊢ S \in J \to \exp [S] \in J$

Proof

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

Metamath Proof Explorer

Theorem efopn

Proof