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 ‘ ( 𝑌 / 𝑋 ) ) ) ) |
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 ‘ ( 𝑌 / 𝑋 ) ) ) ) |