This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )