Metamath Proof Explorer

Theorem angrteqvd

Description: Two vectors are at a right angle iff their quotient is purely imaginary. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses ang.1 ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
angrteqvd.1 ⊢ φ → X ∈ ℂ
angrteqvd.2 ⊢ φ → X ≠ 0
angrteqvd.3 ⊢ φ → Y ∈ ℂ
angrteqvd.4 ⊢ φ → Y ≠ 0
Assertion angrteqvd ⊢ φ → X F Y ∈ π 2 − π 2 ↔ ℜ ⁡ Y X = 0

Proof

Step Hyp Ref Expression
1 ang.1 ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
2 angrteqvd.1 ⊢ φ → X ∈ ℂ
3 angrteqvd.2 ⊢ φ → X ≠ 0
4 angrteqvd.3 ⊢ φ → Y ∈ ℂ
5 angrteqvd.4 ⊢ φ → Y ≠ 0
6 1 2 3 4 5 angvald ⊢ φ → X F Y = ℑ ⁡ log ⁡ Y X
7 6 eleq1d ⊢ φ → X F Y ∈ π 2 − π 2 ↔ ℑ ⁡ log ⁡ Y X ∈ π 2 − π 2
8 4 2 3 divcld ⊢ φ → Y X ∈ ℂ
9 4 2 5 3 divne0d ⊢ φ → Y X ≠ 0
10 8 9 logimclad ⊢ φ → ℑ ⁡ log ⁡ Y X ∈ − π π
11 coseq0negpitopi ⊢ ℑ ⁡ log ⁡ Y X ∈ − π π → cos ⁡ ℑ ⁡ log ⁡ Y X = 0 ↔ ℑ ⁡ log ⁡ Y X ∈ π 2 − π 2
12 10 11 syl ⊢ φ → cos ⁡ ℑ ⁡ log ⁡ Y X = 0 ↔ ℑ ⁡ log ⁡ Y X ∈ π 2 − π 2
13 8 9 cosarg0d ⊢ φ → cos ⁡ ℑ ⁡ log ⁡ Y X = 0 ↔ ℜ ⁡ Y X = 0
14 7 12 13 3bitr2d ⊢ φ → X F Y ∈ π 2 − π 2 ↔ ℜ ⁡ Y X = 0