Metamath Proof Explorer

Theorem efif1o

Description: The exponential function of an imaginary number maps any open-below, closed-above interval of length 2 _pi one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008) (Revised by Mario Carneiro, 13-May-2014)

		Ref	Expression
	Hypotheses	efif1o.1	$⊢ F = (w \in D ⟼ e^{i w})$
		efif1o.2	$⊢ C = {abs}^{-1} [\{1\}]$
		efif1o.3	$⊢ D = (A, A + 2 π]$
	Assertion	efif1o	$⊢ A \in ℝ \to F : D \underset{1-1 onto}{⟶} C$

Proof

Step	Hyp	Ref	Expression
1		efif1o.1	$⊢ F = (w \in D ⟼ e^{i w})$
2		efif1o.2	$⊢ C = {abs}^{-1} [\{1\}]$
3		efif1o.3	$⊢ D = (A, A + 2 π]$
4		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
5		2re	$⊢ 2 \in ℝ$
6		pire	$⊢ π \in ℝ$
7	5 6	remulcli	$⊢ 2 π \in ℝ$
8		readdcl	$⊢ (A \in ℝ \land 2 π \in ℝ) \to A + 2 π \in ℝ$
9	7 8	mpan2	$⊢ A \in ℝ \to A + 2 π \in ℝ$
10		elioc2	$⊢ (A \in ℝ^{*} \land A + 2 π \in ℝ) \to (x \in (A, A + 2 π] \leftrightarrow (x \in ℝ \land A < x \land x \leq A + 2 π))$
11	4 9 10	syl2anc	$⊢ A \in ℝ \to (x \in (A, A + 2 π] \leftrightarrow (x \in ℝ \land A < x \land x \leq A + 2 π))$
12		simp1	$⊢ (x \in ℝ \land A < x \land x \leq A + 2 π) \to x \in ℝ$
13	11 12	syl6bi	$⊢ A \in ℝ \to (x \in (A, A + 2 π] \to x \in ℝ)$
14	13	ssrdv	$⊢ A \in ℝ \to (A, A + 2 π] \subseteq ℝ$
15	3 14	eqsstrid	$⊢ A \in ℝ \to D \subseteq ℝ$
16	3	efif1olem1	$⊢ (A \in ℝ \land (x \in D \land y \in D)) \to \|x - y\| < 2 π$
17	3	efif1olem2	$⊢ (A \in ℝ \land z \in ℝ) \to \exists y \in D \frac{z - y}{2 π} \in ℤ$
18		eqid	$⊢ {\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]} = {\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}$
19	1 2 15 16 17 18	efif1olem4	$⊢ A \in ℝ \to F : D \underset{1-1 onto}{⟶} C$