Metamath Proof Explorer


Theorem angvald

Description: The (signed) angle between two vectors is the argument of their quotient. Deduction form of angval . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses ang.1 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
angvald.1 ( 𝜑𝑋 ∈ ℂ )
angvald.2 ( 𝜑𝑋 ≠ 0 )
angvald.3 ( 𝜑𝑌 ∈ ℂ )
angvald.4 ( 𝜑𝑌 ≠ 0 )
Assertion angvald ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 ang.1 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2 angvald.1 ( 𝜑𝑋 ∈ ℂ )
3 angvald.2 ( 𝜑𝑋 ≠ 0 )
4 angvald.3 ( 𝜑𝑌 ∈ ℂ )
5 angvald.4 ( 𝜑𝑌 ≠ 0 )
6 1 angval ( ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) ∧ ( 𝑌 ∈ ℂ ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 𝐹 𝑌 ) = ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) )
7 2 3 4 5 6 syl22anc ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) )