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