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 : ℂ ⟶ ( ℂ ∖ { 0 } )

Proof

Step	Hyp	Ref	Expression
1		eff	⊢ exp : ℂ ⟶ ℂ
2		ffn	⊢ ( exp : ℂ ⟶ ℂ → exp Fn ℂ )
3	1 2	ax-mp	⊢ exp Fn ℂ
4		efcl	⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ℂ )
5		efne0	⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ≠ 0 )
6		eldifsn	⊢ ( ( exp ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( exp ‘ 𝑥 ) ∈ ℂ ∧ ( exp ‘ 𝑥 ) ≠ 0 ) )
7	4 5 6	sylanbrc	⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
8	7	rgen	⊢ ∀ 𝑥 ∈ ℂ ( exp ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } )
9		ffnfv	⊢ ( exp : ℂ ⟶ ( ℂ ∖ { 0 } ) ↔ ( exp Fn ℂ ∧ ∀ 𝑥 ∈ ℂ ( exp ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) )
10	3 8 9	mpbir2an	⊢ exp : ℂ ⟶ ( ℂ ∖ { 0 } )