eff2

Description: The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008)

		Ref	Expression
	Assertion	eff2	$⊢ \exp : ℂ ⟶ ℂ ∖ \{0\}$

Step	Hyp	Ref	Expression
1		eff	$⊢ \exp : ℂ ⟶ ℂ$
2		ffn	$⊢ \exp : ℂ ⟶ ℂ \to \exp Fn ℂ$
3	1 2	ax-mp	$⊢ \exp Fn ℂ$
4		efcl	$⊢ x \in ℂ \to e^{x} \in ℂ$
5		efne0	$⊢ x \in ℂ \to e^{x} \neq 0$
6		eldifsn	$⊢ e^{x} \in (ℂ ∖ \{0\}) \leftrightarrow (e^{x} \in ℂ \land e^{x} \neq 0)$
7	4 5 6	sylanbrc	$⊢ x \in ℂ \to e^{x} \in (ℂ ∖ \{0\})$
8	7	rgen	$⊢ \forall x \in ℂ e^{x} \in (ℂ ∖ \{0\})$
9		ffnfv	$⊢ \exp : ℂ ⟶ ℂ ∖ \{0\} \leftrightarrow (\exp Fn ℂ \land \forall x \in ℂ e^{x} \in (ℂ ∖ \{0\}))$
10	3 8 9	mpbir2an	$⊢ \exp : ℂ ⟶ ℂ ∖ \{0\}$

Metamath Proof Explorer