Metamath Proof Explorer

Theorem angneg

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

Ref Expression
Hypothesis ang.1 ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
Assertion angneg ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → − A F − B = A F B

Proof

Step Hyp Ref Expression
1 ang.1 ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
2 mulm1 ⊢ A ∈ ℂ → -1 ⁢ A = − A
3 2 ad2antrr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → -1 ⁢ A = − A
4 mulm1 ⊢ B ∈ ℂ → -1 ⁢ B = − B
5 4 ad2antrl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → -1 ⁢ B = − B
6 3 5 oveq12d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → -1 ⁢ A F -1 ⁢ B = − A F − B
7 neg1cn ⊢ − 1 ∈ ℂ
8 neg1ne0 ⊢ − 1 ≠ 0
9 7 8 pm3.2i ⊢ − 1 ∈ ℂ ∧ − 1 ≠ 0
10 1 angcan ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ − 1 ∈ ℂ ∧ − 1 ≠ 0 → -1 ⁢ A F -1 ⁢ B = A F B
11 9 10 mp3an3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → -1 ⁢ A F -1 ⁢ B = A F B
12 6 11 eqtr3d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → − A F − B = A F B