eff1o

Description: The exponential function maps the set S , of complex numbers with imaginary part in the closed-above, open-below interval from -upi to pi one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008) (Revised by Mario Carneiro, 13-May-2014)

		Ref	Expression
	Hypothesis	eff1o.1	$⊢ S = ℑ^{-1} [(- π, π]]$
	Assertion	eff1o	$⊢ ({\exp ↾}_{S}) : S \underset{1-1 onto}{⟶} ℂ ∖ \{0\}$

Proof

Step	Hyp	Ref	Expression
1		eff1o.1	$⊢ S = ℑ^{-1} [(- π, π]]$
2		pire	$⊢ π \in ℝ$
3	2	renegcli	$⊢ - π \in ℝ$
4		eqid	$⊢ (w \in (- π, π] ⟼ e^{i w}) = (w \in (- π, π] ⟼ e^{i w})$
5		rexr	$⊢ - π \in ℝ \to - π \in ℝ^{*}$
6		iocssre	$⊢ (- π \in ℝ^{*} \land π \in ℝ) \to (- π, π] \subseteq ℝ$
7	5 2 6	sylancl	$⊢ - π \in ℝ \to (- π, π] \subseteq ℝ$
8		picn	$⊢ π \in ℂ$
9	8	2timesi	$⊢ 2 π = π + π$
10	9	oveq2i	$⊢ - π + 2 π = (- π) + π + π$
11		negpicn	$⊢ - π \in ℂ$
12	8 8	addcli	$⊢ π + π \in ℂ$
13	11 12	addcomi	$⊢ (- π) + π + π = π + π + (- π)$
14	12 8	negsubi	$⊢ π + π + (- π) = π + π - π$
15	8 8	pncan3oi	$⊢ π + π - π = π$
16	14 15	eqtri	$⊢ π + π + (- π) = π$
17	10 13 16	3eqtrri	$⊢ π = - π + 2 π$
18	17	oveq2i	$⊢ (- π, π] = (- π, - π + 2 π]$
19	18	efif1olem1	$⊢ (- π \in ℝ \land (x \in (- π, π] \land y \in (- π, π])) \to \|x - y\| < 2 π$
20	18	efif1olem2	$⊢ (- π \in ℝ \land z \in ℝ) \to \exists y \in (- π, π] \frac{z - y}{2 π} \in ℤ$
21	4 1 7 19 20	eff1olem	$⊢ - π \in ℝ \to ({\exp ↾}_{S}) : S \underset{1-1 onto}{⟶} ℂ ∖ \{0\}$
22	3 21	ax-mp	$⊢ ({\exp ↾}_{S}) : S \underset{1-1 onto}{⟶} ℂ ∖ \{0\}$

Metamath Proof Explorer

Theorem eff1o

Proof