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	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
	angrteqvd.1	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	angrteqvd.2	⊢ ( 𝜑 → 𝑋 ≠ 0 )
	angrteqvd.3	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
	angrteqvd.4	⊢ ( 𝜑 → 𝑌 ≠ 0 )
Assertion	angrteqvd	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ∈ { ( π / 2 ) , - ( π / 2 ) } ↔ ( ℜ ‘ ( 𝑌 / 𝑋 ) ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		ang.1	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2		angrteqvd.1	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
3		angrteqvd.2	⊢ ( 𝜑 → 𝑋 ≠ 0 )
4		angrteqvd.3	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
5		angrteqvd.4	⊢ ( 𝜑 → 𝑌 ≠ 0 )
6	1 2 3 4 5	angvald	⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) )
7	6	eleq1d	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ∈ { ( π / 2 ) , - ( π / 2 ) } ↔ ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) )
8	4 2 3	divcld	⊢ ( 𝜑 → ( 𝑌 / 𝑋 ) ∈ ℂ )
9	4 2 5 3	divne0d	⊢ ( 𝜑 → ( 𝑌 / 𝑋 ) ≠ 0 )
10	8 9	logimclad	⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ∈ ( - π (,] π ) )
11		coseq0negpitopi	⊢ ( ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ∈ ( - π (,] π ) → ( ( cos ‘ ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ) = 0 ↔ ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) )
12	10 11	syl	⊢ ( 𝜑 → ( ( cos ‘ ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ) = 0 ↔ ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) )
13	8 9	cosarg0d	⊢ ( 𝜑 → ( ( cos ‘ ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ) = 0 ↔ ( ℜ ‘ ( 𝑌 / 𝑋 ) ) = 0 ) )
14	7 12 13	3bitr2d	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ∈ { ( π / 2 ) , - ( π / 2 ) } ↔ ( ℜ ‘ ( 𝑌 / 𝑋 ) ) = 0 ) )