Theorem 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 :ℂ⟶ℂ\setminus \left\{0\right\}$$

Proof

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 {\mathrm{e}}^x\in ℂ$$
5		efne0	$$⊢x\in ℂ\to {\mathrm{e}}^x\ne 0$$
6		eldifsn	$$⊢{\mathrm{e}}^x\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left({\mathrm{e}}^x\in ℂ\wedge {\mathrm{e}}^x\ne 0\right)$$
7	4 5 6	sylanbrc	$$⊢x\in ℂ\to {\mathrm{e}}^x\in \left(ℂ\setminus \left\{0\right\}\right)$$
8	7	rgen	$$⊢\forall x\in ℂ{\mathrm{e}}^x\in \left(ℂ\setminus \left\{0\right\}\right)$$
9		ffnfv	$$⊢\exp :ℂ⟶ℂ\setminus \left\{0\right\}\leftrightarrow \left(\exp Fnℂ\wedge \forall x\in ℂ{\mathrm{e}}^x\in \left(ℂ\setminus \left\{0\right\}\right)\right)$$
10	3 8 9	mpbir2an	$$⊢\exp :ℂ⟶ℂ\setminus \left\{0\right\}$$