Description: The (signed) angle between two vectors is in ( -upi (,] pi ) . Deduction form. (Contributed by David Moews, 28-Feb-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ang.1 | ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) | |
| angcld.1 | ⊢ ( 𝜑 → 𝑋 ∈ ℂ ) | ||
| angcld.2 | ⊢ ( 𝜑 → 𝑋 ≠ 0 ) | ||
| angcld.3 | ⊢ ( 𝜑 → 𝑌 ∈ ℂ ) | ||
| angcld.4 | ⊢ ( 𝜑 → 𝑌 ≠ 0 ) | ||
| Assertion | angcld | ⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) ∈ ( - π (,] π ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ang.1 | ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) | |
| 2 | angcld.1 | ⊢ ( 𝜑 → 𝑋 ∈ ℂ ) | |
| 3 | angcld.2 | ⊢ ( 𝜑 → 𝑋 ≠ 0 ) | |
| 4 | angcld.3 | ⊢ ( 𝜑 → 𝑌 ∈ ℂ ) | |
| 5 | angcld.4 | ⊢ ( 𝜑 → 𝑌 ≠ 0 ) | |
| 6 | 1 2 3 4 5 | angvald | ⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ) |
| 7 | 4 2 3 | divcld | ⊢ ( 𝜑 → ( 𝑌 / 𝑋 ) ∈ ℂ ) |
| 8 | 4 2 5 3 | divne0d | ⊢ ( 𝜑 → ( 𝑌 / 𝑋 ) ≠ 0 ) |
| 9 | 7 8 | logimclad | ⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ∈ ( - π (,] π ) ) |
| 10 | 6 9 | eqeltrd | ⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) ∈ ( - π (,] π ) ) |