Theorem angneg

Description: Cancel a negative sign in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014)

	Ref	Expression
Hypothesis	ang.1	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
Assertion	angneg	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( - 𝐴 𝐹 - 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ang.1	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2		mulm1	⊢ ( 𝐴 ∈ ℂ → ( - 1 · 𝐴 ) = - 𝐴 )
3	2	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( - 1 · 𝐴 ) = - 𝐴 )
4		mulm1	⊢ ( 𝐵 ∈ ℂ → ( - 1 · 𝐵 ) = - 𝐵 )
5	4	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( - 1 · 𝐵 ) = - 𝐵 )
6	3 5	oveq12d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( - 1 · 𝐴 ) 𝐹 ( - 1 · 𝐵 ) ) = ( - 𝐴 𝐹 - 𝐵 ) )
7		neg1cn	⊢ - 1 ∈ ℂ
8		neg1ne0	⊢ - 1 ≠ 0
9	7 8	pm3.2i	⊢ ( - 1 ∈ ℂ ∧ - 1 ≠ 0 )
10	1	angcan	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ) → ( ( - 1 · 𝐴 ) 𝐹 ( - 1 · 𝐵 ) ) = ( 𝐴 𝐹 𝐵 ) )
11	9 10	mp3an3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( - 1 · 𝐴 ) 𝐹 ( - 1 · 𝐵 ) ) = ( 𝐴 𝐹 𝐵 ) )
12	6 11	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( - 𝐴 𝐹 - 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )