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

Metamath Proof Explorer

Theorem logcld

Description: The logarithm of a nonzero complex number is a complex number. Deduction form of logcl . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses logcld.1 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
logcld.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion logcld ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℂ )

Proof

Step Hyp Ref Expression
1 logcld.1 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
2 logcld.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
3 logcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( log ‘ 𝑋 ) ∈ ℂ )
4 1 2 3 syl2anc ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℂ )